[GOAL]
R : Type u_1
inst✝ : CommSemiring R
⊢ R[X] →ₐ[R] R[T;T⁻¹]
[PROOFSTEP]
refine' AlgHom.comp _ (toFinsuppIsoAlg R).toAlgHom
[GOAL]
R : Type u_1
inst✝ : CommSemiring R
⊢ AddMonoidAlgebra R ℕ →ₐ[R] R[T;T⁻¹]
[PROOFSTEP]
exact mapDomainAlgHom R R Int.ofNatHom
[GOAL]
R : Type u_1
inst✝ : Semiring R
m n : ℤ
⊢ T (m + n) = T m * T n
[PROOFSTEP]
simp [T, single_mul_single]
[GOAL]
R : Type u_1
inst✝ : Semiring R
m n : ℤ
⊢ T (m - n) = T m * T (-n)
[PROOFSTEP]
rw [← T_add, sub_eq_add_neg]
[GOAL]
R : Type u_1
inst✝ : Semiring R
m : ℤ
n : ℕ
⊢ T m ^ n = T (↑n * m)
[PROOFSTEP]
rw [T, T, single_pow n, one_pow, nsmul_eq_mul]
[GOAL]
R : Type u_1
inst✝ : Semiring R
f : R[T;T⁻¹]
m n : ℤ
⊢ f * T m * T n = f * T (m + n)
[PROOFSTEP]
simp [← T_add, mul_assoc]
[GOAL]
R : Type u_1
inst✝ : Semiring R
r : R
n : ℤ
⊢ Finsupp.single n r = ↑C r * T n
[PROOFSTEP]
simp [C, T, single_mul_single]
[GOAL]
R : Type u_1
inst✝ : Semiring R
n : ℕ
r : R
⊢ Finsupp.mapDomain Nat.cast (↑(monomial n) r).toFinsupp = ↑C r * T ↑n
[PROOFSTEP]
rw [toFinsupp_monomial, Finsupp.mapDomain_single, single_eq_C_mul_T]
[GOAL]
R : Type u_1
inst✝ : Semiring R
r : R
⊢ ↑toLaurent (↑Polynomial.C r) = ↑C r
[PROOFSTEP]
convert Polynomial.toLaurent_C_mul_T 0 r
[GOAL]
case h.e'_3
R : Type u_1
inst✝ : Semiring R
r : R
⊢ ↑C r = ↑C r * T ↑0
[PROOFSTEP]
simp only [Int.ofNat_zero, T_zero, mul_one]
[GOAL]
R : Type u_1
inst✝ : Semiring R
⊢ ↑toLaurent X = T 1
[PROOFSTEP]
have : (Polynomial.X : R[X]) = monomial 1 1 := by simp [← C_mul_X_pow_eq_monomial]
[GOAL]
R : Type u_1
inst✝ : Semiring R
⊢ X = ↑(monomial 1) 1
[PROOFSTEP]
simp [← C_mul_X_pow_eq_monomial]
[GOAL]
R : Type u_1
inst✝ : Semiring R
this : X = ↑(monomial 1) 1
⊢ ↑toLaurent X = T 1
[PROOFSTEP]
simp [this, Polynomial.toLaurent_C_mul_T]
[GOAL]
R : Type u_1
inst✝ : Semiring R
r : R
f : R[X]
⊢ ↑toLaurent (↑Polynomial.C r * f) = ↑C r * ↑toLaurent f
[PROOFSTEP]
simp only [_root_.map_mul, Polynomial.toLaurent_C]
[GOAL]
R : Type u_1
inst✝ : Semiring R
n : ℕ
⊢ ↑toLaurent (X ^ n) = T ↑n
[PROOFSTEP]
simp only [map_pow, Polynomial.toLaurent_X, T_pow, mul_one]
[GOAL]
R : Type u_1
inst✝ : Semiring R
n : ℕ
r : R
⊢ ↑toLaurent (↑Polynomial.C r * X ^ n) = ↑C r * T ↑n
[PROOFSTEP]
simp only [_root_.map_mul, Polynomial.toLaurent_C, Polynomial.toLaurent_X_pow]
[GOAL]
R : Type u_1
inst✝ : Semiring R
n : ℤ
⊢ T (-n) * T n = 1
[PROOFSTEP]
rw [← T_add, add_left_neg, T_zero]
[GOAL]
R : Type u_1
inst✝ : Semiring R
n : ℤ
⊢ T n * T (-n) = 1
[PROOFSTEP]
rw [← T_add, add_right_neg, T_zero]
[GOAL]
R : Type u_1
inst✝ : Semiring R
M : R[T;T⁻¹] → Prop
p : R[T;T⁻¹]
h_C : ∀ (a : R), M (↑C a)
h_add : ∀ {p q : R[T;T⁻¹]}, M p → M q → M (p + q)
h_C_mul_T : ∀ (n : ℕ) (a : R), M (↑C a * T ↑n) → M (↑C a * T (↑n + 1))
h_C_mul_T_Z : ∀ (n : ℕ) (a : R), M (↑C a * T (-↑n)) → M (↑C a * T (-↑n - 1))
⊢ M p
[PROOFSTEP]
have A : ∀ {n : ℤ} {a : R}, M (C a * T n) := by
  intro n a
  refine Int.induction_on n ?_ ?_ ?_
  · simpa only [T_zero, mul_one] using h_C a
  · exact fun m => h_C_mul_T m a
  · exact fun m => h_C_mul_T_Z m a
[GOAL]
R : Type u_1
inst✝ : Semiring R
M : R[T;T⁻¹] → Prop
p : R[T;T⁻¹]
h_C : ∀ (a : R), M (↑C a)
h_add : ∀ {p q : R[T;T⁻¹]}, M p → M q → M (p + q)
h_C_mul_T : ∀ (n : ℕ) (a : R), M (↑C a * T ↑n) → M (↑C a * T (↑n + 1))
h_C_mul_T_Z : ∀ (n : ℕ) (a : R), M (↑C a * T (-↑n)) → M (↑C a * T (-↑n - 1))
⊢ ∀ {n : ℤ} {a : R}, M (↑C a * T n)
[PROOFSTEP]
intro n a
[GOAL]
R : Type u_1
inst✝ : Semiring R
M : R[T;T⁻¹] → Prop
p : R[T;T⁻¹]
h_C : ∀ (a : R), M (↑C a)
h_add : ∀ {p q : R[T;T⁻¹]}, M p → M q → M (p + q)
h_C_mul_T : ∀ (n : ℕ) (a : R), M (↑C a * T ↑n) → M (↑C a * T (↑n + 1))
h_C_mul_T_Z : ∀ (n : ℕ) (a : R), M (↑C a * T (-↑n)) → M (↑C a * T (-↑n - 1))
n : ℤ
a : R
⊢ M (↑C a * T n)
[PROOFSTEP]
refine Int.induction_on n ?_ ?_ ?_
[GOAL]
case refine_1
R : Type u_1
inst✝ : Semiring R
M : R[T;T⁻¹] → Prop
p : R[T;T⁻¹]
h_C : ∀ (a : R), M (↑C a)
h_add : ∀ {p q : R[T;T⁻¹]}, M p → M q → M (p + q)
h_C_mul_T : ∀ (n : ℕ) (a : R), M (↑C a * T ↑n) → M (↑C a * T (↑n + 1))
h_C_mul_T_Z : ∀ (n : ℕ) (a : R), M (↑C a * T (-↑n)) → M (↑C a * T (-↑n - 1))
n : ℤ
a : R
⊢ M (↑C a * T 0)
[PROOFSTEP]
simpa only [T_zero, mul_one] using h_C a
[GOAL]
case refine_2
R : Type u_1
inst✝ : Semiring R
M : R[T;T⁻¹] → Prop
p : R[T;T⁻¹]
h_C : ∀ (a : R), M (↑C a)
h_add : ∀ {p q : R[T;T⁻¹]}, M p → M q → M (p + q)
h_C_mul_T : ∀ (n : ℕ) (a : R), M (↑C a * T ↑n) → M (↑C a * T (↑n + 1))
h_C_mul_T_Z : ∀ (n : ℕ) (a : R), M (↑C a * T (-↑n)) → M (↑C a * T (-↑n - 1))
n : ℤ
a : R
⊢ ∀ (i : ℕ), M (↑C a * T ↑i) → M (↑C a * T (↑i + 1))
[PROOFSTEP]
exact fun m => h_C_mul_T m a
[GOAL]
case refine_3
R : Type u_1
inst✝ : Semiring R
M : R[T;T⁻¹] → Prop
p : R[T;T⁻¹]
h_C : ∀ (a : R), M (↑C a)
h_add : ∀ {p q : R[T;T⁻¹]}, M p → M q → M (p + q)
h_C_mul_T : ∀ (n : ℕ) (a : R), M (↑C a * T ↑n) → M (↑C a * T (↑n + 1))
h_C_mul_T_Z : ∀ (n : ℕ) (a : R), M (↑C a * T (-↑n)) → M (↑C a * T (-↑n - 1))
n : ℤ
a : R
⊢ ∀ (i : ℕ), M (↑C a * T (-↑i)) → M (↑C a * T (-↑i - 1))
[PROOFSTEP]
exact fun m => h_C_mul_T_Z m a
[GOAL]
R : Type u_1
inst✝ : Semiring R
M : R[T;T⁻¹] → Prop
p : R[T;T⁻¹]
h_C : ∀ (a : R), M (↑C a)
h_add : ∀ {p q : R[T;T⁻¹]}, M p → M q → M (p + q)
h_C_mul_T : ∀ (n : ℕ) (a : R), M (↑C a * T ↑n) → M (↑C a * T (↑n + 1))
h_C_mul_T_Z : ∀ (n : ℕ) (a : R), M (↑C a * T (-↑n)) → M (↑C a * T (-↑n - 1))
A : ∀ {n : ℤ} {a : R}, M (↑C a * T n)
⊢ M p
[PROOFSTEP]
have B : ∀ s : Finset ℤ, M (s.sum fun n : ℤ => C (p.toFun n) * T n) :=
  by
  apply Finset.induction
  · convert h_C 0
    simp only [Finset.sum_empty, _root_.map_zero]
  · intro n s ns ih
    rw [Finset.sum_insert ns]
    exact h_add A ih
[GOAL]
R : Type u_1
inst✝ : Semiring R
M : R[T;T⁻¹] → Prop
p : R[T;T⁻¹]
h_C : ∀ (a : R), M (↑C a)
h_add : ∀ {p q : R[T;T⁻¹]}, M p → M q → M (p + q)
h_C_mul_T : ∀ (n : ℕ) (a : R), M (↑C a * T ↑n) → M (↑C a * T (↑n + 1))
h_C_mul_T_Z : ∀ (n : ℕ) (a : R), M (↑C a * T (-↑n)) → M (↑C a * T (-↑n - 1))
A : ∀ {n : ℤ} {a : R}, M (↑C a * T n)
⊢ ∀ (s : Finset ℤ), M (∑ n in s, ↑C (toFun p n) * T n)
[PROOFSTEP]
apply Finset.induction
[GOAL]
case empty
R : Type u_1
inst✝ : Semiring R
M : R[T;T⁻¹] → Prop
p : R[T;T⁻¹]
h_C : ∀ (a : R), M (↑C a)
h_add : ∀ {p q : R[T;T⁻¹]}, M p → M q → M (p + q)
h_C_mul_T : ∀ (n : ℕ) (a : R), M (↑C a * T ↑n) → M (↑C a * T (↑n + 1))
h_C_mul_T_Z : ∀ (n : ℕ) (a : R), M (↑C a * T (-↑n)) → M (↑C a * T (-↑n - 1))
A : ∀ {n : ℤ} {a : R}, M (↑C a * T n)
⊢ M (∑ n in ∅, ↑C (toFun p n) * T n)
[PROOFSTEP]
convert h_C 0
[GOAL]
case h.e'_1
R : Type u_1
inst✝ : Semiring R
M : R[T;T⁻¹] → Prop
p : R[T;T⁻¹]
h_C : ∀ (a : R), M (↑C a)
h_add : ∀ {p q : R[T;T⁻¹]}, M p → M q → M (p + q)
h_C_mul_T : ∀ (n : ℕ) (a : R), M (↑C a * T ↑n) → M (↑C a * T (↑n + 1))
h_C_mul_T_Z : ∀ (n : ℕ) (a : R), M (↑C a * T (-↑n)) → M (↑C a * T (-↑n - 1))
A : ∀ {n : ℤ} {a : R}, M (↑C a * T n)
⊢ ∑ n in ∅, ↑C (toFun p n) * T n = ↑C 0
[PROOFSTEP]
simp only [Finset.sum_empty, _root_.map_zero]
[GOAL]
case insert
R : Type u_1
inst✝ : Semiring R
M : R[T;T⁻¹] → Prop
p : R[T;T⁻¹]
h_C : ∀ (a : R), M (↑C a)
h_add : ∀ {p q : R[T;T⁻¹]}, M p → M q → M (p + q)
h_C_mul_T : ∀ (n : ℕ) (a : R), M (↑C a * T ↑n) → M (↑C a * T (↑n + 1))
h_C_mul_T_Z : ∀ (n : ℕ) (a : R), M (↑C a * T (-↑n)) → M (↑C a * T (-↑n - 1))
A : ∀ {n : ℤ} {a : R}, M (↑C a * T n)
⊢ ∀ ⦃a : ℤ⦄ {s : Finset ℤ}, ¬a ∈ s → M (∑ n in s, ↑C (toFun p n) * T n) → M (∑ n in insert a s, ↑C (toFun p n) * T n)
[PROOFSTEP]
intro n s ns ih
[GOAL]
case insert
R : Type u_1
inst✝ : Semiring R
M : R[T;T⁻¹] → Prop
p : R[T;T⁻¹]
h_C : ∀ (a : R), M (↑C a)
h_add : ∀ {p q : R[T;T⁻¹]}, M p → M q → M (p + q)
h_C_mul_T : ∀ (n : ℕ) (a : R), M (↑C a * T ↑n) → M (↑C a * T (↑n + 1))
h_C_mul_T_Z : ∀ (n : ℕ) (a : R), M (↑C a * T (-↑n)) → M (↑C a * T (-↑n - 1))
A : ∀ {n : ℤ} {a : R}, M (↑C a * T n)
n : ℤ
s : Finset ℤ
ns : ¬n ∈ s
ih : M (∑ n in s, ↑C (toFun p n) * T n)
⊢ M (∑ n in insert n s, ↑C (toFun p n) * T n)
[PROOFSTEP]
rw [Finset.sum_insert ns]
[GOAL]
case insert
R : Type u_1
inst✝ : Semiring R
M : R[T;T⁻¹] → Prop
p : R[T;T⁻¹]
h_C : ∀ (a : R), M (↑C a)
h_add : ∀ {p q : R[T;T⁻¹]}, M p → M q → M (p + q)
h_C_mul_T : ∀ (n : ℕ) (a : R), M (↑C a * T ↑n) → M (↑C a * T (↑n + 1))
h_C_mul_T_Z : ∀ (n : ℕ) (a : R), M (↑C a * T (-↑n)) → M (↑C a * T (-↑n - 1))
A : ∀ {n : ℤ} {a : R}, M (↑C a * T n)
n : ℤ
s : Finset ℤ
ns : ¬n ∈ s
ih : M (∑ n in s, ↑C (toFun p n) * T n)
⊢ M (↑C (toFun p n) * T n + ∑ x in s, ↑C (toFun p x) * T x)
[PROOFSTEP]
exact h_add A ih
[GOAL]
R : Type u_1
inst✝ : Semiring R
M : R[T;T⁻¹] → Prop
p : R[T;T⁻¹]
h_C : ∀ (a : R), M (↑C a)
h_add : ∀ {p q : R[T;T⁻¹]}, M p → M q → M (p + q)
h_C_mul_T : ∀ (n : ℕ) (a : R), M (↑C a * T ↑n) → M (↑C a * T (↑n + 1))
h_C_mul_T_Z : ∀ (n : ℕ) (a : R), M (↑C a * T (-↑n)) → M (↑C a * T (-↑n - 1))
A : ∀ {n : ℤ} {a : R}, M (↑C a * T n)
B : ∀ (s : Finset ℤ), M (∑ n in s, ↑C (toFun p n) * T n)
⊢ M p
[PROOFSTEP]
convert B p.support
[GOAL]
case h.e'_1
R : Type u_1
inst✝ : Semiring R
M : R[T;T⁻¹] → Prop
p : R[T;T⁻¹]
h_C : ∀ (a : R), M (↑C a)
h_add : ∀ {p q : R[T;T⁻¹]}, M p → M q → M (p + q)
h_C_mul_T : ∀ (n : ℕ) (a : R), M (↑C a * T ↑n) → M (↑C a * T (↑n + 1))
h_C_mul_T_Z : ∀ (n : ℕ) (a : R), M (↑C a * T (-↑n)) → M (↑C a * T (-↑n - 1))
A : ∀ {n : ℤ} {a : R}, M (↑C a * T n)
B : ∀ (s : Finset ℤ), M (∑ n in s, ↑C (toFun p n) * T n)
⊢ p = ∑ n in p.support, ↑C (toFun p n) * T n
[PROOFSTEP]
ext a
[GOAL]
case h.e'_1.h
R : Type u_1
inst✝ : Semiring R
M : R[T;T⁻¹] → Prop
p : R[T;T⁻¹]
h_C : ∀ (a : R), M (↑C a)
h_add : ∀ {p q : R[T;T⁻¹]}, M p → M q → M (p + q)
h_C_mul_T : ∀ (n : ℕ) (a : R), M (↑C a * T ↑n) → M (↑C a * T (↑n + 1))
h_C_mul_T_Z : ∀ (n : ℕ) (a : R), M (↑C a * T (-↑n)) → M (↑C a * T (-↑n - 1))
A : ∀ {n : ℤ} {a : R}, M (↑C a * T n)
B : ∀ (s : Finset ℤ), M (∑ n in s, ↑C (toFun p n) * T n)
a : ℤ
⊢ ↑p a = ↑(∑ n in p.support, ↑C (toFun p n) * T n) a
[PROOFSTEP]
simp_rw [← single_eq_C_mul_T]
  -- Porting note: did not make progress in `simp_rw`
[GOAL]
case h.e'_1.h
R : Type u_1
inst✝ : Semiring R
M : R[T;T⁻¹] → Prop
p : R[T;T⁻¹]
h_C : ∀ (a : R), M (↑C a)
h_add : ∀ {p q : R[T;T⁻¹]}, M p → M q → M (p + q)
h_C_mul_T : ∀ (n : ℕ) (a : R), M (↑C a * T ↑n) → M (↑C a * T (↑n + 1))
h_C_mul_T_Z : ∀ (n : ℕ) (a : R), M (↑C a * T (-↑n)) → M (↑C a * T (-↑n - 1))
A : ∀ {n : ℤ} {a : R}, M (↑C a * T n)
B : ∀ (s : Finset ℤ), M (∑ n in s, ↑C (toFun p n) * T n)
a : ℤ
⊢ ↑p a = ↑(∑ x in p.support, Finsupp.single x (toFun p x)) a
[PROOFSTEP]
rw [Finset.sum_apply']
[GOAL]
case h.e'_1.h
R : Type u_1
inst✝ : Semiring R
M : R[T;T⁻¹] → Prop
p : R[T;T⁻¹]
h_C : ∀ (a : R), M (↑C a)
h_add : ∀ {p q : R[T;T⁻¹]}, M p → M q → M (p + q)
h_C_mul_T : ∀ (n : ℕ) (a : R), M (↑C a * T ↑n) → M (↑C a * T (↑n + 1))
h_C_mul_T_Z : ∀ (n : ℕ) (a : R), M (↑C a * T (-↑n)) → M (↑C a * T (-↑n - 1))
A : ∀ {n : ℤ} {a : R}, M (↑C a * T n)
B : ∀ (s : Finset ℤ), M (∑ n in s, ↑C (toFun p n) * T n)
a : ℤ
⊢ ↑p a = ∑ k in p.support, ↑(Finsupp.single k (toFun p k)) a
[PROOFSTEP]
simp_rw [Finsupp.single_apply, Finset.sum_ite_eq']
[GOAL]
case h.e'_1.h
R : Type u_1
inst✝ : Semiring R
M : R[T;T⁻¹] → Prop
p : R[T;T⁻¹]
h_C : ∀ (a : R), M (↑C a)
h_add : ∀ {p q : R[T;T⁻¹]}, M p → M q → M (p + q)
h_C_mul_T : ∀ (n : ℕ) (a : R), M (↑C a * T ↑n) → M (↑C a * T (↑n + 1))
h_C_mul_T_Z : ∀ (n : ℕ) (a : R), M (↑C a * T (-↑n)) → M (↑C a * T (-↑n - 1))
A : ∀ {n : ℤ} {a : R}, M (↑C a * T n)
B : ∀ (s : Finset ℤ), M (∑ n in s, ↑C (toFun p n) * T n)
a : ℤ
⊢ ↑p a = if a ∈ p.support then toFun p a else 0
[PROOFSTEP]
split_ifs with h
[GOAL]
case pos
R : Type u_1
inst✝ : Semiring R
M : R[T;T⁻¹] → Prop
p : R[T;T⁻¹]
h_C : ∀ (a : R), M (↑C a)
h_add : ∀ {p q : R[T;T⁻¹]}, M p → M q → M (p + q)
h_C_mul_T : ∀ (n : ℕ) (a : R), M (↑C a * T ↑n) → M (↑C a * T (↑n + 1))
h_C_mul_T_Z : ∀ (n : ℕ) (a : R), M (↑C a * T (-↑n)) → M (↑C a * T (-↑n - 1))
A : ∀ {n : ℤ} {a : R}, M (↑C a * T n)
B : ∀ (s : Finset ℤ), M (∑ n in s, ↑C (toFun p n) * T n)
a : ℤ
h : a ∈ p.support
⊢ ↑p a = toFun p a
[PROOFSTEP]
rfl
[GOAL]
case neg
R : Type u_1
inst✝ : Semiring R
M : R[T;T⁻¹] → Prop
p : R[T;T⁻¹]
h_C : ∀ (a : R), M (↑C a)
h_add : ∀ {p q : R[T;T⁻¹]}, M p → M q → M (p + q)
h_C_mul_T : ∀ (n : ℕ) (a : R), M (↑C a * T ↑n) → M (↑C a * T (↑n + 1))
h_C_mul_T_Z : ∀ (n : ℕ) (a : R), M (↑C a * T (-↑n)) → M (↑C a * T (-↑n - 1))
A : ∀ {n : ℤ} {a : R}, M (↑C a * T n)
B : ∀ (s : Finset ℤ), M (∑ n in s, ↑C (toFun p n) * T n)
a : ℤ
h : ¬a ∈ p.support
⊢ ↑p a = 0
[PROOFSTEP]
exact Finsupp.not_mem_support_iff.mp h
[GOAL]
R : Type u_1
inst✝ : Semiring R
M : R[T;T⁻¹] → Prop
p : R[T;T⁻¹]
h_add : ∀ (p q : R[T;T⁻¹]), M p → M q → M (p + q)
h_C_mul_T : ∀ (n : ℤ) (a : R), M (↑C a * T n)
⊢ M p
[PROOFSTEP]
refine' p.induction_on (fun a => _) (fun {p q} => h_add p q) _ _
[GOAL]
case refine'_1
R : Type u_1
inst✝ : Semiring R
M : R[T;T⁻¹] → Prop
p : R[T;T⁻¹]
h_add : ∀ (p q : R[T;T⁻¹]), M p → M q → M (p + q)
h_C_mul_T : ∀ (n : ℤ) (a : R), M (↑C a * T n)
a : R
⊢ M (↑C a)
[PROOFSTEP]
try exact fun n f _ => h_C_mul_T _ f
[GOAL]
case refine'_1
R : Type u_1
inst✝ : Semiring R
M : R[T;T⁻¹] → Prop
p : R[T;T⁻¹]
h_add : ∀ (p q : R[T;T⁻¹]), M p → M q → M (p + q)
h_C_mul_T : ∀ (n : ℤ) (a : R), M (↑C a * T n)
a : R
⊢ M (↑C a)
[PROOFSTEP]
exact fun n f _ => h_C_mul_T _ f
[GOAL]
case refine'_2
R : Type u_1
inst✝ : Semiring R
M : R[T;T⁻¹] → Prop
p : R[T;T⁻¹]
h_add : ∀ (p q : R[T;T⁻¹]), M p → M q → M (p + q)
h_C_mul_T : ∀ (n : ℤ) (a : R), M (↑C a * T n)
⊢ ∀ (n : ℕ) (a : R), M (↑C a * T ↑n) → M (↑C a * T (↑n + 1))
[PROOFSTEP]
try exact fun n f _ => h_C_mul_T _ f
[GOAL]
case refine'_2
R : Type u_1
inst✝ : Semiring R
M : R[T;T⁻¹] → Prop
p : R[T;T⁻¹]
h_add : ∀ (p q : R[T;T⁻¹]), M p → M q → M (p + q)
h_C_mul_T : ∀ (n : ℤ) (a : R), M (↑C a * T n)
⊢ ∀ (n : ℕ) (a : R), M (↑C a * T ↑n) → M (↑C a * T (↑n + 1))
[PROOFSTEP]
exact fun n f _ => h_C_mul_T _ f
[GOAL]
case refine'_3
R : Type u_1
inst✝ : Semiring R
M : R[T;T⁻¹] → Prop
p : R[T;T⁻¹]
h_add : ∀ (p q : R[T;T⁻¹]), M p → M q → M (p + q)
h_C_mul_T : ∀ (n : ℤ) (a : R), M (↑C a * T n)
⊢ ∀ (n : ℕ) (a : R), M (↑C a * T (-↑n)) → M (↑C a * T (-↑n - 1))
[PROOFSTEP]
try exact fun n f _ => h_C_mul_T _ f
[GOAL]
case refine'_3
R : Type u_1
inst✝ : Semiring R
M : R[T;T⁻¹] → Prop
p : R[T;T⁻¹]
h_add : ∀ (p q : R[T;T⁻¹]), M p → M q → M (p + q)
h_C_mul_T : ∀ (n : ℤ) (a : R), M (↑C a * T n)
⊢ ∀ (n : ℕ) (a : R), M (↑C a * T (-↑n)) → M (↑C a * T (-↑n - 1))
[PROOFSTEP]
exact fun n f _ => h_C_mul_T _ f
[GOAL]
case refine'_1
R : Type u_1
inst✝ : Semiring R
M : R[T;T⁻¹] → Prop
p : R[T;T⁻¹]
h_add : ∀ (p q : R[T;T⁻¹]), M p → M q → M (p + q)
h_C_mul_T : ∀ (n : ℤ) (a : R), M (↑C a * T n)
a : R
⊢ M (↑C a)
[PROOFSTEP]
convert h_C_mul_T 0 a
[GOAL]
case h.e'_1
R : Type u_1
inst✝ : Semiring R
M : R[T;T⁻¹] → Prop
p : R[T;T⁻¹]
h_add : ∀ (p q : R[T;T⁻¹]), M p → M q → M (p + q)
h_C_mul_T : ∀ (n : ℤ) (a : R), M (↑C a * T n)
a : R
⊢ ↑C a = ↑C a * T 0
[PROOFSTEP]
exact (mul_one _).symm
[GOAL]
R : Type u_1
inst✝ : Semiring R
n : ℤ
f : R[T;T⁻¹]
m : ℤ
a : R
⊢ T n * (↑C a * T m) = ↑C a * T m * T n
[PROOFSTEP]
rw [T, T, ← single_eq_C, single_mul_single, single_mul_single, single_mul_single]
[GOAL]
R : Type u_1
inst✝ : Semiring R
n : ℤ
f : R[T;T⁻¹]
m : ℤ
a : R
⊢ AddMonoidAlgebra.single (n + (0 + m)) (1 * (a * 1)) = AddMonoidAlgebra.single (0 + m + n) (a * 1 * 1)
[PROOFSTEP]
simp [add_comm]
[GOAL]
R : Type u_1
inst✝ : Semiring R
n : ℤ
r : R
⊢ ↑trunc (↑C r * T n) = if 0 ≤ n then ↑(monomial (Int.toNat n)) r else 0
[PROOFSTEP]
have : Function.Injective Int.ofNat := fun x y h => Int.ofNat_inj.mp h
[GOAL]
R : Type u_1
inst✝ : Semiring R
n : ℤ
r : R
this : Function.Injective Int.ofNat
⊢ ↑trunc (↑C r * T n) = if 0 ≤ n then ↑(monomial (Int.toNat n)) r else 0
[PROOFSTEP]
apply (toFinsuppIso R).injective
[GOAL]
case a
R : Type u_1
inst✝ : Semiring R
n : ℤ
r : R
this : Function.Injective Int.ofNat
⊢ ↑(toFinsuppIso R) (↑trunc (↑C r * T n)) = ↑(toFinsuppIso R) (if 0 ≤ n then ↑(monomial (Int.toNat n)) r else 0)
[PROOFSTEP]
rw [← single_eq_C_mul_T, trunc, AddMonoidHom.coe_comp, Function.comp_apply]
  -- Porting note: was `rw`
[GOAL]
case a
R : Type u_1
inst✝ : Semiring R
n : ℤ
r : R
this : Function.Injective Int.ofNat
⊢ ↑(toFinsuppIso R)
      (↑(RingEquiv.toAddMonoidHom (RingEquiv.symm (toFinsuppIso R)))
        (↑(comapDomain.addMonoidHom (_ : ∀ (x x_1 : ℕ), Int.ofNat x = Int.ofNat x_1 → x = x_1)) (Finsupp.single n r))) =
    ↑(toFinsuppIso R) (if 0 ≤ n then ↑(monomial (Int.toNat n)) r else 0)
[PROOFSTEP]
erw [comapDomain.addMonoidHom_apply this]
[GOAL]
case a
R : Type u_1
inst✝ : Semiring R
n : ℤ
r : R
this : Function.Injective Int.ofNat
⊢ comapDomain Int.ofNat (Finsupp.single n r) (_ : Set.InjOn Int.ofNat (Int.ofNat ⁻¹' ↑(Finsupp.single n r).support)) =
    ↑(toFinsuppIso R) (if 0 ≤ n then ↑(monomial (Int.toNat n)) r else 0)
[PROOFSTEP]
rw [toFinsuppIso_apply]
  -- Porting note: rewrote proof below relative to mathlib3.
[GOAL]
case a
R : Type u_1
inst✝ : Semiring R
n : ℤ
r : R
this : Function.Injective Int.ofNat
⊢ comapDomain Int.ofNat (Finsupp.single n r) (_ : Set.InjOn Int.ofNat (Int.ofNat ⁻¹' ↑(Finsupp.single n r).support)) =
    (if 0 ≤ n then ↑(monomial (Int.toNat n)) r else 0).toFinsupp
[PROOFSTEP]
by_cases n0 : 0 ≤ n
[GOAL]
case pos
R : Type u_1
inst✝ : Semiring R
n : ℤ
r : R
this : Function.Injective Int.ofNat
n0 : 0 ≤ n
⊢ comapDomain Int.ofNat (Finsupp.single n r) (_ : Set.InjOn Int.ofNat (Int.ofNat ⁻¹' ↑(Finsupp.single n r).support)) =
    (if 0 ≤ n then ↑(monomial (Int.toNat n)) r else 0).toFinsupp
[PROOFSTEP]
lift n to ℕ using n0
[GOAL]
case pos.intro
R : Type u_1
inst✝ : Semiring R
r : R
this : Function.Injective Int.ofNat
n : ℕ
⊢ comapDomain Int.ofNat (Finsupp.single (↑n) r)
      (_ : Set.InjOn Int.ofNat (Int.ofNat ⁻¹' ↑(Finsupp.single (↑n) r).support)) =
    (if 0 ≤ ↑n then ↑(monomial (Int.toNat ↑n)) r else 0).toFinsupp
[PROOFSTEP]
erw [comapDomain_single]
[GOAL]
case pos.intro
R : Type u_1
inst✝ : Semiring R
r : R
this : Function.Injective Int.ofNat
n : ℕ
⊢ Finsupp.single n r = (if 0 ≤ ↑n then ↑(monomial (Int.toNat ↑n)) r else 0).toFinsupp
[PROOFSTEP]
simp only [Nat.cast_nonneg, Int.toNat_ofNat, ite_true, toFinsupp_monomial]
[GOAL]
case neg
R : Type u_1
inst✝ : Semiring R
n : ℤ
r : R
this : Function.Injective Int.ofNat
n0 : ¬0 ≤ n
⊢ comapDomain Int.ofNat (Finsupp.single n r) (_ : Set.InjOn Int.ofNat (Int.ofNat ⁻¹' ↑(Finsupp.single n r).support)) =
    (if 0 ≤ n then ↑(monomial (Int.toNat n)) r else 0).toFinsupp
[PROOFSTEP]
lift -n to ℕ using (neg_pos.mpr (not_le.mp n0)).le with m
[GOAL]
case neg.intro
R : Type u_1
inst✝ : Semiring R
n : ℤ
r : R
this : Function.Injective Int.ofNat
n0 : ¬0 ≤ n
m : ℕ
trunc_C_mul_T✝ trunc_C_mul_T : ∀ (n : ℤ) (r : R), ↑trunc (↑C r * T n) = if 0 ≤ n then ↑(monomial (Int.toNat n)) r else 0
⊢ comapDomain Int.ofNat (Finsupp.single n r) (_ : Set.InjOn Int.ofNat (Int.ofNat ⁻¹' ↑(Finsupp.single n r).support)) =
    (if 0 ≤ n then ↑(monomial (Int.toNat n)) r else 0).toFinsupp
[PROOFSTEP]
rw [toFinsupp_inj, if_neg n0]
[GOAL]
case neg.intro
R : Type u_1
inst✝ : Semiring R
n : ℤ
r : R
this : Function.Injective Int.ofNat
n0 : ¬0 ≤ n
m : ℕ
trunc_C_mul_T✝ trunc_C_mul_T : ∀ (n : ℤ) (r : R), ↑trunc (↑C r * T n) = if 0 ≤ n then ↑(monomial (Int.toNat n)) r else 0
⊢ {
      toFinsupp :=
        comapDomain Int.ofNat (Finsupp.single n r)
          (_ : Set.InjOn Int.ofNat (Int.ofNat ⁻¹' ↑(Finsupp.single n r).support)) } =
    0
[PROOFSTEP]
ext a
[GOAL]
case neg.intro.a
R : Type u_1
inst✝ : Semiring R
n : ℤ
r : R
this : Function.Injective Int.ofNat
n0 : ¬0 ≤ n
m : ℕ
trunc_C_mul_T✝ trunc_C_mul_T : ∀ (n : ℤ) (r : R), ↑trunc (↑C r * T n) = if 0 ≤ n then ↑(monomial (Int.toNat n)) r else 0
a : ℕ
⊢ coeff
      {
        toFinsupp :=
          comapDomain Int.ofNat (Finsupp.single n r)
            (_ : Set.InjOn Int.ofNat (Int.ofNat ⁻¹' ↑(Finsupp.single n r).support)) }
      a =
    coeff 0 a
[PROOFSTEP]
have := ((not_le.mp n0).trans_le (Int.ofNat_zero_le a)).ne
[GOAL]
case neg.intro.a
R : Type u_1
inst✝ : Semiring R
n : ℤ
r : R
this✝ : Function.Injective Int.ofNat
n0 : ¬0 ≤ n
m : ℕ
trunc_C_mul_T✝ trunc_C_mul_T : ∀ (n : ℤ) (r : R), ↑trunc (↑C r * T n) = if 0 ≤ n then ↑(monomial (Int.toNat n)) r else 0
a : ℕ
this : n ≠ ↑a
⊢ coeff
      {
        toFinsupp :=
          comapDomain Int.ofNat (Finsupp.single n r)
            (_ : Set.InjOn Int.ofNat (Int.ofNat ⁻¹' ↑(Finsupp.single n r).support)) }
      a =
    coeff 0 a
[PROOFSTEP]
simp only [coeff_ofFinsupp, comapDomain_apply, Int.ofNat_eq_coe, coeff_zero, single_eq_of_ne this]
[GOAL]
R : Type u_1
inst✝ : Semiring R
⊢ Function.LeftInverse ↑trunc ↑toLaurent
[PROOFSTEP]
refine' fun f => f.induction_on' _ _
[GOAL]
case refine'_1
R : Type u_1
inst✝ : Semiring R
f : R[X]
⊢ ∀ (p q : R[X]), ↑trunc (↑toLaurent p) = p → ↑trunc (↑toLaurent q) = q → ↑trunc (↑toLaurent (p + q)) = p + q
[PROOFSTEP]
intro f g hf hg
[GOAL]
case refine'_1
R : Type u_1
inst✝ : Semiring R
f✝ f g : R[X]
hf : ↑trunc (↑toLaurent f) = f
hg : ↑trunc (↑toLaurent g) = g
⊢ ↑trunc (↑toLaurent (f + g)) = f + g
[PROOFSTEP]
simp only [hf, hg, _root_.map_add]
[GOAL]
case refine'_2
R : Type u_1
inst✝ : Semiring R
f : R[X]
⊢ ∀ (n : ℕ) (a : R), ↑trunc (↑toLaurent (↑(monomial n) a)) = ↑(monomial n) a
[PROOFSTEP]
intro n r
[GOAL]
case refine'_2
R : Type u_1
inst✝ : Semiring R
f : R[X]
n : ℕ
r : R
⊢ ↑trunc (↑toLaurent (↑(monomial n) r)) = ↑(monomial n) r
[PROOFSTEP]
simp only [Polynomial.toLaurent_C_mul_T, trunc_C_mul_T, Int.coe_nat_nonneg, Int.toNat_coe_nat, if_true]
[GOAL]
R : Type u_1
inst✝ : Semiring R
f : R[T;T⁻¹]
⊢ ∃ n f', ↑toLaurent f' = f * T ↑n
[PROOFSTEP]
refine f.induction_on' ?_ fun n a => ?_
[GOAL]
case refine_1
R : Type u_1
inst✝ : Semiring R
f : R[T;T⁻¹]
⊢ ∀ (p q : R[T;T⁻¹]),
    (∃ n f', ↑toLaurent f' = p * T ↑n) → (∃ n f', ↑toLaurent f' = q * T ↑n) → ∃ n f', ↑toLaurent f' = (p + q) * T ↑n
[PROOFSTEP]
clear f
[GOAL]
case refine_2
R : Type u_1
inst✝ : Semiring R
f : R[T;T⁻¹]
n : ℤ
a : R
⊢ ∃ n_1 f', ↑toLaurent f' = ↑C a * T n * T ↑n_1
[PROOFSTEP]
clear f
[GOAL]
case refine_1
R : Type u_1
inst✝ : Semiring R
⊢ ∀ (p q : R[T;T⁻¹]),
    (∃ n f', ↑toLaurent f' = p * T ↑n) → (∃ n f', ↑toLaurent f' = q * T ↑n) → ∃ n f', ↑toLaurent f' = (p + q) * T ↑n
[PROOFSTEP]
rintro f g ⟨m, fn, hf⟩ ⟨n, gn, hg⟩
[GOAL]
case refine_1.intro.intro.intro.intro
R : Type u_1
inst✝ : Semiring R
f g : R[T;T⁻¹]
m : ℕ
fn : R[X]
hf : ↑toLaurent fn = f * T ↑m
n : ℕ
gn : R[X]
hg : ↑toLaurent gn = g * T ↑n
⊢ ∃ n f', ↑toLaurent f' = (f + g) * T ↑n
[PROOFSTEP]
refine' ⟨m + n, fn * X ^ n + gn * X ^ m, _⟩
[GOAL]
case refine_1.intro.intro.intro.intro
R : Type u_1
inst✝ : Semiring R
f g : R[T;T⁻¹]
m : ℕ
fn : R[X]
hf : ↑toLaurent fn = f * T ↑m
n : ℕ
gn : R[X]
hg : ↑toLaurent gn = g * T ↑n
⊢ ↑toLaurent (fn * X ^ n + gn * X ^ m) = (f + g) * T ↑(m + n)
[PROOFSTEP]
simp only [hf, hg, add_mul, add_comm (n : ℤ), map_add, map_mul, Polynomial.toLaurent_X_pow, mul_T_assoc, Int.ofNat_add]
[GOAL]
case refine_2
R : Type u_1
inst✝ : Semiring R
n : ℤ
a : R
⊢ ∃ n_1 f', ↑toLaurent f' = ↑C a * T n * T ↑n_1
[PROOFSTEP]
cases' n with n n
[GOAL]
case refine_2.ofNat
R : Type u_1
inst✝ : Semiring R
a : R
n : ℕ
⊢ ∃ n_1 f', ↑toLaurent f' = ↑C a * T (Int.ofNat n) * T ↑n_1
[PROOFSTEP]
exact ⟨0, Polynomial.C a * X ^ n, by simp⟩
[GOAL]
R : Type u_1
inst✝ : Semiring R
a : R
n : ℕ
⊢ ↑toLaurent (↑Polynomial.C a * X ^ n) = ↑C a * T (Int.ofNat n) * T ↑0
[PROOFSTEP]
simp
[GOAL]
case refine_2.negSucc
R : Type u_1
inst✝ : Semiring R
a : R
n : ℕ
⊢ ∃ n_1 f', ↑toLaurent f' = ↑C a * T (Int.negSucc n) * T ↑n_1
[PROOFSTEP]
refine' ⟨n + 1, Polynomial.C a, _⟩
[GOAL]
case refine_2.negSucc
R : Type u_1
inst✝ : Semiring R
a : R
n : ℕ
⊢ ↑toLaurent (↑Polynomial.C a) = ↑C a * T (Int.negSucc n) * T ↑(n + 1)
[PROOFSTEP]
simp only [Int.negSucc_eq, Polynomial.toLaurent_C, Int.ofNat_succ, mul_T_assoc, add_left_neg, T_zero, mul_one]
[GOAL]
R : Type u_1
inst✝ : Semiring R
Q : R[T;T⁻¹] → Prop
f : R[T;T⁻¹]
Qf : ∀ {f : R[X]} {n : ℕ}, Q (↑toLaurent f * T (-↑n))
⊢ Q f
[PROOFSTEP]
rcases f.exists_T_pow with ⟨n, f', hf⟩
[GOAL]
case intro.intro
R : Type u_1
inst✝ : Semiring R
Q : R[T;T⁻¹] → Prop
f : R[T;T⁻¹]
Qf : ∀ {f : R[X]} {n : ℕ}, Q (↑toLaurent f * T (-↑n))
n : ℕ
f' : R[X]
hf : ↑toLaurent f' = f * T ↑n
⊢ Q f
[PROOFSTEP]
rw [← mul_one f, ← T_zero, ← Nat.cast_zero, ← Nat.sub_self n, Nat.cast_sub rfl.le, T_sub, ← mul_assoc, ← hf]
[GOAL]
case intro.intro
R : Type u_1
inst✝ : Semiring R
Q : R[T;T⁻¹] → Prop
f : R[T;T⁻¹]
Qf : ∀ {f : R[X]} {n : ℕ}, Q (↑toLaurent f * T (-↑n))
n : ℕ
f' : R[X]
hf : ↑toLaurent f' = f * T ↑n
⊢ Q (↑toLaurent f' * T (-↑n))
[PROOFSTEP]
exact Qf
[GOAL]
R : Type u_1
inst✝ : Semiring R
f : R[T;T⁻¹]
Q : R[T;T⁻¹] → Prop
Qf : ∀ (f : R[X]), Q (↑toLaurent f)
QT : ∀ (f : R[T;T⁻¹]), Q (f * T 1) → Q f
⊢ Q f
[PROOFSTEP]
induction' f using LaurentPolynomial.induction_on_mul_T with f n
[GOAL]
case Qf
R : Type u_1
inst✝ : Semiring R
Q : R[T;T⁻¹] → Prop
Qf : ∀ (f : R[X]), Q (↑toLaurent f)
QT : ∀ (f : R[T;T⁻¹]), Q (f * T 1) → Q f
f : R[X]
n : ℕ
⊢ Q (↑toLaurent f * T (-↑n))
[PROOFSTEP]
induction' n with n hn
[GOAL]
case Qf.zero
R : Type u_1
inst✝ : Semiring R
Q : R[T;T⁻¹] → Prop
Qf : ∀ (f : R[X]), Q (↑toLaurent f)
QT : ∀ (f : R[T;T⁻¹]), Q (f * T 1) → Q f
f : R[X]
⊢ Q (↑toLaurent f * T (-↑Nat.zero))
[PROOFSTEP]
simpa only [Nat.zero_eq, Nat.cast_zero, neg_zero, T_zero, mul_one] using Qf _
[GOAL]
case Qf.succ
R : Type u_1
inst✝ : Semiring R
Q : R[T;T⁻¹] → Prop
Qf : ∀ (f : R[X]), Q (↑toLaurent f)
QT : ∀ (f : R[T;T⁻¹]), Q (f * T 1) → Q f
f : R[X]
n : ℕ
hn : Q (↑toLaurent f * T (-↑n))
⊢ Q (↑toLaurent f * T (-↑(Nat.succ n)))
[PROOFSTEP]
convert QT _ _
[GOAL]
case Qf.succ.convert_2
R : Type u_1
inst✝ : Semiring R
Q : R[T;T⁻¹] → Prop
Qf : ∀ (f : R[X]), Q (↑toLaurent f)
QT : ∀ (f : R[T;T⁻¹]), Q (f * T 1) → Q f
f : R[X]
n : ℕ
hn : Q (↑toLaurent f * T (-↑n))
⊢ Q (↑toLaurent f * T (-↑(Nat.succ n)) * T 1)
[PROOFSTEP]
simpa using hn
[GOAL]
R : Type u_1
inst✝ : Semiring R
a : R
n : ℤ
⊢ (↑C a * T n).support ⊆ {n}
[PROOFSTEP]
rw [← single_eq_C_mul_T]
[GOAL]
R : Type u_1
inst✝ : Semiring R
a : R
n : ℤ
⊢ (Finsupp.single n a).support ⊆ {n}
[PROOFSTEP]
exact support_single_subset
[GOAL]
R : Type u_1
inst✝ : Semiring R
a : R
a0 : a ≠ 0
n : ℤ
⊢ (↑C a * T n).support = {n}
[PROOFSTEP]
rw [← single_eq_C_mul_T]
[GOAL]
R : Type u_1
inst✝ : Semiring R
a : R
a0 : a ≠ 0
n : ℤ
⊢ (Finsupp.single n a).support = {n}
[PROOFSTEP]
exact support_single_ne_zero _ a0
[GOAL]
R : Type u_1
inst✝ : Semiring R
f : R[X]
⊢ (↑toLaurent f).support = Finset.map Nat.castEmbedding (Polynomial.support f)
[PROOFSTEP]
generalize hd : f.support = s
[GOAL]
R : Type u_1
inst✝ : Semiring R
f : R[X]
s : Finset ℕ
hd : Polynomial.support f = s
⊢ (↑toLaurent f).support = Finset.map Nat.castEmbedding s
[PROOFSTEP]
revert f
[GOAL]
R : Type u_1
inst✝ : Semiring R
s : Finset ℕ
⊢ ∀ (f : R[X]), Polynomial.support f = s → (↑toLaurent f).support = Finset.map Nat.castEmbedding s
[PROOFSTEP]
refine' Finset.induction_on s _ _
[GOAL]
case refine'_1
R : Type u_1
inst✝ : Semiring R
s : Finset ℕ
⊢ ∀ (f : R[X]), Polynomial.support f = ∅ → (↑toLaurent f).support = Finset.map Nat.castEmbedding ∅
[PROOFSTEP]
clear s
[GOAL]
case refine'_2
R : Type u_1
inst✝ : Semiring R
s : Finset ℕ
⊢ ∀ ⦃a : ℕ⦄ {s : Finset ℕ},
    ¬a ∈ s →
      (∀ (f : R[X]), Polynomial.support f = s → (↑toLaurent f).support = Finset.map Nat.castEmbedding s) →
        ∀ (f : R[X]),
          Polynomial.support f = insert a s → (↑toLaurent f).support = Finset.map Nat.castEmbedding (insert a s)
[PROOFSTEP]
clear s
[GOAL]
case refine'_1
R : Type u_1
inst✝ : Semiring R
⊢ ∀ (f : R[X]), Polynomial.support f = ∅ → (↑toLaurent f).support = Finset.map Nat.castEmbedding ∅
[PROOFSTEP]
simp (config := { contextual := true }) only [Polynomial.support_eq_empty, map_zero, Finsupp.support_zero,
  eq_self_iff_true, imp_true_iff, Finset.map_empty, Finsupp.support_eq_empty]
[GOAL]
case refine'_2
R : Type u_1
inst✝ : Semiring R
⊢ ∀ ⦃a : ℕ⦄ {s : Finset ℕ},
    ¬a ∈ s →
      (∀ (f : R[X]), Polynomial.support f = s → (↑toLaurent f).support = Finset.map Nat.castEmbedding s) →
        ∀ (f : R[X]),
          Polynomial.support f = insert a s → (↑toLaurent f).support = Finset.map Nat.castEmbedding (insert a s)
[PROOFSTEP]
intro a s as hf f fs
[GOAL]
case refine'_2
R : Type u_1
inst✝ : Semiring R
a : ℕ
s : Finset ℕ
as : ¬a ∈ s
hf : ∀ (f : R[X]), Polynomial.support f = s → (↑toLaurent f).support = Finset.map Nat.castEmbedding s
f : R[X]
fs : Polynomial.support f = insert a s
⊢ (↑toLaurent f).support = Finset.map Nat.castEmbedding (insert a s)
[PROOFSTEP]
have : (erase a f).toLaurent.support = s.map Nat.castEmbedding :=
  by
  refine' hf (f.erase a) _
  simp only [fs, Finset.erase_eq_of_not_mem as, Polynomial.support_erase, Finset.erase_insert_eq_erase]
[GOAL]
R : Type u_1
inst✝ : Semiring R
a : ℕ
s : Finset ℕ
as : ¬a ∈ s
hf : ∀ (f : R[X]), Polynomial.support f = s → (↑toLaurent f).support = Finset.map Nat.castEmbedding s
f : R[X]
fs : Polynomial.support f = insert a s
⊢ (↑toLaurent (Polynomial.erase a f)).support = Finset.map Nat.castEmbedding s
[PROOFSTEP]
refine' hf (f.erase a) _
[GOAL]
R : Type u_1
inst✝ : Semiring R
a : ℕ
s : Finset ℕ
as : ¬a ∈ s
hf : ∀ (f : R[X]), Polynomial.support f = s → (↑toLaurent f).support = Finset.map Nat.castEmbedding s
f : R[X]
fs : Polynomial.support f = insert a s
⊢ Polynomial.support (Polynomial.erase a f) = s
[PROOFSTEP]
simp only [fs, Finset.erase_eq_of_not_mem as, Polynomial.support_erase, Finset.erase_insert_eq_erase]
[GOAL]
case refine'_2
R : Type u_1
inst✝ : Semiring R
a : ℕ
s : Finset ℕ
as : ¬a ∈ s
hf : ∀ (f : R[X]), Polynomial.support f = s → (↑toLaurent f).support = Finset.map Nat.castEmbedding s
f : R[X]
fs : Polynomial.support f = insert a s
this : (↑toLaurent (Polynomial.erase a f)).support = Finset.map Nat.castEmbedding s
⊢ (↑toLaurent f).support = Finset.map Nat.castEmbedding (insert a s)
[PROOFSTEP]
rw [← monomial_add_erase f a, Finset.map_insert, ← this, map_add, Polynomial.toLaurent_C_mul_T, support_add_eq,
  Finset.insert_eq]
[GOAL]
case refine'_2
R : Type u_1
inst✝ : Semiring R
a : ℕ
s : Finset ℕ
as : ¬a ∈ s
hf : ∀ (f : R[X]), Polynomial.support f = s → (↑toLaurent f).support = Finset.map Nat.castEmbedding s
f : R[X]
fs : Polynomial.support f = insert a s
this : (↑toLaurent (Polynomial.erase a f)).support = Finset.map Nat.castEmbedding s
⊢ (↑C (coeff f a) * T ↑a).support ∪ (↑toLaurent (Polynomial.erase a f)).support =
    {↑Nat.castEmbedding a} ∪ (↑toLaurent (Polynomial.erase a f)).support
[PROOFSTEP]
congr
[GOAL]
case refine'_2.e_a
R : Type u_1
inst✝ : Semiring R
a : ℕ
s : Finset ℕ
as : ¬a ∈ s
hf : ∀ (f : R[X]), Polynomial.support f = s → (↑toLaurent f).support = Finset.map Nat.castEmbedding s
f : R[X]
fs : Polynomial.support f = insert a s
this : (↑toLaurent (Polynomial.erase a f)).support = Finset.map Nat.castEmbedding s
⊢ (↑C (coeff f a) * T ↑a).support = {↑Nat.castEmbedding a}
[PROOFSTEP]
exact support_C_mul_T_of_ne_zero (Polynomial.mem_support_iff.mp (by simp [fs])) _
[GOAL]
R : Type u_1
inst✝ : Semiring R
a : ℕ
s : Finset ℕ
as : ¬a ∈ s
hf : ∀ (f : R[X]), Polynomial.support f = s → (↑toLaurent f).support = Finset.map Nat.castEmbedding s
f : R[X]
fs : Polynomial.support f = insert a s
this : (↑toLaurent (Polynomial.erase a f)).support = Finset.map Nat.castEmbedding s
⊢ a ∈ Polynomial.support f
[PROOFSTEP]
simp [fs]
[GOAL]
case refine'_2
R : Type u_1
inst✝ : Semiring R
a : ℕ
s : Finset ℕ
as : ¬a ∈ s
hf : ∀ (f : R[X]), Polynomial.support f = s → (↑toLaurent f).support = Finset.map Nat.castEmbedding s
f : R[X]
fs : Polynomial.support f = insert a s
this : (↑toLaurent (Polynomial.erase a f)).support = Finset.map Nat.castEmbedding s
⊢ Disjoint (↑C (coeff f a) * T ↑a).support (↑toLaurent (Polynomial.erase a f)).support
[PROOFSTEP]
rw [this]
[GOAL]
case refine'_2
R : Type u_1
inst✝ : Semiring R
a : ℕ
s : Finset ℕ
as : ¬a ∈ s
hf : ∀ (f : R[X]), Polynomial.support f = s → (↑toLaurent f).support = Finset.map Nat.castEmbedding s
f : R[X]
fs : Polynomial.support f = insert a s
this : (↑toLaurent (Polynomial.erase a f)).support = Finset.map Nat.castEmbedding s
⊢ Disjoint (↑C (coeff f a) * T ↑a).support (Finset.map Nat.castEmbedding s)
[PROOFSTEP]
exact Disjoint.mono_left (support_C_mul_T _ _) (by simpa)
[GOAL]
R : Type u_1
inst✝ : Semiring R
a : ℕ
s : Finset ℕ
as : ¬a ∈ s
hf : ∀ (f : R[X]), Polynomial.support f = s → (↑toLaurent f).support = Finset.map Nat.castEmbedding s
f : R[X]
fs : Polynomial.support f = insert a s
this : (↑toLaurent (Polynomial.erase a f)).support = Finset.map Nat.castEmbedding s
⊢ Disjoint {↑a} (Finset.map Nat.castEmbedding s)
[PROOFSTEP]
simpa
[GOAL]
R : Type u_1
inst✝ : Semiring R
f : R[T;T⁻¹]
⊢ degree f = ⊥ ↔ f = 0
[PROOFSTEP]
refine' ⟨fun h => _, fun h => by rw [h, degree_zero]⟩
[GOAL]
R : Type u_1
inst✝ : Semiring R
f : R[T;T⁻¹]
h : f = 0
⊢ degree f = ⊥
[PROOFSTEP]
rw [h, degree_zero]
[GOAL]
R : Type u_1
inst✝ : Semiring R
f : R[T;T⁻¹]
h : degree f = ⊥
⊢ f = 0
[PROOFSTEP]
rw [degree, Finset.max_eq_sup_withBot] at h
[GOAL]
R : Type u_1
inst✝ : Semiring R
f : R[T;T⁻¹]
h : Finset.sup f.support WithBot.some = ⊥
⊢ f = 0
[PROOFSTEP]
ext n
[GOAL]
case h
R : Type u_1
inst✝ : Semiring R
f : R[T;T⁻¹]
h : Finset.sup f.support WithBot.some = ⊥
n : ℤ
⊢ ↑f n = ↑0 n
[PROOFSTEP]
refine' not_not.mp fun f0 => _
[GOAL]
case h
R : Type u_1
inst✝ : Semiring R
f : R[T;T⁻¹]
h : Finset.sup f.support WithBot.some = ⊥
n : ℤ
f0 : ¬↑f n = ↑0 n
⊢ False
[PROOFSTEP]
simp_rw [Finset.sup_eq_bot_iff, Finsupp.mem_support_iff, Ne.def, WithBot.coe_ne_bot] at h
[GOAL]
case h
R : Type u_1
inst✝ : Semiring R
f : R[T;T⁻¹]
n : ℤ
f0 : ¬↑f n = ↑0 n
h : ∀ (s : ℤ), ¬↑f s = 0 → False
⊢ False
[PROOFSTEP]
exact h n f0
[GOAL]
R : Type u_1
inst✝ : Semiring R
n : ℤ
a : R
a0 : a ≠ 0
⊢ degree (↑C a * T n) = ↑n
[PROOFSTEP]
rw [degree]
  -- Porting note: was `convert Finset.max_singleton`
[GOAL]
R : Type u_1
inst✝ : Semiring R
n : ℤ
a : R
a0 : a ≠ 0
⊢ Finset.max (↑C a * T n).support = ↑n
[PROOFSTEP]
have : Finsupp.support (C a * T n) = { n } :=
  by
  refine' support_eq_singleton.mpr _
  rw [← single_eq_C_mul_T]
  simp only [single_eq_same, a0, Ne.def, not_false_iff, eq_self_iff_true, and_self_iff]
[GOAL]
R : Type u_1
inst✝ : Semiring R
n : ℤ
a : R
a0 : a ≠ 0
⊢ (↑C a * T n).support = {n}
[PROOFSTEP]
refine' support_eq_singleton.mpr _
[GOAL]
R : Type u_1
inst✝ : Semiring R
n : ℤ
a : R
a0 : a ≠ 0
⊢ ↑(↑C a * T n) n ≠ 0 ∧ ↑C a * T n = Finsupp.single n (↑(↑C a * T n) n)
[PROOFSTEP]
rw [← single_eq_C_mul_T]
[GOAL]
R : Type u_1
inst✝ : Semiring R
n : ℤ
a : R
a0 : a ≠ 0
⊢ ↑(Finsupp.single n a) n ≠ 0 ∧ Finsupp.single n a = Finsupp.single n (↑(Finsupp.single n a) n)
[PROOFSTEP]
simp only [single_eq_same, a0, Ne.def, not_false_iff, eq_self_iff_true, and_self_iff]
[GOAL]
R : Type u_1
inst✝ : Semiring R
n : ℤ
a : R
a0 : a ≠ 0
this : (↑C a * T n).support = {n}
⊢ Finset.max (↑C a * T n).support = ↑n
[PROOFSTEP]
rw [this]
[GOAL]
R : Type u_1
inst✝ : Semiring R
n : ℤ
a : R
a0 : a ≠ 0
this : (↑C a * T n).support = {n}
⊢ Finset.max {n} = ↑n
[PROOFSTEP]
exact Finset.max_singleton
[GOAL]
R : Type u_1
inst✝ : Semiring R
n : ℤ
a : R
⊢ degree (↑C a * T n) = if a = 0 then ⊥ else ↑n
[PROOFSTEP]
split_ifs with h
[GOAL]
case pos
R : Type u_1
inst✝ : Semiring R
n : ℤ
a : R
h : a = 0
⊢ degree (↑C a * T n) = ⊥
[PROOFSTEP]
simp only [h, map_zero, zero_mul, degree_zero, degree_C_mul_T, Ne.def, not_false_iff]
[GOAL]
case neg
R : Type u_1
inst✝ : Semiring R
n : ℤ
a : R
h : ¬a = 0
⊢ degree (↑C a * T n) = ↑n
[PROOFSTEP]
simp only [h, map_zero, zero_mul, degree_zero, degree_C_mul_T, Ne.def, not_false_iff]
[GOAL]
R : Type u_1
inst✝¹ : Semiring R
inst✝ : Nontrivial R
n : ℤ
⊢ degree (T n) = ↑n
[PROOFSTEP]
rw [← one_mul (T n), ← map_one C]
[GOAL]
R : Type u_1
inst✝¹ : Semiring R
inst✝ : Nontrivial R
n : ℤ
⊢ degree (↑C 1 * T n) = ↑n
[PROOFSTEP]
exact degree_C_mul_T n 1 (one_ne_zero : (1 : R) ≠ 0)
[GOAL]
R : Type u_1
inst✝ : Semiring R
a : R
a0 : a ≠ 0
⊢ degree (↑C a) = 0
[PROOFSTEP]
rw [← mul_one (C a), ← T_zero]
[GOAL]
R : Type u_1
inst✝ : Semiring R
a : R
a0 : a ≠ 0
⊢ degree (↑C a * T 0) = 0
[PROOFSTEP]
exact degree_C_mul_T 0 a a0
[GOAL]
R : Type u_1
inst✝ : Semiring R
a : R
⊢ degree (↑C a) = if a = 0 then ⊥ else 0
[PROOFSTEP]
split_ifs with h
[GOAL]
case pos
R : Type u_1
inst✝ : Semiring R
a : R
h : a = 0
⊢ degree (↑C a) = ⊥
[PROOFSTEP]
simp only [h, map_zero, degree_zero, degree_C, Ne.def, not_false_iff]
[GOAL]
case neg
R : Type u_1
inst✝ : Semiring R
a : R
h : ¬a = 0
⊢ degree (↑C a) = 0
[PROOFSTEP]
simp only [h, map_zero, degree_zero, degree_C, Ne.def, not_false_iff]
[GOAL]
R : Type u_1
inst✝ : Semiring R
n : ℤ
a : R
⊢ degree (↑C a * T n) ≤ ↑n
[PROOFSTEP]
by_cases a0 : a = 0
[GOAL]
case pos
R : Type u_1
inst✝ : Semiring R
n : ℤ
a : R
a0 : a = 0
⊢ degree (↑C a * T n) ≤ ↑n
[PROOFSTEP]
simp only [a0, map_zero, zero_mul, degree_zero, bot_le]
[GOAL]
case neg
R : Type u_1
inst✝ : Semiring R
n : ℤ
a : R
a0 : ¬a = 0
⊢ degree (↑C a * T n) ≤ ↑n
[PROOFSTEP]
exact (degree_C_mul_T n a a0).le
[GOAL]
R : Type u_1
inst✝ : Semiring R
n : ℤ
⊢ degree (T n) = degree (↑C 1 * T n)
[PROOFSTEP]
rw [map_one, one_mul]
[GOAL]
R : Type u_1
inst✝ : Semiring R
a : R
⊢ degree (↑C a) = degree (↑C a * T 0)
[PROOFSTEP]
rw [T_zero, mul_one]
[GOAL]
R✝ : Type u_1
inst✝¹ : Semiring R✝
R : Type u_2
inst✝ : Semiring R
x y : R[X]
z : R[T;T⁻¹]
⊢ (x • y) • z = x • y • z
[PROOFSTEP]
simp only [(· • ·), SMul.smul, SMul.comp.smul, map_mul, mul_assoc]
[GOAL]
R✝ : Type u_1
inst✝¹ : CommSemiring R✝
R : Type u_2
inst✝ : CommSemiring R
src✝ : R[X] →+* R[T;T⁻¹] := toLaurent
f : R[X]
l : (fun x => R[T;T⁻¹]) f
⊢ ↑{ toMonoidHom := ↑src✝, map_zero' := (_ : OneHom.toFun (↑↑src✝) 0 = 0),
            map_add' :=
              (_ : ∀ (x y : R[X]), OneHom.toFun (↑↑src✝) (x + y) = OneHom.toFun (↑↑src✝) x + OneHom.toFun (↑↑src✝) y) }
        f *
      l =
    l *
      ↑{ toMonoidHom := ↑src✝, map_zero' := (_ : OneHom.toFun (↑↑src✝) 0 = 0),
            map_add' :=
              (_ : ∀ (x y : R[X]), OneHom.toFun (↑↑src✝) (x + y) = OneHom.toFun (↑↑src✝) x + OneHom.toFun (↑↑src✝) y) }
        f
[PROOFSTEP]
simp [mul_comm]
[GOAL]
R : Type u_1
inst✝ : CommSemiring R
t : { x // x ∈ Submonoid.closure {X} }
⊢ IsUnit (↑(algebraMap R[X] R[T;T⁻¹]) ↑t)
[PROOFSTEP]
cases' t with t ht
[GOAL]
case mk
R : Type u_1
inst✝ : CommSemiring R
t : R[X]
ht : t ∈ Submonoid.closure {X}
⊢ IsUnit (↑(algebraMap R[X] R[T;T⁻¹]) ↑{ val := t, property := ht })
[PROOFSTEP]
rcases Submonoid.mem_closure_singleton.mp ht with ⟨n, rfl⟩
[GOAL]
case mk.intro
R : Type u_1
inst✝ : CommSemiring R
n : ℕ
ht : X ^ n ∈ Submonoid.closure {X}
⊢ IsUnit (↑(algebraMap R[X] R[T;T⁻¹]) ↑{ val := X ^ n, property := ht })
[PROOFSTEP]
simp only [isUnit_T n, algebraMap_eq_toLaurent, Polynomial.toLaurent_X_pow]
[GOAL]
R : Type u_1
inst✝ : CommSemiring R
f : R[T;T⁻¹]
⊢ ∃ x, f * ↑(algebraMap R[X] R[T;T⁻¹]) ↑x.snd = ↑(algebraMap R[X] R[T;T⁻¹]) x.fst
[PROOFSTEP]
induction' f using LaurentPolynomial.induction_on_mul_T with f n
[GOAL]
case Qf
R : Type u_1
inst✝ : CommSemiring R
f : R[X]
n : ℕ
⊢ ∃ x, ↑toLaurent f * T (-↑n) * ↑(algebraMap R[X] R[T;T⁻¹]) ↑x.snd = ↑(algebraMap R[X] R[T;T⁻¹]) x.fst
[PROOFSTEP]
have := (Submonoid.closure ({ X } : Set R[X])).pow_mem Submonoid.mem_closure_singleton_self n
[GOAL]
case Qf
R : Type u_1
inst✝ : CommSemiring R
f : R[X]
n : ℕ
this : X ^ n ∈ Submonoid.closure {X}
⊢ ∃ x, ↑toLaurent f * T (-↑n) * ↑(algebraMap R[X] R[T;T⁻¹]) ↑x.snd = ↑(algebraMap R[X] R[T;T⁻¹]) x.fst
[PROOFSTEP]
refine' ⟨(f, ⟨_, this⟩), _⟩
[GOAL]
case Qf
R : Type u_1
inst✝ : CommSemiring R
f : R[X]
n : ℕ
this : X ^ n ∈ Submonoid.closure {X}
⊢ ↑toLaurent f * T (-↑n) * ↑(algebraMap R[X] R[T;T⁻¹]) ↑(f, { val := X ^ n, property := this }).snd =
    ↑(algebraMap R[X] R[T;T⁻¹]) (f, { val := X ^ n, property := this }).fst
[PROOFSTEP]
simp only [algebraMap_eq_toLaurent, Polynomial.toLaurent_X_pow, mul_T_assoc, add_left_neg, T_zero, mul_one]
[GOAL]
R : Type u_1
inst✝ : CommSemiring R
f g : R[X]
⊢ ↑(algebraMap R[X] R[T;T⁻¹]) f = ↑(algebraMap R[X] R[T;T⁻¹]) g ↔ ∃ c, ↑c * f = ↑c * g
[PROOFSTEP]
rw [algebraMap_eq_toLaurent, algebraMap_eq_toLaurent, Polynomial.toLaurent_inj]
[GOAL]
R : Type u_1
inst✝ : CommSemiring R
f g : R[X]
⊢ f = g ↔ ∃ c, ↑c * f = ↑c * g
[PROOFSTEP]
refine' ⟨_, _⟩
[GOAL]
case refine'_1
R : Type u_1
inst✝ : CommSemiring R
f g : R[X]
⊢ f = g → ∃ c, ↑c * f = ↑c * g
[PROOFSTEP]
rintro rfl
[GOAL]
case refine'_1
R : Type u_1
inst✝ : CommSemiring R
f : R[X]
⊢ ∃ c, ↑c * f = ↑c * f
[PROOFSTEP]
exact ⟨1, rfl⟩
[GOAL]
case refine'_2
R : Type u_1
inst✝ : CommSemiring R
f g : R[X]
⊢ (∃ c, ↑c * f = ↑c * g) → f = g
[PROOFSTEP]
rintro ⟨⟨h, hX⟩, h⟩
[GOAL]
case refine'_2.intro.mk
R : Type u_1
inst✝ : CommSemiring R
f g h✝ : R[X]
hX : h✝ ∈ Submonoid.closure {X}
h : ↑{ val := h✝, property := hX } * f = ↑{ val := h✝, property := hX } * g
⊢ f = g
[PROOFSTEP]
rcases Submonoid.mem_closure_singleton.mp hX with ⟨n, rfl⟩
[GOAL]
case refine'_2.intro.mk.intro
R : Type u_1
inst✝ : CommSemiring R
f g : R[X]
n : ℕ
hX : X ^ n ∈ Submonoid.closure {X}
h : ↑{ val := X ^ n, property := hX } * f = ↑{ val := X ^ n, property := hX } * g
⊢ f = g
[PROOFSTEP]
exact (isRegular_X_pow n).left h


[GOAL]
α : Type u_1
β : Type u_2
ι : Type u_3
a : α
n : ℕ
⊢ ↑toMultiset (single a n) = n • {a}
[PROOFSTEP]
rw [toMultiset_apply, sum_single_index]
[GOAL]
α : Type u_1
β : Type u_2
ι : Type u_3
a : α
n : ℕ
⊢ 0 • {a} = 0
[PROOFSTEP]
apply zero_nsmul
[GOAL]
α : Type u_1
β : Type u_2
ι : Type u_3
s : Finset ι
n : ℕ
⊢ ↑toMultiset (∑ i in s, single i n) = n • s.val
[PROOFSTEP]
simp_rw [toMultiset_sum, Finsupp.toMultiset_single, sum_nsmul, sum_multiset_singleton]
[GOAL]
α : Type u_1
β : Type u_2
ι : Type u_3
f : α →₀ ℕ
⊢ ↑Multiset.card (↑toMultiset f) = sum f fun x => id
[PROOFSTEP]
simp [toMultiset_apply, map_finsupp_sum, Function.id_def]
[GOAL]
α : Type u_1
β : Type u_2
ι : Type u_3
f : α →₀ ℕ
g : α → β
⊢ Multiset.map g (↑toMultiset f) = ↑toMultiset (mapDomain g f)
[PROOFSTEP]
refine' f.induction _ _
[GOAL]
case refine'_1
α : Type u_1
β : Type u_2
ι : Type u_3
f : α →₀ ℕ
g : α → β
⊢ Multiset.map g (↑toMultiset 0) = ↑toMultiset (mapDomain g 0)
[PROOFSTEP]
rw [toMultiset_zero, Multiset.map_zero, mapDomain_zero, toMultiset_zero]
[GOAL]
case refine'_2
α : Type u_1
β : Type u_2
ι : Type u_3
f : α →₀ ℕ
g : α → β
⊢ ∀ (a : α) (b : ℕ) (f : α →₀ ℕ),
    ¬a ∈ f.support →
      b ≠ 0 →
        Multiset.map g (↑toMultiset f) = ↑toMultiset (mapDomain g f) →
          Multiset.map g (↑toMultiset (single a b + f)) = ↑toMultiset (mapDomain g (single a b + f))
[PROOFSTEP]
intro a n f _ _ ih
[GOAL]
case refine'_2
α : Type u_1
β : Type u_2
ι : Type u_3
f✝ : α →₀ ℕ
g : α → β
a : α
n : ℕ
f : α →₀ ℕ
a✝¹ : ¬a ∈ f.support
a✝ : n ≠ 0
ih : Multiset.map g (↑toMultiset f) = ↑toMultiset (mapDomain g f)
⊢ Multiset.map g (↑toMultiset (single a n + f)) = ↑toMultiset (mapDomain g (single a n + f))
[PROOFSTEP]
rw [toMultiset_add, Multiset.map_add, ih, mapDomain_add, mapDomain_single, toMultiset_single, toMultiset_add,
  toMultiset_single, ← Multiset.coe_mapAddMonoidHom, (Multiset.mapAddMonoidHom g).map_nsmul]
[GOAL]
case refine'_2
α : Type u_1
β : Type u_2
ι : Type u_3
f✝ : α →₀ ℕ
g : α → β
a : α
n : ℕ
f : α →₀ ℕ
a✝¹ : ¬a ∈ f.support
a✝ : n ≠ 0
ih : Multiset.map g (↑toMultiset f) = ↑toMultiset (mapDomain g f)
⊢ n • ↑(Multiset.mapAddMonoidHom g) {a} + ↑toMultiset (mapDomain g f) = n • {g a} + ↑toMultiset (mapDomain g f)
[PROOFSTEP]
rfl
[GOAL]
α : Type u_1
β : Type u_2
ι : Type u_3
inst✝ : CommMonoid α
f : α →₀ ℕ
⊢ Multiset.prod (↑toMultiset f) = prod f fun a n => a ^ n
[PROOFSTEP]
refine' f.induction _ _
[GOAL]
case refine'_1
α : Type u_1
β : Type u_2
ι : Type u_3
inst✝ : CommMonoid α
f : α →₀ ℕ
⊢ Multiset.prod (↑toMultiset 0) = prod 0 fun a n => a ^ n
[PROOFSTEP]
rw [toMultiset_zero, Multiset.prod_zero, Finsupp.prod_zero_index]
[GOAL]
case refine'_2
α : Type u_1
β : Type u_2
ι : Type u_3
inst✝ : CommMonoid α
f : α →₀ ℕ
⊢ ∀ (a : α) (b : ℕ) (f : α →₀ ℕ),
    ¬a ∈ f.support →
      b ≠ 0 →
        (Multiset.prod (↑toMultiset f) = prod f fun a n => a ^ n) →
          Multiset.prod (↑toMultiset (single a b + f)) = prod (single a b + f) fun a n => a ^ n
[PROOFSTEP]
intro a n f _ _ ih
[GOAL]
case refine'_2
α : Type u_1
β : Type u_2
ι : Type u_3
inst✝ : CommMonoid α
f✝ : α →₀ ℕ
a : α
n : ℕ
f : α →₀ ℕ
a✝¹ : ¬a ∈ f.support
a✝ : n ≠ 0
ih : Multiset.prod (↑toMultiset f) = prod f fun a n => a ^ n
⊢ Multiset.prod (↑toMultiset (single a n + f)) = prod (single a n + f) fun a n => a ^ n
[PROOFSTEP]
rw [toMultiset_add, Multiset.prod_add, ih, toMultiset_single, Multiset.prod_nsmul,
  Finsupp.prod_add_index' pow_zero pow_add, Finsupp.prod_single_index, Multiset.prod_singleton]
[GOAL]
case refine'_2
α : Type u_1
β : Type u_2
ι : Type u_3
inst✝ : CommMonoid α
f✝ : α →₀ ℕ
a : α
n : ℕ
f : α →₀ ℕ
a✝¹ : ¬a ∈ f.support
a✝ : n ≠ 0
ih : Multiset.prod (↑toMultiset f) = prod f fun a n => a ^ n
⊢ a ^ 0 = 1
[PROOFSTEP]
exact pow_zero a
[GOAL]
α : Type u_1
β : Type u_2
ι : Type u_3
inst✝ : DecidableEq α
f : α →₀ ℕ
⊢ Multiset.toFinset (↑toMultiset f) = f.support
[PROOFSTEP]
refine' f.induction _ _
[GOAL]
case refine'_1
α : Type u_1
β : Type u_2
ι : Type u_3
inst✝ : DecidableEq α
f : α →₀ ℕ
⊢ Multiset.toFinset (↑toMultiset 0) = 0.support
[PROOFSTEP]
rw [toMultiset_zero, Multiset.toFinset_zero, support_zero]
[GOAL]
case refine'_2
α : Type u_1
β : Type u_2
ι : Type u_3
inst✝ : DecidableEq α
f : α →₀ ℕ
⊢ ∀ (a : α) (b : ℕ) (f : α →₀ ℕ),
    ¬a ∈ f.support →
      b ≠ 0 →
        Multiset.toFinset (↑toMultiset f) = f.support →
          Multiset.toFinset (↑toMultiset (single a b + f)) = (single a b + f).support
[PROOFSTEP]
intro a n f ha hn ih
[GOAL]
case refine'_2
α : Type u_1
β : Type u_2
ι : Type u_3
inst✝ : DecidableEq α
f✝ : α →₀ ℕ
a : α
n : ℕ
f : α →₀ ℕ
ha : ¬a ∈ f.support
hn : n ≠ 0
ih : Multiset.toFinset (↑toMultiset f) = f.support
⊢ Multiset.toFinset (↑toMultiset (single a n + f)) = (single a n + f).support
[PROOFSTEP]
rw [toMultiset_add, Multiset.toFinset_add, ih, toMultiset_single, support_add_eq, support_single_ne_zero _ hn,
  Multiset.toFinset_nsmul _ _ hn, Multiset.toFinset_singleton]
[GOAL]
case refine'_2
α : Type u_1
β : Type u_2
ι : Type u_3
inst✝ : DecidableEq α
f✝ : α →₀ ℕ
a : α
n : ℕ
f : α →₀ ℕ
ha : ¬a ∈ f.support
hn : n ≠ 0
ih : Multiset.toFinset (↑toMultiset f) = f.support
⊢ Disjoint (single a n).support f.support
[PROOFSTEP]
refine' Disjoint.mono_left support_single_subset _
[GOAL]
case refine'_2
α : Type u_1
β : Type u_2
ι : Type u_3
inst✝ : DecidableEq α
f✝ : α →₀ ℕ
a : α
n : ℕ
f : α →₀ ℕ
ha : ¬a ∈ f.support
hn : n ≠ 0
ih : Multiset.toFinset (↑toMultiset f) = f.support
⊢ Disjoint {a} f.support
[PROOFSTEP]
rwa [Finset.disjoint_singleton_left]
[GOAL]
α : Type u_1
β : Type u_2
ι : Type u_3
inst✝ : DecidableEq α
f : α →₀ ℕ
a : α
⊢ Multiset.count a (↑toMultiset f) = sum f fun x n => Multiset.count a (n • {x})
[PROOFSTEP]
rw [toMultiset_apply]
[GOAL]
α : Type u_1
β : Type u_2
ι : Type u_3
inst✝ : DecidableEq α
f : α →₀ ℕ
a : α
⊢ Multiset.count a (sum f fun a n => n • {a}) = sum f fun x n => Multiset.count a (n • {x})
[PROOFSTEP]
exact map_sum (Multiset.countAddMonoidHom a) _ f.support
[GOAL]
α : Type u_1
β : Type u_2
ι : Type u_3
inst✝ : DecidableEq α
f : α →₀ ℕ
a : α
⊢ (sum f fun x n => Multiset.count a (n • {x})) = sum f fun x n => n * Multiset.count a {x}
[PROOFSTEP]
simp only [Multiset.count_nsmul]
[GOAL]
α : Type u_1
β : Type u_2
ι : Type u_3
inst✝ : DecidableEq α
f : α →₀ ℕ
a a' : α
x✝ : a' ∈ f.support
H : a' ≠ a
⊢ (fun x n => n * Multiset.count a {x}) a' (↑f a') = 0
[PROOFSTEP]
simp only [Multiset.count_singleton, if_false, H.symm, mul_zero]
[GOAL]
α : Type u_1
β : Type u_2
ι : Type u_3
inst✝ : DecidableEq α
f : α →₀ ℕ
a : α
H : ¬a ∈ f.support
⊢ (fun x n => n * Multiset.count a {x}) a (↑f a) = 0
[PROOFSTEP]
simp only [not_mem_support_iff.1 H, zero_mul]
[GOAL]
α : Type u_1
β : Type u_2
ι : Type u_3
inst✝ : DecidableEq α
f : α →₀ ℕ
a : α
⊢ ↑f a * Multiset.count a {a} = ↑f a
[PROOFSTEP]
rw [Multiset.count_singleton_self, mul_one]
[GOAL]
α : Type u_1
β : Type u_2
ι : Type u_3
f : α →₀ ℕ
i : α
⊢ i ∈ ↑toMultiset f ↔ i ∈ f.support
[PROOFSTEP]
classical rw [← Multiset.count_ne_zero, Finsupp.count_toMultiset, Finsupp.mem_support_iff]
[GOAL]
α : Type u_1
β : Type u_2
ι : Type u_3
f : α →₀ ℕ
i : α
⊢ i ∈ ↑toMultiset f ↔ i ∈ f.support
[PROOFSTEP]
rw [← Multiset.count_ne_zero, Finsupp.count_toMultiset, Finsupp.mem_support_iff]
[GOAL]
α : Type u_1
β : Type u_2
ι : Type u_3
inst✝ : DecidableEq α
s : Multiset α
a : α
⊢ a ∈ toFinset s ↔ (fun a => count a s) a ≠ 0
[PROOFSTEP]
simp
[GOAL]
α : Type u_1
β : Type u_2
ι : Type u_3
inst✝ : DecidableEq α
s : Multiset α
⊢ (fun f => ↑Finsupp.toMultiset f)
      ((fun s =>
          { support := toFinset s, toFun := fun a => count a s,
            mem_support_toFun := (_ : ∀ (a : α), a ∈ toFinset s ↔ ¬count a s = 0) })
        s) =
    s
[PROOFSTEP]
simp only [Finsupp.toMultiset_apply, Finsupp.sum, Finsupp.coe_mk, Multiset.toFinset_sum_count_nsmul_eq]
[GOAL]
α : Type u_1
β : Type u_2
ι : Type u_3
inst✝ : DecidableEq α
f : α →₀ ℕ
a : α
⊢ ↑((fun s =>
            { support := toFinset s, toFun := fun a => count a s,
              mem_support_toFun := (_ : ∀ (a : α), a ∈ toFinset s ↔ ¬count a s = 0) })
          ((fun f => ↑Finsupp.toMultiset f) f))
      a =
    ↑f a
[PROOFSTEP]
simp only [Finsupp.toMultiset_apply, Finsupp.sum, Multiset.count_sum', Multiset.count_singleton, mul_boole,
  Finsupp.coe_mk, Finsupp.mem_support_iff, Multiset.count_nsmul, Finset.sum_ite_eq, ite_not, ite_eq_right_iff]
[GOAL]
α : Type u_1
β : Type u_2
ι : Type u_3
inst✝ : DecidableEq α
f : α →₀ ℕ
a : α
⊢ ↑f a = 0 → 0 = ↑f a
[PROOFSTEP]
exact Eq.symm
[GOAL]
α : Type u_1
β : Type u_2
ι : Type u_3
inst✝ : DecidableEq α
a : α
⊢ ↑toFinsupp {a} = Finsupp.single a 1
[PROOFSTEP]
ext
[GOAL]
case h
α : Type u_1
β : Type u_2
ι : Type u_3
inst✝ : DecidableEq α
a a✝ : α
⊢ ↑(↑toFinsupp {a}) a✝ = ↑(Finsupp.single a 1) a✝
[PROOFSTEP]
rw [toFinsupp_apply, count_singleton, Finsupp.single_eq_pi_single, Pi.single_apply]
[GOAL]
α : Type u_1
β : Type u_2
ι : Type u_3
inst✝ : DecidableEq ι
f g : ι →₀ ℕ
⊢ ↑(AddEquiv.symm Multiset.toFinsupp).toEquiv f ≤ ↑(AddEquiv.symm Multiset.toFinsupp).toEquiv g ↔ f ≤ g
[PROOFSTEP]
simp [le_def, Multiset.le_iff_count]
[GOAL]
α : Type u_1
β : Type u_2
ι : Type u_3
⊢ StrictMono ↑toMultiset
[PROOFSTEP]
classical exact (@orderIsoMultiset ι _).strictMono
[GOAL]
α : Type u_1
β : Type u_2
ι : Type u_3
⊢ StrictMono ↑toMultiset
[PROOFSTEP]
exact (@orderIsoMultiset ι _).strictMono
[GOAL]
α : Type u_1
β : Type u_2
ι : Type u_3
m n : ι →₀ ℕ
h : m < n
⊢ (sum m fun x => id) < sum n fun x => id
[PROOFSTEP]
rw [← card_toMultiset, ← card_toMultiset]
[GOAL]
α : Type u_1
β : Type u_2
ι : Type u_3
m n : ι →₀ ℕ
h : m < n
⊢ ↑Multiset.card (↑toMultiset m) < ↑Multiset.card (↑toMultiset n)
[PROOFSTEP]
apply Multiset.card_lt_of_lt
[GOAL]
case h
α : Type u_1
β : Type u_2
ι : Type u_3
m n : ι →₀ ℕ
h : m < n
⊢ ↑toMultiset m < ↑toMultiset n
[PROOFSTEP]
exact toMultiset_strictMono h


[GOAL]
α : Type u_1
β : Type u_2
f : α → β
⊢ classes (ker f) ⊆ Set.range fun y => {x | f x = y}
[PROOFSTEP]
rintro s ⟨x, rfl⟩
[GOAL]
case intro
α : Type u_1
β : Type u_2
f : α → β
x : α
⊢ {x_1 | Rel (ker f) x_1 x} ∈ Set.range fun y => {x | f x = y}
[PROOFSTEP]
rw [Set.mem_range]
[GOAL]
case intro
α : Type u_1
β : Type u_2
f : α → β
x : α
⊢ ∃ y, {x | f x = y} = {x_1 | Rel (ker f) x_1 x}
[PROOFSTEP]
exact ⟨f x, rfl⟩
[GOAL]
α✝ : Type u_1
α : Type u_2
β : Type u_3
inst✝¹ : Fintype β
f : α → β
inst✝ : Fintype ↑(classes (ker f))
⊢ Fintype.card ↑(classes (ker f)) ≤ Fintype.card β
[PROOFSTEP]
classical exact le_trans (Set.card_le_of_subset (classes_ker_subset_fiber_set f)) (Fintype.card_range_le _)
[GOAL]
α✝ : Type u_1
α : Type u_2
β : Type u_3
inst✝¹ : Fintype β
f : α → β
inst✝ : Fintype ↑(classes (ker f))
⊢ Fintype.card ↑(classes (ker f)) ≤ Fintype.card β
[PROOFSTEP]
exact le_trans (Set.card_le_of_subset (classes_ker_subset_fiber_set f)) (Fintype.card_range_le _)
[GOAL]
α : Type u_1
r : Setoid α
x y : α
x✝ : ∃ c, c ∈ classes r ∧ x ∈ c ∧ y ∈ c
c : Set α
z : α
hz : c = {x | Rel r x z}
hx : x ∈ c
hy : y ∈ c
⊢ Rel r x y
[PROOFSTEP]
subst c
[GOAL]
α : Type u_1
r : Setoid α
x y : α
x✝ : ∃ c, c ∈ classes r ∧ x ∈ c ∧ y ∈ c
z : α
hx : x ∈ {x | Rel r x z}
hy : y ∈ {x | Rel r x z}
⊢ Rel r x y
[PROOFSTEP]
exact r.trans' hx (r.symm' hy)
[GOAL]
α : Type u_1
r₁ r₂ : Setoid α
h : classes r₁ = classes r₂
a b : α
⊢ Rel r₁ a b ↔ Rel r₂ a b
[PROOFSTEP]
simp only [rel_iff_exists_classes, exists_prop, h]
[GOAL]
α : Type u_1
r : Setoid α
a : α
⊢ ∀ (y : Set α), y ∈ classes r → a ∈ y → y = {x | Rel r x a}
[PROOFSTEP]
rintro _ ⟨y, rfl⟩ ha
[GOAL]
case intro
α : Type u_1
r : Setoid α
a y : α
ha : a ∈ {x | Rel r x y}
⊢ {x | Rel r x y} = {x | Rel r x a}
[PROOFSTEP]
ext x
[GOAL]
case intro.h
α : Type u_1
r : Setoid α
a y : α
ha : a ∈ {x | Rel r x y}
x : α
⊢ x ∈ {x | Rel r x y} ↔ x ∈ {x | Rel r x a}
[PROOFSTEP]
exact ⟨fun hx => r.trans' hx (r.symm' ha), fun hx => r.trans' hx ha⟩
[GOAL]
α : Type u_1
c : Set (Set α)
H : ∀ (a : α), ∃! b x, a ∈ b
x : α
⊢ {y | Rel (mkClasses c H) x y} ∈ c
[PROOFSTEP]
convert @Setoid.eqv_class_mem _ _ H x using 3
[GOAL]
case h.e'_4.h.e'_2.h.a
α : Type u_1
c : Set (Set α)
H : ∀ (a : α), ∃! b x, a ∈ b
x x✝ : α
⊢ Rel (mkClasses c H) x x✝ ↔ Rel (mkClasses c H) x✝ x
[PROOFSTEP]
rw [Setoid.comm']
[GOAL]
α : Type u_1
c : Set (Set α)
hu : ⋃₀ c = Set.univ
H : Set.PairwiseDisjoint c id
a : α
⊢ a ∈ ⋃₀ c
[PROOFSTEP]
rw [hu]
[GOAL]
α : Type u_1
c : Set (Set α)
hu : ⋃₀ c = Set.univ
H : Set.PairwiseDisjoint c id
a : α
⊢ a ∈ Set.univ
[PROOFSTEP]
exact Set.mem_univ a
[GOAL]
α : Type u_1
c : Set (Set α)
hc : IsPartition c
x : α
t : Set α
ht : (fun b => ∃! x_1, x ∈ b) t ∧ ∀ (y : Set α), (fun b => ∃! x_1, x ∈ b) y → y = t
⊢ t ∈ c ∧ x ∈ t
[PROOFSTEP]
simp only [exists_unique_iff_exists] at ht
[GOAL]
α : Type u_1
c : Set (Set α)
hc : IsPartition c
x : α
t : Set α
ht : (∃ x_1, x ∈ t) ∧ ∀ (y : Set α), (∃ x_1, x ∈ y) → y = t
⊢ t ∈ c ∧ x ∈ t
[PROOFSTEP]
tauto
[GOAL]
α : Type u_1
c : Set (Set α)
hc : IsPartition c
s : Set α
x✝ : s ∈ classes (mkClasses c (_ : ∀ (a : α), ∃! b x, a ∈ b))
y : α
hs : s = {x | Rel (mkClasses c (_ : ∀ (a : α), ∃! b x, a ∈ b)) x y}
b : Set α
hm : b ∈ c
hb : y ∈ b
_hy : ∀ (y_1 : Set α), y_1 ∈ c → y ∈ y_1 → y_1 = b
⊢ s ∈ c
[PROOFSTEP]
rwa [show s = b from
    hs.symm ▸
      Set.ext fun x =>
        ⟨fun hx => symm' (mkClasses c hc.2) hx b hm hb, fun hx b' hc' hx' =>
          eq_of_mem_eqv_class hc.2 hm hx hc' hx' ▸ hb⟩]
[GOAL]
α : Type u_1
x y : Subtype IsPartition
hx : x ≤ y
hy : y ≤ x
⊢ x = y
[PROOFSTEP]
let h := @le_antisymm (Setoid α) _ _ _ hx hy
[GOAL]
α : Type u_1
x y : Subtype IsPartition
hx : x ≤ y
hy : y ≤ x
h : mkClasses ↑x (_ : ∀ (a : α), ∃! b x, a ∈ b) = mkClasses ↑y (_ : ∀ (a : α), ∃! b x, a ∈ b) := le_antisymm hx hy
⊢ x = y
[PROOFSTEP]
rw [Subtype.ext_iff_val, ← classes_mkClasses x.1 x.2, ← classes_mkClasses y.1 y.2, h]
[GOAL]
α : Type u_1
C : { C // IsPartition C }
⊢ (fun r => { val := classes r, property := (_ : ¬∅ ∈ classes r ∧ ∀ (a : α), ∃! b x, a ∈ b) })
      ((fun C => mkClasses ↑C (_ : ∀ (a : α), ∃! b x, a ∈ b)) C) =
    C
[PROOFSTEP]
rw [Subtype.ext_iff_val, ← classes_mkClasses C.1 C.2]
[GOAL]
α : Type u_1
r s : Setoid α
⊢ ↑{ toFun := fun r => { val := classes r, property := (_ : ¬∅ ∈ classes r ∧ ∀ (a : α), ∃! b x, a ∈ b) },
            invFun := fun C => mkClasses ↑C (_ : ∀ (a : α), ∃! b x, a ∈ b),
            left_inv := (_ : ∀ (r : Setoid α), mkClasses (classes r) (_ : ∀ (a : α), ∃! b x, a ∈ b) = r),
            right_inv :=
              (_ :
                ∀ (C : { C // IsPartition C }),
                  (fun r => { val := classes r, property := (_ : ¬∅ ∈ classes r ∧ ∀ (a : α), ∃! b x, a ∈ b) })
                      ((fun C => mkClasses ↑C (_ : ∀ (a : α), ∃! b x, a ∈ b)) C) =
                    C) }
        r ≤
      ↑{ toFun := fun r => { val := classes r, property := (_ : ¬∅ ∈ classes r ∧ ∀ (a : α), ∃! b x, a ∈ b) },
            invFun := fun C => mkClasses ↑C (_ : ∀ (a : α), ∃! b x, a ∈ b),
            left_inv := (_ : ∀ (r : Setoid α), mkClasses (classes r) (_ : ∀ (a : α), ∃! b x, a ∈ b) = r),
            right_inv :=
              (_ :
                ∀ (C : { C // IsPartition C }),
                  (fun r => { val := classes r, property := (_ : ¬∅ ∈ classes r ∧ ∀ (a : α), ∃! b x, a ∈ b) })
                      ((fun C => mkClasses ↑C (_ : ∀ (a : α), ∃! b x, a ∈ b)) C) =
                    C) }
        s ↔
    r ≤ s
[PROOFSTEP]
conv_rhs => rw [← mkClasses_classes r, ← mkClasses_classes s]
[GOAL]
α : Type u_1
r s : Setoid α
| r ≤ s
[PROOFSTEP]
rw [← mkClasses_classes r, ← mkClasses_classes s]
[GOAL]
α : Type u_1
r s : Setoid α
| r ≤ s
[PROOFSTEP]
rw [← mkClasses_classes r, ← mkClasses_classes s]
[GOAL]
α : Type u_1
r s : Setoid α
| r ≤ s
[PROOFSTEP]
rw [← mkClasses_classes r, ← mkClasses_classes s]
[GOAL]
ι : Type u_1
α : Type u_2
s : ι → Set α
hs : IndexedPartition s
⊢ ⋃ (i : ι), s i = univ
[PROOFSTEP]
ext x
[GOAL]
case h
ι : Type u_1
α : Type u_2
s : ι → Set α
hs : IndexedPartition s
x : α
⊢ x ∈ ⋃ (i : ι), s i ↔ x ∈ univ
[PROOFSTEP]
simp [hs.exists_mem x]
[GOAL]
ι : Type u_1
α : Type u_2
s : ι → Set α
hs : IndexedPartition s
x✝ : IndexedPartition.Quotient hs
x : α
⊢ proj hs ⁻¹' {Quotient.mk'' x} = s (↑(equivQuotient hs).symm (Quotient.mk'' x))
[PROOFSTEP]
ext y
[GOAL]
case h
ι : Type u_1
α : Type u_2
s : ι → Set α
hs : IndexedPartition s
x✝ : IndexedPartition.Quotient hs
x y : α
⊢ y ∈ proj hs ⁻¹' {Quotient.mk'' x} ↔ y ∈ s (↑(equivQuotient hs).symm (Quotient.mk'' x))
[PROOFSTEP]
simp only [Set.mem_preimage, Set.mem_singleton_iff, hs.mem_iff_index_eq]
[GOAL]
case h
ι : Type u_1
α : Type u_2
s : ι → Set α
hs : IndexedPartition s
x✝ : IndexedPartition.Quotient hs
x y : α
⊢ proj hs y = Quotient.mk'' x ↔ index hs y = ↑(equivQuotient hs).symm (Quotient.mk'' x)
[PROOFSTEP]
exact Quotient.eq''


[GOAL]
K : Type u_1
E : Type u_2
inst✝ : IsROrC K
⊢ Submodule.span ℝ ↑{1, I} = ⊤
[PROOFSTEP]
rw [eq_top_iff]
[GOAL]
K : Type u_1
E : Type u_2
inst✝ : IsROrC K
⊢ ⊤ ≤ Submodule.span ℝ ↑{1, I}
[PROOFSTEP]
intro a _
[GOAL]
K : Type u_1
E : Type u_2
inst✝ : IsROrC K
a : K
a✝ : a ∈ ⊤
⊢ a ∈ Submodule.span ℝ ↑{1, I}
[PROOFSTEP]
rw [Finset.coe_insert, Finset.coe_singleton, Submodule.mem_span_insert]
[GOAL]
K : Type u_1
E : Type u_2
inst✝ : IsROrC K
a : K
a✝ : a ∈ ⊤
⊢ ∃ a_1 z, z ∈ Submodule.span ℝ {I} ∧ a = a_1 • 1 + z
[PROOFSTEP]
refine' ⟨re a, im a • I, _, _⟩
[GOAL]
case refine'_1
K : Type u_1
E : Type u_2
inst✝ : IsROrC K
a : K
a✝ : a ∈ ⊤
⊢ ↑im a • I ∈ Submodule.span ℝ {I}
[PROOFSTEP]
rw [Submodule.mem_span_singleton]
[GOAL]
case refine'_1
K : Type u_1
E : Type u_2
inst✝ : IsROrC K
a : K
a✝ : a ∈ ⊤
⊢ ∃ a_1, a_1 • I = ↑im a • I
[PROOFSTEP]
use im a
[GOAL]
case refine'_2
K : Type u_1
E : Type u_2
inst✝ : IsROrC K
a : K
a✝ : a ∈ ⊤
⊢ a = ↑re a • 1 + ↑im a • I
[PROOFSTEP]
simp [re_add_im a, Algebra.smul_def, algebraMap_eq_ofReal]
[GOAL]
K : Type u_1
E : Type u_2
inst✝³ : IsROrC K
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace K E
inst✝ : FiniteDimensional K E
⊢ ProperSpace E
[PROOFSTEP]
letI : NormedSpace ℝ E := RestrictScalars.normedSpace ℝ K E
[GOAL]
K : Type u_1
E : Type u_2
inst✝³ : IsROrC K
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace K E
inst✝ : FiniteDimensional K E
this : NormedSpace ℝ E := RestrictScalars.normedSpace ℝ K E
⊢ ProperSpace E
[PROOFSTEP]
letI : FiniteDimensional ℝ E := FiniteDimensional.trans ℝ K E
[GOAL]
K : Type u_1
E : Type u_2
inst✝³ : IsROrC K
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace K E
inst✝ : FiniteDimensional K E
this✝ : NormedSpace ℝ E := RestrictScalars.normedSpace ℝ K E
this : FiniteDimensional ℝ E := trans ℝ K E
⊢ ProperSpace E
[PROOFSTEP]
infer_instance
[GOAL]
K : Type u_1
E : Type u_2
inst✝ : IsROrC K
⊢ ‖reClm‖ = 1
[PROOFSTEP]
apply le_antisymm (LinearMap.mkContinuous_norm_le _ zero_le_one _)
[GOAL]
K : Type u_1
E : Type u_2
inst✝ : IsROrC K
⊢ 1 ≤ ‖LinearMap.mkContinuous reLm 1 (_ : ∀ (x : K), ‖↑reLm x‖ ≤ 1 * ‖x‖)‖
[PROOFSTEP]
convert ContinuousLinearMap.ratio_le_op_norm (reClm : K →L[ℝ] ℝ) (1 : K)
[GOAL]
case h.e'_3
K : Type u_1
E : Type u_2
inst✝ : IsROrC K
⊢ 1 = ‖↑reClm 1‖ / ‖1‖
[PROOFSTEP]
simp


[GOAL]
α : Type u_1
β : Type u_2
s : Set (Setoid α)
⊢ Rel (sInf s) = sInf (Rel '' s)
[PROOFSTEP]
ext
[GOAL]
case h.h.a
α : Type u_1
β : Type u_2
s : Set (Setoid α)
x✝¹ x✝ : α
⊢ Rel (sInf s) x✝¹ x✝ ↔ sInf (Rel '' s) x✝¹ x✝
[PROOFSTEP]
simp only [sInf_image, iInf_apply, iInf_Prop_eq]
[GOAL]
case h.h.a
α : Type u_1
β : Type u_2
s : Set (Setoid α)
x✝¹ x✝ : α
⊢ Rel (sInf s) x✝¹ x✝ ↔ ∀ (i : Setoid α), i ∈ s → Rel i x✝¹ x✝
[PROOFSTEP]
rfl
[GOAL]
α : Type u_1
β : Type u_2
s : Setoid α
⊢ s = ⊤ ↔ ∀ (x y : α), Rel s x y
[PROOFSTEP]
rw [_root_.eq_top_iff, Setoid.le_def, Setoid.top_def]
[GOAL]
α : Type u_1
β : Type u_2
s : Setoid α
⊢ (∀ {x y : α}, ⊤ x y → Rel s x y) ↔ ∀ (x y : α), Rel s x y
[PROOFSTEP]
simp only [Pi.top_apply, Prop.top_eq_true, forall_true_left]
[GOAL]
α : Type u_1
β : Type u_2
r s : Setoid α
⊢ r ⊔ s = EqvGen.Setoid fun x y => Rel r x y ∨ Rel s x y
[PROOFSTEP]
rw [eqvGen_eq]
[GOAL]
α : Type u_1
β : Type u_2
r s : Setoid α
⊢ r ⊔ s = sInf {s_1 | ∀ ⦃x y : α⦄, Rel r x y ∨ Rel s x y → Rel s_1 x y}
[PROOFSTEP]
apply congr_arg sInf
[GOAL]
α : Type u_1
β : Type u_2
r s : Setoid α
⊢ {x | r ≤ x ∧ s ≤ x} = {s_1 | ∀ ⦃x y : α⦄, Rel r x y ∨ Rel s x y → Rel s_1 x y}
[PROOFSTEP]
simp only [le_def, or_imp, ← forall_and]
[GOAL]
α : Type u_1
β : Type u_2
r s : Setoid α
⊢ r ⊔ s = EqvGen.Setoid (Rel r ⊔ Rel s)
[PROOFSTEP]
rw [sup_eq_eqvGen]
[GOAL]
α : Type u_1
β : Type u_2
r s : Setoid α
⊢ (EqvGen.Setoid fun x y => Rel r x y ∨ Rel s x y) = EqvGen.Setoid (Rel r ⊔ Rel s)
[PROOFSTEP]
rfl
[GOAL]
α : Type u_1
β : Type u_2
S : Set (Setoid α)
⊢ sSup S = EqvGen.Setoid fun x y => ∃ r, r ∈ S ∧ Rel r x y
[PROOFSTEP]
rw [eqvGen_eq]
[GOAL]
α : Type u_1
β : Type u_2
S : Set (Setoid α)
⊢ sSup S = sInf {s | ∀ ⦃x y : α⦄, (∃ r, r ∈ S ∧ Rel r x y) → Rel s x y}
[PROOFSTEP]
apply congr_arg sInf
[GOAL]
α : Type u_1
β : Type u_2
S : Set (Setoid α)
⊢ upperBounds S = {s | ∀ ⦃x y : α⦄, (∃ r, r ∈ S ∧ Rel r x y) → Rel s x y}
[PROOFSTEP]
simp only [upperBounds, le_def, and_imp, exists_imp]
[GOAL]
α : Type u_1
β : Type u_2
S : Set (Setoid α)
⊢ {x | ∀ ⦃a : Setoid α⦄, a ∈ S → ∀ {x_1 y : α}, Rel a x_1 y → Rel x x_1 y} =
    {s | ∀ ⦃x y : α⦄ (x_1 : Setoid α), x_1 ∈ S → Rel x_1 x y → Rel s x y}
[PROOFSTEP]
ext
[GOAL]
case h
α : Type u_1
β : Type u_2
S : Set (Setoid α)
x✝ : Setoid α
⊢ x✝ ∈ {x | ∀ ⦃a : Setoid α⦄, a ∈ S → ∀ {x_1 y : α}, Rel a x_1 y → Rel x x_1 y} ↔
    x✝ ∈ {s | ∀ ⦃x y : α⦄ (x_1 : Setoid α), x_1 ∈ S → Rel x_1 x y → Rel s x y}
[PROOFSTEP]
exact ⟨fun H x y r hr => H hr, fun H r hr x y => H r hr⟩
[GOAL]
α : Type u_1
β : Type u_2
s : Set (Setoid α)
⊢ sSup s = EqvGen.Setoid (sSup (Rel '' s))
[PROOFSTEP]
rw [sSup_eq_eqvGen, sSup_image]
[GOAL]
α : Type u_1
β : Type u_2
s : Set (Setoid α)
⊢ (EqvGen.Setoid fun x y => ∃ r, r ∈ s ∧ Rel r x y) = EqvGen.Setoid (⨆ (a : Setoid α) (_ : a ∈ s), Rel a)
[PROOFSTEP]
congr with (x y)
[GOAL]
case e_r.h.h.a
α : Type u_1
β : Type u_2
s : Set (Setoid α)
x y : α
⊢ (∃ r, r ∈ s ∧ Rel r x y) ↔ iSup (fun a => ⨆ (_ : a ∈ s), Rel a) x y
[PROOFSTEP]
simp only [iSup_apply, iSup_Prop_eq, exists_prop]
[GOAL]
α : Type u_1
β : Type u_2
r : Setoid α
⊢ EqvGen.Setoid Setoid.r ≤ r
[PROOFSTEP]
rw [eqvGen_eq]
[GOAL]
α : Type u_1
β : Type u_2
r : Setoid α
⊢ sInf {s | ∀ ⦃x y : α⦄, Setoid.r x y → Rel s x y} ≤ r
[PROOFSTEP]
exact sInf_le fun _ _ => id
[GOAL]
α : Type u_1
β : Type u_2
r : α → α → Prop
s : Setoid α
h : ∀ (x y : α), r x y → Rel s x y
⊢ EqvGen.Setoid r ≤ s
[PROOFSTEP]
rw [eqvGen_eq]
[GOAL]
α : Type u_1
β : Type u_2
r : α → α → Prop
s : Setoid α
h : ∀ (x y : α), r x y → Rel s x y
⊢ sInf {s | ∀ ⦃x y : α⦄, r x y → Rel s x y} ≤ s
[PROOFSTEP]
exact sInf_le h
[GOAL]
α : Type u_1
β : Type u_2
r : Setoid α
f : Quotient r → β
x y : α
h : Rel r x y
⊢ Rel (ker (f ∘ Quotient.mk'')) x y
[PROOFSTEP]
simp [ker_def, Quotient.sound' h]
[GOAL]
α : Type u_1
β : Type u_2
r : Setoid α
f : α → β
H : r ≤ ker f
g : Quotient r → β
Hg : f = g ∘ Quotient.mk''
⊢ Quotient.lift f H = g
[PROOFSTEP]
ext ⟨x⟩
[GOAL]
case h.mk
α : Type u_1
β : Type u_2
r : Setoid α
f : α → β
H : r ≤ ker f
g : Quotient r → β
Hg : f = g ∘ Quotient.mk''
x✝ : Quotient r
x : α
⊢ Quotient.lift f H (Quot.mk Setoid.r x) = g (Quot.mk Setoid.r x)
[PROOFSTEP]
erw [Quotient.lift_mk f H, Hg]
[GOAL]
case h.mk
α : Type u_1
β : Type u_2
r : Setoid α
f : α → β
H : r ≤ ker f
g : Quotient r → β
Hg : f = g ∘ Quotient.mk''
x✝ : Quotient r
x : α
⊢ (g ∘ Quotient.mk'') x = g (Quot.mk Setoid.r x)
[PROOFSTEP]
rfl
[GOAL]
α : Type u_1
β : Type u_2
r : Setoid α
f : α → β
x y : Quotient (ker f)
h :
  Quotient.lift (fun x => { val := f x, property := (_ : f x ∈ Set.range f) })
      (_ :
        ∀ (x x_1 : α),
          x ≈ x_1 →
            { val := f x, property := (_ : f x ∈ Set.range f) } =
              { val := f x_1, property := (_ : f x_1 ∈ Set.range f) })
      x =
    Quotient.lift (fun x => { val := f x, property := (_ : f x ∈ Set.range f) })
      (_ :
        ∀ (x x_1 : α),
          x ≈ x_1 →
            { val := f x, property := (_ : f x ∈ Set.range f) } =
              { val := f x_1, property := (_ : f x_1 ∈ Set.range f) })
      y
⊢ Quotient.lift f (_ : ∀ (x x_1 : α), x ≈ x_1 → x ≈ x_1) x = Quotient.lift f (_ : ∀ (x x_1 : α), x ≈ x_1 → x ≈ x_1) y
[PROOFSTEP]
rcases x with ⟨⟩
[GOAL]
case mk
α : Type u_1
β : Type u_2
r : Setoid α
f : α → β
x y : Quotient (ker f)
a✝ : α
h :
  Quotient.lift (fun x => { val := f x, property := (_ : f x ∈ Set.range f) })
      (_ :
        ∀ (x x_1 : α),
          x ≈ x_1 →
            { val := f x, property := (_ : f x ∈ Set.range f) } =
              { val := f x_1, property := (_ : f x_1 ∈ Set.range f) })
      (Quot.mk Setoid.r a✝) =
    Quotient.lift (fun x => { val := f x, property := (_ : f x ∈ Set.range f) })
      (_ :
        ∀ (x x_1 : α),
          x ≈ x_1 →
            { val := f x, property := (_ : f x ∈ Set.range f) } =
              { val := f x_1, property := (_ : f x_1 ∈ Set.range f) })
      y
⊢ Quotient.lift f (_ : ∀ (x x_1 : α), x ≈ x_1 → x ≈ x_1) (Quot.mk Setoid.r a✝) =
    Quotient.lift f (_ : ∀ (x x_1 : α), x ≈ x_1 → x ≈ x_1) y
[PROOFSTEP]
rcases y with ⟨⟩
[GOAL]
case mk.mk
α : Type u_1
β : Type u_2
r : Setoid α
f : α → β
x y : Quotient (ker f)
a✝¹ a✝ : α
h :
  Quotient.lift (fun x => { val := f x, property := (_ : f x ∈ Set.range f) })
      (_ :
        ∀ (x x_1 : α),
          x ≈ x_1 →
            { val := f x, property := (_ : f x ∈ Set.range f) } =
              { val := f x_1, property := (_ : f x_1 ∈ Set.range f) })
      (Quot.mk Setoid.r a✝¹) =
    Quotient.lift (fun x => { val := f x, property := (_ : f x ∈ Set.range f) })
      (_ :
        ∀ (x x_1 : α),
          x ≈ x_1 →
            { val := f x, property := (_ : f x ∈ Set.range f) } =
              { val := f x_1, property := (_ : f x_1 ∈ Set.range f) })
      (Quot.mk Setoid.r a✝)
⊢ Quotient.lift f (_ : ∀ (x x_1 : α), x ≈ x_1 → x ≈ x_1) (Quot.mk Setoid.r a✝¹) =
    Quotient.lift f (_ : ∀ (x x_1 : α), x ≈ x_1 → x ≈ x_1) (Quot.mk Setoid.r a✝)
[PROOFSTEP]
injections
[GOAL]
α : Type u_1
β : Type u_2
r✝ : Setoid α
f✝ : α → β
r : Setoid α
f : α → β
h : ker f ≤ r
hf : Surjective f
x✝² y✝ z✝ : β
x✝¹ : ∃ a b, f a = x✝² ∧ f b = y✝ ∧ Rel r a b
x✝ : ∃ a b, f a = y✝ ∧ f b = z✝ ∧ Rel r a b
x y : α
hx : f x = x✝²
hy : f y = y✝
h₁ : Rel r x y
y' z : α
hy' : f y' = y✝
hz : f z = z✝
h₂ : Rel r y' z
⊢ Rel (ker f) y y'
[PROOFSTEP]
rwa [← hy'] at hy
[GOAL]
α : Type u_1
β : Type u_2
r : Setoid α
f : α → β
h : ker f ≤ r
hf : Surjective f
⊢ map r f = mapOfSurjective r f h hf
[PROOFSTEP]
rw [← eqvGen_of_setoid (mapOfSurjective r f h hf)]
[GOAL]
α : Type u_1
β : Type u_2
r : Setoid α
f : α → β
h : ker f ≤ r
hf : Surjective f
⊢ map r f = EqvGen.Setoid Setoid.r
[PROOFSTEP]
rfl
[GOAL]
α : Type u_1
β : Type u_2
r✝ : Setoid α
f✝ f : α → β
r : Setoid β
x y : α
⊢ Setoid.r x y ↔ Quotient.mk r (f x) = Quotient.mk r (f y)
[PROOFSTEP]
rw [Quotient.eq]
[GOAL]
α : Type u_1
β : Type u_2
r✝ : Setoid α
f✝ f : α → β
r : Setoid β
x y : α
⊢ Setoid.r x y ↔ f x ≈ f y
[PROOFSTEP]
rfl
[GOAL]
α : Type u_1
β : Type u_2
r : Setoid α
f : α → β
s : Setoid α
h : r ≤ s
x : Quotient (ker (Quot.mapRight h))
y : Quot fun a₁ a₂ => Rel r a₁ a₂
w : α
⊢ (fun x =>
        Quotient.liftOn' x (fun w => Quotient.mk'' (Quotient.mk'' w))
          (_ : ∀ (x y : α), Setoid.r x y → Quotient.mk'' (Quotient.mk'' x) = Quotient.mk'' (Quotient.mk'' y)))
      ((fun x =>
          Quotient.liftOn' x
            (fun w =>
              Quotient.liftOn' w Quotient.mk'' (_ : ∀ (x y : α), Setoid.r x y → Quotient.mk s x = Quotient.mk s y))
            (_ :
              ∀ (x y : Quot fun a₁ a₂ => Rel r a₁ a₂),
                Setoid.r x y →
                  Quotient.liftOn' x Quotient.mk'' (_ : ∀ (x y : α), Setoid.r x y → Quotient.mk s x = Quotient.mk s y) =
                    Quotient.liftOn' y Quotient.mk''
                      (_ : ∀ (x y : α), Setoid.r x y → Quotient.mk s x = Quotient.mk s y)))
        (Quotient.mk'' (Quotient.mk'' w))) =
    Quotient.mk'' (Quotient.mk'' w)
[PROOFSTEP]
show ⟦_⟧ = _
[GOAL]
α : Type u_1
β : Type u_2
r : Setoid α
f : α → β
s : Setoid α
h : r ≤ s
x : Quotient (ker (Quot.mapRight h))
y : Quot fun a₁ a₂ => Rel r a₁ a₂
w : α
⊢ Quotient.mk (ker (Quot.mapRight h)) (Quotient.mk'' w) = Quotient.mk'' (Quotient.mk'' w)
[PROOFSTEP]
rfl
[GOAL]
α : Type u_1
β : Type u_2
r : Setoid α
f : α → β
s : Setoid α
h : r ≤ s
x : Quotient s
y : α
⊢ (fun x =>
        Quotient.liftOn' x
          (fun w =>
            Quotient.liftOn' w Quotient.mk'' (_ : ∀ (x y : α), Setoid.r x y → Quotient.mk s x = Quotient.mk s y))
          (_ :
            ∀ (x y : Quot fun a₁ a₂ => Rel r a₁ a₂),
              Setoid.r x y →
                Quotient.liftOn' x Quotient.mk'' (_ : ∀ (x y : α), Setoid.r x y → Quotient.mk s x = Quotient.mk s y) =
                  Quotient.liftOn' y Quotient.mk'' (_ : ∀ (x y : α), Setoid.r x y → Quotient.mk s x = Quotient.mk s y)))
      ((fun x =>
          Quotient.liftOn' x (fun w => Quotient.mk'' (Quotient.mk'' w))
            (_ : ∀ (x y : α), Setoid.r x y → Quotient.mk'' (Quotient.mk'' x) = Quotient.mk'' (Quotient.mk'' y)))
        (Quotient.mk'' y)) =
    Quotient.mk'' y
[PROOFSTEP]
show ⟦_⟧ = _
[GOAL]
α : Type u_1
β : Type u_2
r : Setoid α
f : α → β
s : Setoid α
h : r ≤ s
x : Quotient s
y : α
⊢ Quotient.mk s y = Quotient.mk'' y
[PROOFSTEP]
rfl
[GOAL]
α : Type u_1
β : Type u_2
r✝ : Setoid α
f : α → β
r : Setoid α
s : Setoid (Quotient r)
x y : α
h : Rel r x y
⊢ Rel (comap Quotient.mk' s) x y
[PROOFSTEP]
rw [comap_rel, eq_rel.2 h]
[GOAL]
α : Type u_1
β : Type u_2
r✝ : Setoid α
f : α → β
r : Setoid α
s : { s // r ≤ s }
⊢ (fun s => { val := comap Quotient.mk' s, property := (_ : ∀ (x y : α), Rel r x y → Rel (comap Quotient.mk' s) x y) })
      ((fun s =>
          mapOfSurjective (↑s) Quotient.mk'' (_ : ker Quotient.mk'' ≤ ↑s)
            (_ : ∀ (q : Quotient r), ∃ a, Quotient.mk r a = q))
        s) =
    s
[PROOFSTEP]
ext
[GOAL]
case a.H
α : Type u_1
β : Type u_2
r✝ : Setoid α
f : α → β
r : Setoid α
s : { s // r ≤ s }
a✝ b✝ : α
⊢ Rel
      (↑((fun s =>
            { val := comap Quotient.mk' s, property := (_ : ∀ (x y : α), Rel r x y → Rel (comap Quotient.mk' s) x y) })
          ((fun s =>
              mapOfSurjective (↑s) Quotient.mk'' (_ : ker Quotient.mk'' ≤ ↑s)
                (_ : ∀ (q : Quotient r), ∃ a, Quotient.mk r a = q))
            s)))
      a✝ b✝ ↔
    Rel (↑s) a✝ b✝
[PROOFSTEP]
refine ⟨?_, fun h => ⟨_, _, rfl, rfl, h⟩⟩
[GOAL]
case a.H
α : Type u_1
β : Type u_2
r✝ : Setoid α
f : α → β
r : Setoid α
s : { s // r ≤ s }
a✝ b✝ : α
⊢ Rel
      (↑((fun s =>
            { val := comap Quotient.mk' s, property := (_ : ∀ (x y : α), Rel r x y → Rel (comap Quotient.mk' s) x y) })
          ((fun s =>
              mapOfSurjective (↑s) Quotient.mk'' (_ : ker Quotient.mk'' ≤ ↑s)
                (_ : ∀ (q : Quotient r), ∃ a, Quotient.mk r a = q))
            s)))
      a✝ b✝ →
    Rel (↑s) a✝ b✝
[PROOFSTEP]
intro ⟨a, b, hx, hy, H⟩
[GOAL]
case a.H
α : Type u_1
β : Type u_2
r✝ : Setoid α
f : α → β
r : Setoid α
s : { s // r ≤ s }
a✝ b✝ a b : α
hx : Quotient.mk'' a = Quotient.mk' a✝
hy : Quotient.mk'' b = Quotient.mk' b✝
H : Rel (↑s) a b
⊢ Rel (↑s) a✝ b✝
[PROOFSTEP]
refine s.1.trans' (s.1.symm' <| s.2 <| eq_rel.1 hx) (s.1.trans' H <| s.2 <| (eq_rel.1 hy))
[GOAL]
α : Type u_1
β : Type u_2
r✝ : Setoid α
f : α → β
r : Setoid α
⊢ ∀ {a b : { s // r ≤ s }},
    ↑{
              toFun := fun s =>
                mapOfSurjective (↑s) Quotient.mk'' (_ : ker Quotient.mk'' ≤ ↑s)
                  (_ : ∀ (q : Quotient r), ∃ a, Quotient.mk r a = q),
              invFun := fun s =>
                { val := comap Quotient.mk' s,
                  property := (_ : ∀ (x y : α), Rel r x y → Rel (comap Quotient.mk' s) x y) },
              left_inv :=
                (_ :
                  ∀ (s : { s // r ≤ s }),
                    (fun s =>
                          { val := comap Quotient.mk' s,
                            property := (_ : ∀ (x y : α), Rel r x y → Rel (comap Quotient.mk' s) x y) })
                        ((fun s =>
                            mapOfSurjective (↑s) Quotient.mk'' (_ : ker Quotient.mk'' ≤ ↑s)
                              (_ : ∀ (q : Quotient r), ∃ a, Quotient.mk r a = q))
                          s) =
                      s),
              right_inv :=
                (_ :
                  ∀ (s : Setoid (Quotient r)),
                    (fun s =>
                          mapOfSurjective (↑s) Quotient.mk'' (_ : ker Quotient.mk'' ≤ ↑s)
                            (_ : ∀ (q : Quotient r), ∃ a, Quotient.mk r a = q))
                        ((fun s =>
                            { val := comap Quotient.mk' s,
                              property := (_ : ∀ (x y : α), Rel r x y → Rel (comap Quotient.mk' s) x y) })
                          s) =
                      s) }
          a ≤
        ↑{
              toFun := fun s =>
                mapOfSurjective (↑s) Quotient.mk'' (_ : ker Quotient.mk'' ≤ ↑s)
                  (_ : ∀ (q : Quotient r), ∃ a, Quotient.mk r a = q),
              invFun := fun s =>
                { val := comap Quotient.mk' s,
                  property := (_ : ∀ (x y : α), Rel r x y → Rel (comap Quotient.mk' s) x y) },
              left_inv :=
                (_ :
                  ∀ (s : { s // r ≤ s }),
                    (fun s =>
                          { val := comap Quotient.mk' s,
                            property := (_ : ∀ (x y : α), Rel r x y → Rel (comap Quotient.mk' s) x y) })
                        ((fun s =>
                            mapOfSurjective (↑s) Quotient.mk'' (_ : ker Quotient.mk'' ≤ ↑s)
                              (_ : ∀ (q : Quotient r), ∃ a, Quotient.mk r a = q))
                          s) =
                      s),
              right_inv :=
                (_ :
                  ∀ (s : Setoid (Quotient r)),
                    (fun s =>
                          mapOfSurjective (↑s) Quotient.mk'' (_ : ker Quotient.mk'' ≤ ↑s)
                            (_ : ∀ (q : Quotient r), ∃ a, Quotient.mk r a = q))
                        ((fun s =>
                            { val := comap Quotient.mk' s,
                              property := (_ : ∀ (x y : α), Rel r x y → Rel (comap Quotient.mk' s) x y) })
                          s) =
                      s) }
          b ↔
      a ≤ b
[PROOFSTEP]
intro s t
[GOAL]
α : Type u_1
β : Type u_2
r✝ : Setoid α
f : α → β
r : Setoid α
s t : { s // r ≤ s }
⊢ ↑{
            toFun := fun s =>
              mapOfSurjective (↑s) Quotient.mk'' (_ : ker Quotient.mk'' ≤ ↑s)
                (_ : ∀ (q : Quotient r), ∃ a, Quotient.mk r a = q),
            invFun := fun s =>
              { val := comap Quotient.mk' s,
                property := (_ : ∀ (x y : α), Rel r x y → Rel (comap Quotient.mk' s) x y) },
            left_inv :=
              (_ :
                ∀ (s : { s // r ≤ s }),
                  (fun s =>
                        { val := comap Quotient.mk' s,
                          property := (_ : ∀ (x y : α), Rel r x y → Rel (comap Quotient.mk' s) x y) })
                      ((fun s =>
                          mapOfSurjective (↑s) Quotient.mk'' (_ : ker Quotient.mk'' ≤ ↑s)
                            (_ : ∀ (q : Quotient r), ∃ a, Quotient.mk r a = q))
                        s) =
                    s),
            right_inv :=
              (_ :
                ∀ (s : Setoid (Quotient r)),
                  (fun s =>
                        mapOfSurjective (↑s) Quotient.mk'' (_ : ker Quotient.mk'' ≤ ↑s)
                          (_ : ∀ (q : Quotient r), ∃ a, Quotient.mk r a = q))
                      ((fun s =>
                          { val := comap Quotient.mk' s,
                            property := (_ : ∀ (x y : α), Rel r x y → Rel (comap Quotient.mk' s) x y) })
                        s) =
                    s) }
        s ≤
      ↑{
            toFun := fun s =>
              mapOfSurjective (↑s) Quotient.mk'' (_ : ker Quotient.mk'' ≤ ↑s)
                (_ : ∀ (q : Quotient r), ∃ a, Quotient.mk r a = q),
            invFun := fun s =>
              { val := comap Quotient.mk' s,
                property := (_ : ∀ (x y : α), Rel r x y → Rel (comap Quotient.mk' s) x y) },
            left_inv :=
              (_ :
                ∀ (s : { s // r ≤ s }),
                  (fun s =>
                        { val := comap Quotient.mk' s,
                          property := (_ : ∀ (x y : α), Rel r x y → Rel (comap Quotient.mk' s) x y) })
                      ((fun s =>
                          mapOfSurjective (↑s) Quotient.mk'' (_ : ker Quotient.mk'' ≤ ↑s)
                            (_ : ∀ (q : Quotient r), ∃ a, Quotient.mk r a = q))
                        s) =
                    s),
            right_inv :=
              (_ :
                ∀ (s : Setoid (Quotient r)),
                  (fun s =>
                        mapOfSurjective (↑s) Quotient.mk'' (_ : ker Quotient.mk'' ≤ ↑s)
                          (_ : ∀ (q : Quotient r), ∃ a, Quotient.mk r a = q))
                      ((fun s =>
                          { val := comap Quotient.mk' s,
                            property := (_ : ∀ (x y : α), Rel r x y → Rel (comap Quotient.mk' s) x y) })
                        s) =
                    s) }
        t ↔
    s ≤ t
[PROOFSTEP]
refine ⟨?_, ?_⟩
[GOAL]
case refine_1
α : Type u_1
β : Type u_2
r✝ : Setoid α
f : α → β
r : Setoid α
s t : { s // r ≤ s }
⊢ ↑{
            toFun := fun s =>
              mapOfSurjective (↑s) Quotient.mk'' (_ : ker Quotient.mk'' ≤ ↑s)
                (_ : ∀ (q : Quotient r), ∃ a, Quotient.mk r a = q),
            invFun := fun s =>
              { val := comap Quotient.mk' s,
                property := (_ : ∀ (x y : α), Rel r x y → Rel (comap Quotient.mk' s) x y) },
            left_inv :=
              (_ :
                ∀ (s : { s // r ≤ s }),
                  (fun s =>
                        { val := comap Quotient.mk' s,
                          property := (_ : ∀ (x y : α), Rel r x y → Rel (comap Quotient.mk' s) x y) })
                      ((fun s =>
                          mapOfSurjective (↑s) Quotient.mk'' (_ : ker Quotient.mk'' ≤ ↑s)
                            (_ : ∀ (q : Quotient r), ∃ a, Quotient.mk r a = q))
                        s) =
                    s),
            right_inv :=
              (_ :
                ∀ (s : Setoid (Quotient r)),
                  (fun s =>
                        mapOfSurjective (↑s) Quotient.mk'' (_ : ker Quotient.mk'' ≤ ↑s)
                          (_ : ∀ (q : Quotient r), ∃ a, Quotient.mk r a = q))
                      ((fun s =>
                          { val := comap Quotient.mk' s,
                            property := (_ : ∀ (x y : α), Rel r x y → Rel (comap Quotient.mk' s) x y) })
                        s) =
                    s) }
        s ≤
      ↑{
            toFun := fun s =>
              mapOfSurjective (↑s) Quotient.mk'' (_ : ker Quotient.mk'' ≤ ↑s)
                (_ : ∀ (q : Quotient r), ∃ a, Quotient.mk r a = q),
            invFun := fun s =>
              { val := comap Quotient.mk' s,
                property := (_ : ∀ (x y : α), Rel r x y → Rel (comap Quotient.mk' s) x y) },
            left_inv :=
              (_ :
                ∀ (s : { s // r ≤ s }),
                  (fun s =>
                        { val := comap Quotient.mk' s,
                          property := (_ : ∀ (x y : α), Rel r x y → Rel (comap Quotient.mk' s) x y) })
                      ((fun s =>
                          mapOfSurjective (↑s) Quotient.mk'' (_ : ker Quotient.mk'' ≤ ↑s)
                            (_ : ∀ (q : Quotient r), ∃ a, Quotient.mk r a = q))
                        s) =
                    s),
            right_inv :=
              (_ :
                ∀ (s : Setoid (Quotient r)),
                  (fun s =>
                        mapOfSurjective (↑s) Quotient.mk'' (_ : ker Quotient.mk'' ≤ ↑s)
                          (_ : ∀ (q : Quotient r), ∃ a, Quotient.mk r a = q))
                      ((fun s =>
                          { val := comap Quotient.mk' s,
                            property := (_ : ∀ (x y : α), Rel r x y → Rel (comap Quotient.mk' s) x y) })
                        s) =
                    s) }
        t →
    s ≤ t
[PROOFSTEP]
intro h x y hs
[GOAL]
case refine_1
α : Type u_1
β : Type u_2
r✝ : Setoid α
f : α → β
r : Setoid α
s t : { s // r ≤ s }
h :
  ↑{
          toFun := fun s =>
            mapOfSurjective (↑s) Quotient.mk'' (_ : ker Quotient.mk'' ≤ ↑s)
              (_ : ∀ (q : Quotient r), ∃ a, Quotient.mk r a = q),
          invFun := fun s =>
            { val := comap Quotient.mk' s, property := (_ : ∀ (x y : α), Rel r x y → Rel (comap Quotient.mk' s) x y) },
          left_inv :=
            (_ :
              ∀ (s : { s // r ≤ s }),
                (fun s =>
                      { val := comap Quotient.mk' s,
                        property := (_ : ∀ (x y : α), Rel r x y → Rel (comap Quotient.mk' s) x y) })
                    ((fun s =>
                        mapOfSurjective (↑s) Quotient.mk'' (_ : ker Quotient.mk'' ≤ ↑s)
                          (_ : ∀ (q : Quotient r), ∃ a, Quotient.mk r a = q))
                      s) =
                  s),
          right_inv :=
            (_ :
              ∀ (s : Setoid (Quotient r)),
                (fun s =>
                      mapOfSurjective (↑s) Quotient.mk'' (_ : ker Quotient.mk'' ≤ ↑s)
                        (_ : ∀ (q : Quotient r), ∃ a, Quotient.mk r a = q))
                    ((fun s =>
                        { val := comap Quotient.mk' s,
                          property := (_ : ∀ (x y : α), Rel r x y → Rel (comap Quotient.mk' s) x y) })
                      s) =
                  s) }
      s ≤
    ↑{
          toFun := fun s =>
            mapOfSurjective (↑s) Quotient.mk'' (_ : ker Quotient.mk'' ≤ ↑s)
              (_ : ∀ (q : Quotient r), ∃ a, Quotient.mk r a = q),
          invFun := fun s =>
            { val := comap Quotient.mk' s, property := (_ : ∀ (x y : α), Rel r x y → Rel (comap Quotient.mk' s) x y) },
          left_inv :=
            (_ :
              ∀ (s : { s // r ≤ s }),
                (fun s =>
                      { val := comap Quotient.mk' s,
                        property := (_ : ∀ (x y : α), Rel r x y → Rel (comap Quotient.mk' s) x y) })
                    ((fun s =>
                        mapOfSurjective (↑s) Quotient.mk'' (_ : ker Quotient.mk'' ≤ ↑s)
                          (_ : ∀ (q : Quotient r), ∃ a, Quotient.mk r a = q))
                      s) =
                  s),
          right_inv :=
            (_ :
              ∀ (s : Setoid (Quotient r)),
                (fun s =>
                      mapOfSurjective (↑s) Quotient.mk'' (_ : ker Quotient.mk'' ≤ ↑s)
                        (_ : ∀ (q : Quotient r), ∃ a, Quotient.mk r a = q))
                    ((fun s =>
                        { val := comap Quotient.mk' s,
                          property := (_ : ∀ (x y : α), Rel r x y → Rel (comap Quotient.mk' s) x y) })
                      s) =
                  s) }
      t
x y : α
hs : Rel (↑s) x y
⊢ Rel (↑t) x y
[PROOFSTEP]
let ⟨a, b, hx, hy, ht⟩ := h ⟨x, y, rfl, rfl, hs⟩
[GOAL]
case refine_1
α : Type u_1
β : Type u_2
r✝ : Setoid α
f : α → β
r : Setoid α
s t : { s // r ≤ s }
h :
  ↑{
          toFun := fun s =>
            mapOfSurjective (↑s) Quotient.mk'' (_ : ker Quotient.mk'' ≤ ↑s)
              (_ : ∀ (q : Quotient r), ∃ a, Quotient.mk r a = q),
          invFun := fun s =>
            { val := comap Quotient.mk' s, property := (_ : ∀ (x y : α), Rel r x y → Rel (comap Quotient.mk' s) x y) },
          left_inv :=
            (_ :
              ∀ (s : { s // r ≤ s }),
                (fun s =>
                      { val := comap Quotient.mk' s,
                        property := (_ : ∀ (x y : α), Rel r x y → Rel (comap Quotient.mk' s) x y) })
                    ((fun s =>
                        mapOfSurjective (↑s) Quotient.mk'' (_ : ker Quotient.mk'' ≤ ↑s)
                          (_ : ∀ (q : Quotient r), ∃ a, Quotient.mk r a = q))
                      s) =
                  s),
          right_inv :=
            (_ :
              ∀ (s : Setoid (Quotient r)),
                (fun s =>
                      mapOfSurjective (↑s) Quotient.mk'' (_ : ker Quotient.mk'' ≤ ↑s)
                        (_ : ∀ (q : Quotient r), ∃ a, Quotient.mk r a = q))
                    ((fun s =>
                        { val := comap Quotient.mk' s,
                          property := (_ : ∀ (x y : α), Rel r x y → Rel (comap Quotient.mk' s) x y) })
                      s) =
                  s) }
      s ≤
    ↑{
          toFun := fun s =>
            mapOfSurjective (↑s) Quotient.mk'' (_ : ker Quotient.mk'' ≤ ↑s)
              (_ : ∀ (q : Quotient r), ∃ a, Quotient.mk r a = q),
          invFun := fun s =>
            { val := comap Quotient.mk' s, property := (_ : ∀ (x y : α), Rel r x y → Rel (comap Quotient.mk' s) x y) },
          left_inv :=
            (_ :
              ∀ (s : { s // r ≤ s }),
                (fun s =>
                      { val := comap Quotient.mk' s,
                        property := (_ : ∀ (x y : α), Rel r x y → Rel (comap Quotient.mk' s) x y) })
                    ((fun s =>
                        mapOfSurjective (↑s) Quotient.mk'' (_ : ker Quotient.mk'' ≤ ↑s)
                          (_ : ∀ (q : Quotient r), ∃ a, Quotient.mk r a = q))
                      s) =
                  s),
          right_inv :=
            (_ :
              ∀ (s : Setoid (Quotient r)),
                (fun s =>
                      mapOfSurjective (↑s) Quotient.mk'' (_ : ker Quotient.mk'' ≤ ↑s)
                        (_ : ∀ (q : Quotient r), ∃ a, Quotient.mk r a = q))
                    ((fun s =>
                        { val := comap Quotient.mk' s,
                          property := (_ : ∀ (x y : α), Rel r x y → Rel (comap Quotient.mk' s) x y) })
                      s) =
                  s) }
      t
x y : α
hs : Rel (↑s) x y
a b : α
hx : Quotient.mk'' a = Quotient.mk'' x
hy : Quotient.mk'' b = Quotient.mk'' y
ht : Rel (↑t) a b
⊢ Rel (↑t) x y
[PROOFSTEP]
exact t.1.trans' (t.1.symm' <| t.2 <| eq_rel.1 hx) <| t.1.trans' ht <| t.2 <| eq_rel.1 hy
[GOAL]
case refine_2
α : Type u_1
β : Type u_2
r✝ : Setoid α
f : α → β
r : Setoid α
s t : { s // r ≤ s }
⊢ s ≤ t →
    ↑{
            toFun := fun s =>
              mapOfSurjective (↑s) Quotient.mk'' (_ : ker Quotient.mk'' ≤ ↑s)
                (_ : ∀ (q : Quotient r), ∃ a, Quotient.mk r a = q),
            invFun := fun s =>
              { val := comap Quotient.mk' s,
                property := (_ : ∀ (x y : α), Rel r x y → Rel (comap Quotient.mk' s) x y) },
            left_inv :=
              (_ :
                ∀ (s : { s // r ≤ s }),
                  (fun s =>
                        { val := comap Quotient.mk' s,
                          property := (_ : ∀ (x y : α), Rel r x y → Rel (comap Quotient.mk' s) x y) })
                      ((fun s =>
                          mapOfSurjective (↑s) Quotient.mk'' (_ : ker Quotient.mk'' ≤ ↑s)
                            (_ : ∀ (q : Quotient r), ∃ a, Quotient.mk r a = q))
                        s) =
                    s),
            right_inv :=
              (_ :
                ∀ (s : Setoid (Quotient r)),
                  (fun s =>
                        mapOfSurjective (↑s) Quotient.mk'' (_ : ker Quotient.mk'' ≤ ↑s)
                          (_ : ∀ (q : Quotient r), ∃ a, Quotient.mk r a = q))
                      ((fun s =>
                          { val := comap Quotient.mk' s,
                            property := (_ : ∀ (x y : α), Rel r x y → Rel (comap Quotient.mk' s) x y) })
                        s) =
                    s) }
        s ≤
      ↑{
            toFun := fun s =>
              mapOfSurjective (↑s) Quotient.mk'' (_ : ker Quotient.mk'' ≤ ↑s)
                (_ : ∀ (q : Quotient r), ∃ a, Quotient.mk r a = q),
            invFun := fun s =>
              { val := comap Quotient.mk' s,
                property := (_ : ∀ (x y : α), Rel r x y → Rel (comap Quotient.mk' s) x y) },
            left_inv :=
              (_ :
                ∀ (s : { s // r ≤ s }),
                  (fun s =>
                        { val := comap Quotient.mk' s,
                          property := (_ : ∀ (x y : α), Rel r x y → Rel (comap Quotient.mk' s) x y) })
                      ((fun s =>
                          mapOfSurjective (↑s) Quotient.mk'' (_ : ker Quotient.mk'' ≤ ↑s)
                            (_ : ∀ (q : Quotient r), ∃ a, Quotient.mk r a = q))
                        s) =
                    s),
            right_inv :=
              (_ :
                ∀ (s : Setoid (Quotient r)),
                  (fun s =>
                        mapOfSurjective (↑s) Quotient.mk'' (_ : ker Quotient.mk'' ≤ ↑s)
                          (_ : ∀ (q : Quotient r), ∃ a, Quotient.mk r a = q))
                      ((fun s =>
                          { val := comap Quotient.mk' s,
                            property := (_ : ∀ (x y : α), Rel r x y → Rel (comap Quotient.mk' s) x y) })
                        s) =
                    s) }
        t
[PROOFSTEP]
intro h x y hs
[GOAL]
case refine_2
α : Type u_1
β : Type u_2
r✝ : Setoid α
f : α → β
r : Setoid α
s t : { s // r ≤ s }
h : s ≤ t
x y : Quotient r
hs :
  Rel
    (↑{
          toFun := fun s =>
            mapOfSurjective (↑s) Quotient.mk'' (_ : ker Quotient.mk'' ≤ ↑s)
              (_ : ∀ (q : Quotient r), ∃ a, Quotient.mk r a = q),
          invFun := fun s =>
            { val := comap Quotient.mk' s, property := (_ : ∀ (x y : α), Rel r x y → Rel (comap Quotient.mk' s) x y) },
          left_inv :=
            (_ :
              ∀ (s : { s // r ≤ s }),
                (fun s =>
                      { val := comap Quotient.mk' s,
                        property := (_ : ∀ (x y : α), Rel r x y → Rel (comap Quotient.mk' s) x y) })
                    ((fun s =>
                        mapOfSurjective (↑s) Quotient.mk'' (_ : ker Quotient.mk'' ≤ ↑s)
                          (_ : ∀ (q : Quotient r), ∃ a, Quotient.mk r a = q))
                      s) =
                  s),
          right_inv :=
            (_ :
              ∀ (s : Setoid (Quotient r)),
                (fun s =>
                      mapOfSurjective (↑s) Quotient.mk'' (_ : ker Quotient.mk'' ≤ ↑s)
                        (_ : ∀ (q : Quotient r), ∃ a, Quotient.mk r a = q))
                    ((fun s =>
                        { val := comap Quotient.mk' s,
                          property := (_ : ∀ (x y : α), Rel r x y → Rel (comap Quotient.mk' s) x y) })
                      s) =
                  s) }
      s)
    x y
⊢ Rel
    (↑{
          toFun := fun s =>
            mapOfSurjective (↑s) Quotient.mk'' (_ : ker Quotient.mk'' ≤ ↑s)
              (_ : ∀ (q : Quotient r), ∃ a, Quotient.mk r a = q),
          invFun := fun s =>
            { val := comap Quotient.mk' s, property := (_ : ∀ (x y : α), Rel r x y → Rel (comap Quotient.mk' s) x y) },
          left_inv :=
            (_ :
              ∀ (s : { s // r ≤ s }),
                (fun s =>
                      { val := comap Quotient.mk' s,
                        property := (_ : ∀ (x y : α), Rel r x y → Rel (comap Quotient.mk' s) x y) })
                    ((fun s =>
                        mapOfSurjective (↑s) Quotient.mk'' (_ : ker Quotient.mk'' ≤ ↑s)
                          (_ : ∀ (q : Quotient r), ∃ a, Quotient.mk r a = q))
                      s) =
                  s),
          right_inv :=
            (_ :
              ∀ (s : Setoid (Quotient r)),
                (fun s =>
                      mapOfSurjective (↑s) Quotient.mk'' (_ : ker Quotient.mk'' ≤ ↑s)
                        (_ : ∀ (q : Quotient r), ∃ a, Quotient.mk r a = q))
                    ((fun s =>
                        { val := comap Quotient.mk' s,
                          property := (_ : ∀ (x y : α), Rel r x y → Rel (comap Quotient.mk' s) x y) })
                      s) =
                  s) }
      t)
    x y
[PROOFSTEP]
let ⟨a, b, hx, hy, Hs⟩ := hs
[GOAL]
case refine_2
α : Type u_1
β : Type u_2
r✝ : Setoid α
f : α → β
r : Setoid α
s t : { s // r ≤ s }
h : s ≤ t
x y : Quotient r
hs :
  Rel
    (↑{
          toFun := fun s =>
            mapOfSurjective (↑s) Quotient.mk'' (_ : ker Quotient.mk'' ≤ ↑s)
              (_ : ∀ (q : Quotient r), ∃ a, Quotient.mk r a = q),
          invFun := fun s =>
            { val := comap Quotient.mk' s, property := (_ : ∀ (x y : α), Rel r x y → Rel (comap Quotient.mk' s) x y) },
          left_inv :=
            (_ :
              ∀ (s : { s // r ≤ s }),
                (fun s =>
                      { val := comap Quotient.mk' s,
                        property := (_ : ∀ (x y : α), Rel r x y → Rel (comap Quotient.mk' s) x y) })
                    ((fun s =>
                        mapOfSurjective (↑s) Quotient.mk'' (_ : ker Quotient.mk'' ≤ ↑s)
                          (_ : ∀ (q : Quotient r), ∃ a, Quotient.mk r a = q))
                      s) =
                  s),
          right_inv :=
            (_ :
              ∀ (s : Setoid (Quotient r)),
                (fun s =>
                      mapOfSurjective (↑s) Quotient.mk'' (_ : ker Quotient.mk'' ≤ ↑s)
                        (_ : ∀ (q : Quotient r), ∃ a, Quotient.mk r a = q))
                    ((fun s =>
                        { val := comap Quotient.mk' s,
                          property := (_ : ∀ (x y : α), Rel r x y → Rel (comap Quotient.mk' s) x y) })
                      s) =
                  s) }
      s)
    x y
a b : α
hx : Quotient.mk'' a = x
hy : Quotient.mk'' b = y
Hs : Rel (↑s) a b
⊢ Rel
    (↑{
          toFun := fun s =>
            mapOfSurjective (↑s) Quotient.mk'' (_ : ker Quotient.mk'' ≤ ↑s)
              (_ : ∀ (q : Quotient r), ∃ a, Quotient.mk r a = q),
          invFun := fun s =>
            { val := comap Quotient.mk' s, property := (_ : ∀ (x y : α), Rel r x y → Rel (comap Quotient.mk' s) x y) },
          left_inv :=
            (_ :
              ∀ (s : { s // r ≤ s }),
                (fun s =>
                      { val := comap Quotient.mk' s,
                        property := (_ : ∀ (x y : α), Rel r x y → Rel (comap Quotient.mk' s) x y) })
                    ((fun s =>
                        mapOfSurjective (↑s) Quotient.mk'' (_ : ker Quotient.mk'' ≤ ↑s)
                          (_ : ∀ (q : Quotient r), ∃ a, Quotient.mk r a = q))
                      s) =
                  s),
          right_inv :=
            (_ :
              ∀ (s : Setoid (Quotient r)),
                (fun s =>
                      mapOfSurjective (↑s) Quotient.mk'' (_ : ker Quotient.mk'' ≤ ↑s)
                        (_ : ∀ (q : Quotient r), ∃ a, Quotient.mk r a = q))
                    ((fun s =>
                        { val := comap Quotient.mk' s,
                          property := (_ : ∀ (x y : α), Rel r x y → Rel (comap Quotient.mk' s) x y) })
                      s) =
                  s) }
      t)
    x y
[PROOFSTEP]
exact ⟨a, b, hx, hy, h Hs⟩
[GOAL]
α : Type u_1
β : Type u_2
s : Setoid α
⊢ Subsingleton (Quotient s) ↔ s = ⊤
[PROOFSTEP]
simp only [_root_.subsingleton_iff, eq_top_iff, Setoid.le_def, Setoid.top_def, Pi.top_apply, forall_const]
[GOAL]
α : Type u_1
β : Type u_2
s : Setoid α
⊢ (∀ (x y : Quotient s), x = y) ↔ ∀ {x y : α}, ⊤ → Setoid.Rel s x y
[PROOFSTEP]
refine' (surjective_quotient_mk _).forall.trans (forall_congr' fun a => _)
[GOAL]
α : Type u_1
β : Type u_2
s : Setoid α
a : α
⊢ (∀ (y : Quotient s), Quotient.mk s a = y) ↔ ∀ {y : α}, ⊤ → Setoid.Rel s a y
[PROOFSTEP]
refine' (surjective_quotient_mk _).forall.trans (forall_congr' fun b => _)
[GOAL]
α : Type u_1
β : Type u_2
s : Setoid α
a b : α
⊢ Quotient.mk s a = Quotient.mk s b ↔ ⊤ → Setoid.Rel s a b
[PROOFSTEP]
simp_rw [← Quotient.mk''_eq_mk, Prop.top_eq_true, true_implies, Quotient.eq'']
[GOAL]
α : Type u_1
β : Type u_2
s : Setoid α
a b : α
⊢ Setoid.r a b ↔ Setoid.Rel s a b
[PROOFSTEP]
rfl
[GOAL]
α : Type u_1
β : Type u_2
r : α → α → Prop
⊢ Subsingleton (Quot r) ↔ EqvGen r = ⊤
[PROOFSTEP]
simp only [_root_.subsingleton_iff, _root_.eq_top_iff, Pi.le_def, Pi.top_apply, forall_const]
[GOAL]
α : Type u_1
β : Type u_2
r : α → α → Prop
⊢ (∀ (x y : Quot r), x = y) ↔ ∀ (i i_1 : α), ⊤ ≤ EqvGen r i i_1
[PROOFSTEP]
refine' (surjective_quot_mk _).forall.trans (forall_congr' fun a => _)
[GOAL]
α : Type u_1
β : Type u_2
r : α → α → Prop
a : α
⊢ (∀ (y : Quot r), mk r a = y) ↔ ∀ (i : α), ⊤ ≤ EqvGen r a i
[PROOFSTEP]
refine' (surjective_quot_mk _).forall.trans (forall_congr' fun b => _)
[GOAL]
α : Type u_1
β : Type u_2
r : α → α → Prop
a b : α
⊢ mk r a = mk r b ↔ ⊤ ≤ EqvGen r a b
[PROOFSTEP]
rw [Quot.eq]
[GOAL]
α : Type u_1
β : Type u_2
r : α → α → Prop
a b : α
⊢ EqvGen r a b ↔ ⊤ ≤ EqvGen r a b
[PROOFSTEP]
simp only [forall_const, le_Prop_eq, OrderTop.toTop, Pi.orderTop, Pi.top_apply, Prop.top_eq_true, true_implies]