internlm/Lean-Github huggingface dataset:
Theorem: DividedPowerAlgebra.gamma_mem_grade
Proof state before:
case add.a.mk
R : Type u
inst✝⁴ : CommRing R
M : Type u_1
inst✝³ : AddCommGroup M
inst✝² : Module R M
S : Type u_2
inst✝¹ : CommRing S
inst✝ : Algebra R S
x y : S ⊗[R] M
hx : ∀ (n : ℕ), (gamma R M n).toFun S x ∈ LinearMap.range (LinearMap.lTensor S (grade R M n).subtype)
hy : ∀ (n : ℕ), (gamma R M n).toFun S y ∈ LinearMap.range (LinearMap.lTensor S (grade R M n).subtype)
n k l : ℕ
hkl : (k, l) ∈ Finset.antidiagonal n
⊢ (dpScalarExtensionInv R S M) (dp S k x) * (dpScalarExtensionInv R S M) (dp S l y) ∈
    LinearMap.range (LinearMap.lTensor S (grade R M n).subtype)
Tactic:
specialize hx k
Proof state after:
case add.a.mk
R : Type u
inst✝⁴ : CommRing R
M : Type u_1
inst✝³ : AddCommGroup M
inst✝² : Module R M
S : Type u_2
inst✝¹ : CommRing S
inst✝ : Algebra R S
x y : S ⊗[R] M
hy : ∀ (n : ℕ), (gamma R M n).toFun S y ∈ LinearMap.range (LinearMap.lTensor S (grade R M n).subtype)
n k l : ℕ
hkl : (k, l) ∈ Finset.antidiagonal n
hx : (gamma R M k).toFun S x ∈ LinearMap.range (LinearMap.lTensor S (grade R M k).subtype)
⊢ (dpScalarExtensionInv R S M) (dp S k x) * (dpScalarExtensionInv R S M) (dp S l y) ∈
    LinearMap.range (LinearMap.lTensor S (grade R M n).subtype)
Theorem: DividedPowerAlgebra.gamma_mem_grade
Proof state before:
case add.a.mk
R : Type u
inst✝⁴ : CommRing R
M : Type u_1
inst✝³ : AddCommGroup M
inst✝² : Module R M
S : Type u_2
inst✝¹ : CommRing S
inst✝ : Algebra R S
x y : S ⊗[R] M
hy : ∀ (n : ℕ), (gamma R M n).toFun S y ∈ LinearMap.range (LinearMap.lTensor S (grade R M n).subtype)
n k l : ℕ
hkl : (k, l) ∈ Finset.antidiagonal n
hx : (gamma R M k).toFun S x ∈ LinearMap.range (LinearMap.lTensor S (grade R M k).subtype)
⊢ (dpScalarExtensionInv R S M) (dp S k x) * (dpScalarExtensionInv R S M) (dp S l y) ∈
    LinearMap.range (LinearMap.lTensor S (grade R M n).subtype)
Tactic:
specialize hy l
Proof state after:
case add.a.mk
R : Type u
inst✝⁴ : CommRing R
M : Type u_1
inst✝³ : AddCommGroup M
inst✝² : Module R M
S : Type u_2
inst✝¹ : CommRing S
inst✝ : Algebra R S
x y : S ⊗[R] M
n k l : ℕ
hkl : (k, l) ∈ Finset.antidiagonal n
hx : (gamma R M k).toFun S x ∈ LinearMap.range (LinearMap.lTensor S (grade R M k).subtype)
hy : (gamma R M l).toFun S y ∈ LinearMap.range (LinearMap.lTensor S (grade R M l).subtype)
⊢ (dpScalarExtensionInv R S M) (dp S k x) * (dpScalarExtensionInv R S M) (dp S l y) ∈
    LinearMap.range (LinearMap.lTensor S (grade R M n).subtype)
Theorem: DividedPowerAlgebra.gamma_mem_grade
Proof state before:
case add.a.mk
R : Type u
inst✝⁴ : CommRing R
M : Type u_1
inst✝³ : AddCommGroup M
inst✝² : Module R M
S : Type u_2
inst✝¹ : CommRing S
inst✝ : Algebra R S
x y : S ⊗[R] M
n k l : ℕ
hkl : (k, l) ∈ Finset.antidiagonal n
hx : (gamma R M k).toFun S x ∈ LinearMap.range (LinearMap.lTensor S (grade R M k).subtype)
hy : (gamma R M l).toFun S y ∈ LinearMap.range (LinearMap.lTensor S (grade R M l).subtype)
⊢ (dpScalarExtensionInv R S M) (dp S k x) * (dpScalarExtensionInv R S M) (dp S l y) ∈
    LinearMap.range (LinearMap.lTensor S (grade R M n).subtype)
Tactic:
simp only [gamma_toFun, dpScalarExtensionEquiv, ofAlgHom_symm_apply, LinearMap.mem_range] at hx hy
Proof state after:
case add.a.mk
R : Type u
inst✝⁴ : CommRing R
M : Type u_1
inst✝³ : AddCommGroup M
inst✝² : Module R M
S : Type u_2
inst✝¹ : CommRing S
inst✝ : Algebra R S
x y : S ⊗[R] M
n k l : ℕ
hkl : (k, l) ∈ Finset.antidiagonal n
hx : ∃ y, (LinearMap.lTensor S (grade R M k).subtype) y = (dpScalarExtensionInv R S M) (dp S k x)
hy : ∃ y_1, (LinearMap.lTensor S (grade R M l).subtype) y_1 = (dpScalarExtensionInv R S M) (dp S l y)
⊢ (dpScalarExtensionInv R S M) (dp S k x) * (dpScalarExtensionInv R S M) (dp S l y) ∈
    LinearMap.range (LinearMap.lTensor S (grade R M n).subtype)
Theorem: DividedPowerAlgebra.gamma_mem_grade
Proof state before:
case add.a.mk
R : Type u
inst✝⁴ : CommRing R
M : Type u_1
inst✝³ : AddCommGroup M
inst✝² : Module R M
S : Type u_2
inst✝¹ : CommRing S
inst✝ : Algebra R S
x y : S ⊗[R] M
n k l : ℕ
hkl : (k, l) ∈ Finset.antidiagonal n
hx : ∃ y, (LinearMap.lTensor S (grade R M k).subtype) y = (dpScalarExtensionInv R S M) (dp S k x)
hy : ∃ y_1, (LinearMap.lTensor S (grade R M l).subtype) y_1 = (dpScalarExtensionInv R S M) (dp S l y)
⊢ (dpScalarExtensionInv R S M) (dp S k x) * (dpScalarExtensionInv R S M) (dp S l y) ∈
    LinearMap.range (LinearMap.lTensor S (grade R M n).subtype)
Tactic:
obtain ⟨x', hx'⟩ := hx
Proof state after:
case add.a.mk.intro
R : Type u
inst✝⁴ : CommRing R
M : Type u_1
inst✝³ : AddCommGroup M
inst✝² : Module R M
S : Type u_2
inst✝¹ : CommRing S
inst✝ : Algebra R S
x y : S ⊗[R] M
n k l : ℕ
hkl : (k, l) ∈ Finset.antidiagonal n
hy : ∃ y_1, (LinearMap.lTensor S (grade R M l).subtype) y_1 = (dpScalarExtensionInv R S M) (dp S l y)
x' : S ⊗[R] ↥(grade R M k)
hx' : (LinearMap.lTensor S (grade R M k).subtype) x' = (dpScalarExtensionInv R S M) (dp S k x)
⊢ (dpScalarExtensionInv R S M) (dp S k x) * (dpScalarExtensionInv R S M) (dp S l y) ∈
    LinearMap.range (LinearMap.lTensor S (grade R M n).subtype)
Theorem: DividedPowerAlgebra.gamma_mem_grade
Proof state before:
case add.a.mk.intro
R : Type u
inst✝⁴ : CommRing R
M : Type u_1
inst✝³ : AddCommGroup M
inst✝² : Module R M
S : Type u_2
inst✝¹ : CommRing S
inst✝ : Algebra R S
x y : S ⊗[R] M
n k l : ℕ
hkl : (k, l) ∈ Finset.antidiagonal n
hy : ∃ y_1, (LinearMap.lTensor S (grade R M l).subtype) y_1 = (dpScalarExtensionInv R S M) (dp S l y)
x' : S ⊗[R] ↥(grade R M k)
hx' : (LinearMap.lTensor S (grade R M k).subtype) x' = (dpScalarExtensionInv R S M) (dp S k x)
⊢ (dpScalarExtensionInv R S M) (dp S k x) * (dpScalarExtensionInv R S M) (dp S l y) ∈
    LinearMap.range (LinearMap.lTensor S (grade R M n).subtype)
Tactic:
obtain ⟨y', hy'⟩ := hy
Proof state after:
case add.a.mk.intro.intro
R : Type u
inst✝⁴ : CommRing R
M : Type u_1
inst✝³ : AddCommGroup M
inst✝² : Module R M
S : Type u_2
inst✝¹ : CommRing S
inst✝ : Algebra R S
x y : S ⊗[R] M
n k l : ℕ
hkl : (k, l) ∈ Finset.antidiagonal n
x' : S ⊗[R] ↥(grade R M k)
hx' : (LinearMap.lTensor S (grade R M k).subtype) x' = (dpScalarExtensionInv R S M) (dp S k x)
y' : S ⊗[R] ↥(grade R M l)
hy' : (LinearMap.lTensor S (grade R M l).subtype) y' = (dpScalarExtensionInv R S M) (dp S l y)
⊢ (dpScalarExtensionInv R S M) (dp S k x) * (dpScalarExtensionInv R S M) (dp S l y) ∈
    LinearMap.range (LinearMap.lTensor S (grade R M n).subtype)
Theorem: DividedPowerAlgebra.gamma_mem_grade
Proof state before:
case add.a.mk.intro.intro
R : Type u
inst✝⁴ : CommRing R
M : Type u_1
inst✝³ : AddCommGroup M
inst✝² : Module R M
S : Type u_2
inst✝¹ : CommRing S
inst✝ : Algebra R S
x y : S ⊗[R] M
n k l : ℕ
hkl : (k, l) ∈ Finset.antidiagonal n
x' : S ⊗[R] ↥(grade R M k)
hx' : (LinearMap.lTensor S (grade R M k).subtype) x' = (dpScalarExtensionInv R S M) (dp S k x)
y' : S ⊗[R] ↥(grade R M l)
hy' : (LinearMap.lTensor S (grade R M l).subtype) y' = (dpScalarExtensionInv R S M) (dp S l y)
⊢ (dpScalarExtensionInv R S M) (dp S k x) * (dpScalarExtensionInv R S M) (dp S l y) ∈
    LinearMap.range (LinearMap.lTensor S (grade R M n).subtype)
Tactic:
simp only [LinearMap.mem_range]
Proof state after:
case add.a.mk.intro.intro
R : Type u
inst✝⁴ : CommRing R
M : Type u_1
inst✝³ : AddCommGroup M
inst✝² : Module R M
S : Type u_2
inst✝¹ : CommRing S
inst✝ : Algebra R S
x y : S ⊗[R] M
n k l : ℕ
hkl : (k, l) ∈ Finset.antidiagonal n
x' : S ⊗[R] ↥(grade R M k)
hx' : (LinearMap.lTensor S (grade R M k).subtype) x' = (dpScalarExtensionInv R S M) (dp S k x)
y' : S ⊗[R] ↥(grade R M l)
hy' : (LinearMap.lTensor S (grade R M l).subtype) y' = (dpScalarExtensionInv R S M) (dp S l y)
⊢ ∃ y_1,
    (LinearMap.lTensor S (grade R M n).subtype) y_1 =
      (dpScalarExtensionInv R S M) (dp S k x) * (dpScalarExtensionInv R S M) (dp S l y)
Theorem: DividedPowerAlgebra.gamma_mem_grade
Proof state before:
case add.a.mk.intro.intro
R : Type u
inst✝⁴ : CommRing R
M : Type u_1
inst✝³ : AddCommGroup M
inst✝² : Module R M
S : Type u_2
inst✝¹ : CommRing S
inst✝ : Algebra R S
x y : S ⊗[R] M
n k l : ℕ
hkl : (k, l) ∈ Finset.antidiagonal n
x' : S ⊗[R] ↥(grade R M k)
hx' : (LinearMap.lTensor S (grade R M k).subtype) x' = (dpScalarExtensionInv R S M) (dp S k x)
y' : S ⊗[R] ↥(grade R M l)
hy' : (LinearMap.lTensor S (grade R M l).subtype) y' = (dpScalarExtensionInv R S M) (dp S l y)
⊢ ∃ y_1,
    (LinearMap.lTensor S (grade R M n).subtype) y_1 =
      (dpScalarExtensionInv R S M) (dp S k x) * (dpScalarExtensionInv R S M) (dp S l y)
Tactic:
rw [← hx', ← hy']
Proof state after:
case add.a.mk.intro.intro
R : Type u
inst✝⁴ : CommRing R
M : Type u_1
inst✝³ : AddCommGroup M
inst✝² : Module R M
S : Type u_2
inst✝¹ : CommRing S
inst✝ : Algebra R S
x y : S ⊗[R] M
n k l : ℕ
hkl : (k, l) ∈ Finset.antidiagonal n
x' : S ⊗[R] ↥(grade R M k)
hx' : (LinearMap.lTensor S (grade R M k).subtype) x' = (dpScalarExtensionInv R S M) (dp S k x)
y' : S ⊗[R] ↥(grade R M l)
hy' : (LinearMap.lTensor S (grade R M l).subtype) y' = (dpScalarExtensionInv R S M) (dp S l y)
⊢ ∃ y,
    (LinearMap.lTensor S (grade R M n).subtype) y =
      (LinearMap.lTensor S (grade R M k).subtype) x' * (LinearMap.lTensor S (grade R M l).subtype) y'
Theorem: DividedPowerAlgebra.gamma_mem_grade
Proof state before:
case add.a.mk.intro.intro
R : Type u
inst✝⁴ : CommRing R
M : Type u_1
inst✝³ : AddCommGroup M
inst✝² : Module R M
S : Type u_2
inst✝¹ : CommRing S
inst✝ : Algebra R S
x y : S ⊗[R] M
n k l : ℕ
hkl : (k, l) ∈ Finset.antidiagonal n
x' : S ⊗[R] ↥(grade R M k)
hx' : (LinearMap.lTensor S (grade R M k).subtype) x' = (dpScalarExtensionInv R S M) (dp S k x)
y' : S ⊗[R] ↥(grade R M l)
hy' : (LinearMap.lTensor S (grade R M l).subtype) y' = (dpScalarExtensionInv R S M) (dp S l y)
⊢ ∃ y,
    (LinearMap.lTensor S (grade R M n).subtype) y =
      (LinearMap.lTensor S (grade R M k).subtype) x' * (LinearMap.lTensor S (grade R M l).subtype) y'
Tactic:
sorry
Proof state after:
no goals
Theorem: DividedPowerAlgebra.toModule_free
Proof state before:
R : Type u
inst✝³ : CommRing R
M : Type u_1
inst✝² : AddCommGroup M
inst✝¹ : Module R M
inst✝ : Module.Free R M
⊢ Module.Free R (DividedPowerAlgebra R M)
Tactic:
classical
haveI : ∀ i, Module.Free R (grade R M i) := fun i ↦ grade_free R M i
haveI : Module.Free R (DirectSum ℕ fun i ↦ ↥(grade R M i)) := by
  apply Module.Free.directSum
apply Module.Free.of_equiv (DirectSum.decomposeLinearEquiv (grade R M)).symm
Proof state after:
no goals
Theorem: DividedPowerAlgebra.toModule_free
Proof state before:
R : Type u
inst✝³ : CommRing R
M : Type u_1
inst✝² : AddCommGroup M
inst✝¹ : Module R M
inst✝ : Module.Free R M
⊢ Module.Free R (DividedPowerAlgebra R M)
Tactic:
haveI : ∀ i, Module.Free R (grade R M i) := fun i ↦ grade_free R M i
Proof state after:
R : Type u
inst✝³ : CommRing R
M : Type u_1
inst✝² : AddCommGroup M
inst✝¹ : Module R M
inst✝ : Module.Free R M
this : ∀ (i : ℕ), Module.Free R ↥(grade R M i)
⊢ Module.Free R (DividedPowerAlgebra R M)
Theorem: DividedPowerAlgebra.toModule_free
Proof state before:
R : Type u
inst✝³ : CommRing R
M : Type u_1
inst✝² : AddCommGroup M
inst✝¹ : Module R M
inst✝ : Module.Free R M
this : ∀ (i : ℕ), Module.Free R ↥(grade R M i)
⊢ Module.Free R (DividedPowerAlgebra R M)
Tactic:
haveI : Module.Free R (DirectSum ℕ fun i ↦ ↥(grade R M i)) := by
  apply Module.Free.directSum
Proof state after:
R : Type u
inst✝³ : CommRing R
M : Type u_1
inst✝² : AddCommGroup M
inst✝¹ : Module R M
inst✝ : Module.Free R M
this✝ : ∀ (i : ℕ), Module.Free R ↥(grade R M i)
this : Module.Free R (DirectSum ℕ fun i => ↥(grade R M i))
⊢ Module.Free R (DividedPowerAlgebra R M)
Theorem: DividedPowerAlgebra.toModule_free
Proof state before:
R : Type u
inst✝³ : CommRing R
M : Type u_1
inst✝² : AddCommGroup M
inst✝¹ : Module R M
inst✝ : Module.Free R M
this✝ : ∀ (i : ℕ), Module.Free R ↥(grade R M i)
this : Module.Free R (DirectSum ℕ fun i => ↥(grade R M i))
⊢ Module.Free R (DividedPowerAlgebra R M)
Tactic:
apply Module.Free.of_equiv (DirectSum.decomposeLinearEquiv (grade R M)).symm
Proof state after:
no goals
Theorem: DividedPowerAlgebra.toModule_free
Proof state before:
R : Type u
inst✝³ : CommRing R
M : Type u_1
inst✝² : AddCommGroup M
inst✝¹ : Module R M
inst✝ : Module.Free R M
this : ∀ (i : ℕ), Module.Free R ↥(grade R M i)
⊢ Module.Free R (DirectSum ℕ fun i => ↥(grade R M i))
Tactic:
apply Module.Free.directSum
Proof state after:
no goals
Theorem: Nat.isUnitFactorial
Proof state before:
n : ℕ
⊢ IsUnit ↑n !
Tactic:
rw [isUnit_iff_ne_zero, ne_eq, Nat.cast_eq_zero]
Proof state after:
n : ℕ
⊢ ¬n ! = 0
Theorem: Nat.isUnitFactorial
Proof state before:
n : ℕ
⊢ ¬n ! = 0
Tactic:
apply Nat.factorial_ne_zero
Proof state after:
no goals
Theorem: Nat.inv_smul_eq_invCast_mul
Proof state before:
A : Type u_1
inst✝¹ : CommSemiring A
inst✝ : Algebra ℚ A
n : ℕ
a : A
⊢ Ring.inverse ↑n • a = Ring.inverse ↑n * a
Tactic:
cases' Nat.eq_zero_or_pos n with hn hn
Proof state after:
case inl
A : Type u_1
inst✝¹ : CommSemiring A
inst✝ : Algebra ℚ A
n : ℕ
a : A
hn : n = 0
⊢ Ring.inverse ↑n • a = Ring.inverse ↑n * a

case inr
A : Type u_1
inst✝¹ : CommSemiring A
inst✝ : Algebra ℚ A
n : ℕ
a : A
hn : n > 0
⊢ Ring.inverse ↑n • a = Ring.inverse ↑n * a
Theorem: Nat.inv_smul_eq_invCast_mul
Proof state before:
case inl
A : Type u_1
inst✝¹ : CommSemiring A
inst✝ : Algebra ℚ A
n : ℕ
a : A
hn : n = 0
⊢ Ring.inverse ↑n • a = Ring.inverse ↑n * a

case inr
A : Type u_1
inst✝¹ : CommSemiring A
inst✝ : Algebra ℚ A
n : ℕ
a : A
hn : n > 0
⊢ Ring.inverse ↑n • a = Ring.inverse ↑n * a
Tactic:
. simp only [hn, Nat.cast_zero, isUnit_zero_iff, not_false_eq_true, Ring.inverse_non_unit, zero_smul,
  Ring.inverse_zero, zero_mul]
Proof state after:
case inr
A : Type u_1
inst✝¹ : CommSemiring A
inst✝ : Algebra ℚ A
n : ℕ
a : A
hn : n > 0
⊢ Ring.inverse ↑n • a = Ring.inverse ↑n * a
Theorem: Nat.inv_smul_eq_invCast_mul
Proof state before:
case inr
A : Type u_1
inst✝¹ : CommSemiring A
inst✝ : Algebra ℚ A
n : ℕ
a : A
hn : n > 0
⊢ Ring.inverse ↑n • a = Ring.inverse ↑n * a
Tactic:
. suffices hn' : IsUnit (n : ℚ) by
    simp only [Algebra.smul_def, ← map_natCast (algebraMap ℚ A)]
    apply symm
    rw [Ring.inverse_mul_eq_iff_eq_mul _ _ _ (RingHom.isUnit_map _ hn'), ← mul_assoc]
    apply symm
    convert @one_mul A _ _
    simp only [← map_mul, ← map_one (algebraMap ℚ A)]
    apply congr_arg
    apply symm
    rw [Ring.eq_mul_inverse_iff_mul_eq _ _ _ hn', one_mul]
  rw [isUnit_iff_ne_zero, ne_eq, Nat.cast_eq_zero]
  exact Nat.ne_of_gt hn
Proof state after:
no goals
Theorem: Nat.inv_smul_eq_invCast_mul
Proof state before:
case inl
A : Type u_1
inst✝¹ : CommSemiring A
inst✝ : Algebra ℚ A
n : ℕ
a : A
hn : n = 0
⊢ Ring.inverse ↑n • a = Ring.inverse ↑n * a
Tactic:
simp only [hn, Nat.cast_zero, isUnit_zero_iff, not_false_eq_true, Ring.inverse_non_unit, zero_smul,
Ring.inverse_zero, zero_mul]
Proof state after:
no goals
Theorem: Nat.inv_smul_eq_invCast_mul
Proof state before:
case inr
A : Type u_1
inst✝¹ : CommSemiring A
inst✝ : Algebra ℚ A
n : ℕ
a : A
hn : n > 0
⊢ Ring.inverse ↑n • a = Ring.inverse ↑n * a
Tactic:
suffices hn' : IsUnit (n : ℚ) by
  simp only [Algebra.smul_def, ← map_natCast (algebraMap ℚ A)]
  apply symm
  rw [Ring.inverse_mul_eq_iff_eq_mul _ _ _ (RingHom.isUnit_map _ hn'), ← mul_assoc]
  apply symm
  convert @one_mul A _ _
  simp only [← map_mul, ← map_one (algebraMap ℚ A)]
  apply congr_arg
  apply symm
  rw [Ring.eq_mul_inverse_iff_mul_eq _ _ _ hn', one_mul]
Proof state after:
case inr
A : Type u_1
inst✝¹ : CommSemiring A
inst✝ : Algebra ℚ A
n : ℕ
a : A
hn : n > 0
⊢ IsUnit ↑n
Theorem: Nat.inv_smul_eq_invCast_mul
Proof state before:
case inr
A : Type u_1
inst✝¹ : CommSemiring A
inst✝ : Algebra ℚ A
n : ℕ
a : A
hn : n > 0
⊢ IsUnit ↑n
Tactic:
rw [isUnit_iff_ne_zero, ne_eq, Nat.cast_eq_zero]
Proof state after:
case inr
A : Type u_1
inst✝¹ : CommSemiring A
inst✝ : Algebra ℚ A
n : ℕ
a : A
hn : n > 0
⊢ ¬n = 0
Theorem: Nat.inv_smul_eq_invCast_mul
Proof state before:
case inr
A : Type u_1
inst✝¹ : CommSemiring A
inst✝ : Algebra ℚ A
n : ℕ
a : A
hn : n > 0
⊢ ¬n = 0
Tactic:
exact Nat.ne_of_gt hn
Proof state after:
no goals
Theorem: Nat.inv_smul_eq_invCast_mul
Proof state before:
A : Type u_1
inst✝¹ : CommSemiring A
inst✝ : Algebra ℚ A
n : ℕ
a : A
hn : n > 0
hn' : IsUnit ↑n
⊢ Ring.inverse ↑n • a = Ring.inverse ↑n * a
Tactic:
simp only [Algebra.smul_def, ← map_natCast (algebraMap ℚ A)]
Proof state after:
A : Type u_1
inst✝¹ : CommSemiring A
inst✝ : Algebra ℚ A
n : ℕ
a : A
hn : n > 0
hn' : IsUnit ↑n
⊢ (algebraMap ℚ A) (Ring.inverse ↑n) * a = Ring.inverse ((algebraMap ℚ A) ↑n) * a
Theorem: Nat.inv_smul_eq_invCast_mul
Proof state before:
A : Type u_1
inst✝¹ : CommSemiring A
inst✝ : Algebra ℚ A
n : ℕ
a : A
hn : n > 0
hn' : IsUnit ↑n
⊢ (algebraMap ℚ A) (Ring.inverse ↑n) * a = Ring.inverse ((algebraMap ℚ A) ↑n) * a
Tactic:
apply symm
Proof state after:
case a
A : Type u_1
inst✝¹ : CommSemiring A
inst✝ : Algebra ℚ A
n : ℕ
a : A
hn : n > 0
hn' : IsUnit ↑n
⊢ Ring.inverse ((algebraMap ℚ A) ↑n) * a = (algebraMap ℚ A) (Ring.inverse ↑n) * a
Theorem: Nat.inv_smul_eq_invCast_mul
Proof state before:
case a
A : Type u_1
inst✝¹ : CommSemiring A
inst✝ : Algebra ℚ A
n : ℕ
a : A
hn : n > 0
hn' : IsUnit ↑n
⊢ Ring.inverse ((algebraMap ℚ A) ↑n) * a = (algebraMap ℚ A) (Ring.inverse ↑n) * a
Tactic:
rw [Ring.inverse_mul_eq_iff_eq_mul _ _ _ (RingHom.isUnit_map _ hn'), ← mul_assoc]
Proof state after:
case a
A : Type u_1
inst✝¹ : CommSemiring A
inst✝ : Algebra ℚ A
n : ℕ
a : A
hn : n > 0
hn' : IsUnit ↑n
⊢ a = (algebraMap ℚ A) ↑n * (algebraMap ℚ A) (Ring.inverse ↑n) * a
Theorem: Nat.inv_smul_eq_invCast_mul
Proof state before:
case a
A : Type u_1
inst✝¹ : CommSemiring A
inst✝ : Algebra ℚ A
n : ℕ
a : A
hn : n > 0
hn' : IsUnit ↑n
⊢ a = (algebraMap ℚ A) ↑n * (algebraMap ℚ A) (Ring.inverse ↑n) * a
Tactic:
apply symm
Proof state after:
case a.a
A : Type u_1
inst✝¹ : CommSemiring A
inst✝ : Algebra ℚ A
n : ℕ
a : A
hn : n > 0
hn' : IsUnit ↑n
⊢ (algebraMap ℚ A) ↑n * (algebraMap ℚ A) (Ring.inverse ↑n) * a = a
Theorem: Nat.inv_smul_eq_invCast_mul
Proof state before:
case a.a
A : Type u_1
inst✝¹ : CommSemiring A
inst✝ : Algebra ℚ A
n : ℕ
a : A
hn : n > 0
hn' : IsUnit ↑n
⊢ (algebraMap ℚ A) ↑n * (algebraMap ℚ A) (Ring.inverse ↑n) * a = a
Tactic:
convert @one_mul A _ _
Proof state after:
case h.e'_2.h.e'_5
A : Type u_1
inst✝¹ : CommSemiring A
inst✝ : Algebra ℚ A
n : ℕ
a : A
hn : n > 0
hn' : IsUnit ↑n
⊢ (algebraMap ℚ A) ↑n * (algebraMap ℚ A) (Ring.inverse ↑n) = 1
Theorem: Nat.inv_smul_eq_invCast_mul
Proof state before:
case h.e'_2.h.e'_5
A : Type u_1
inst✝¹ : CommSemiring A
inst✝ : Algebra ℚ A
n : ℕ
a : A
hn : n > 0
hn' : IsUnit ↑n
⊢ (algebraMap ℚ A) ↑n * (algebraMap ℚ A) (Ring.inverse ↑n) = 1
Tactic:
simp only [← map_mul, ← map_one (algebraMap ℚ A)]
Proof state after:
case h.e'_2.h.e'_5
A : Type u_1
inst✝¹ : CommSemiring A
inst✝ : Algebra ℚ A
n : ℕ
a : A
hn : n > 0
hn' : IsUnit ↑n
⊢ (algebraMap ℚ A) (↑n * Ring.inverse ↑n) = (algebraMap ℚ A) 1
Theorem: Nat.inv_smul_eq_invCast_mul
Proof state before:
case h.e'_2.h.e'_5
A : Type u_1
inst✝¹ : CommSemiring A
inst✝ : Algebra ℚ A
n : ℕ
a : A
hn : n > 0
hn' : IsUnit ↑n
⊢ (algebraMap ℚ A) (↑n * Ring.inverse ↑n) = (algebraMap ℚ A) 1
Tactic:
apply congr_arg
Proof state after:
case h.e'_2.h.e'_5.h
A : Type u_1
inst✝¹ : CommSemiring A
inst✝ : Algebra ℚ A
n : ℕ
a : A
hn : n > 0
hn' : IsUnit ↑n
⊢ ↑n * Ring.inverse ↑n = 1
Theorem: Nat.inv_smul_eq_invCast_mul
Proof state before:
case h.e'_2.h.e'_5.h
A : Type u_1
inst✝¹ : CommSemiring A
inst✝ : Algebra ℚ A
n : ℕ
a : A
hn : n > 0
hn' : IsUnit ↑n
⊢ ↑n * Ring.inverse ↑n = 1
Tactic:
apply symm
Proof state after:
case h.e'_2.h.e'_5.h.a
A : Type u_1
inst✝¹ : CommSemiring A
inst✝ : Algebra ℚ A
n : ℕ
a : A
hn : n > 0
hn' : IsUnit ↑n
⊢ 1 = ↑n * Ring.inverse ↑n
Theorem: Nat.inv_smul_eq_invCast_mul
Proof state before:
case h.e'_2.h.e'_5.h.a
A : Type u_1
inst✝¹ : CommSemiring A
inst✝ : Algebra ℚ A
n : ℕ
a : A
hn : n > 0
hn' : IsUnit ↑n
⊢ 1 = ↑n * Ring.inverse ↑n
Tactic:
rw [Ring.eq_mul_inverse_iff_mul_eq _ _ _ hn', one_mul]
Proof state after:
no goals
Theorem: DividedPowers.OfInvertibleFactorial.dpow_eq_of_mem
Proof state before:
A : Type u_1
inst✝ : CommSemiring A
I✝ I : Ideal A
m : ℕ
x : A
hx : x ∈ I
⊢ dpow I m x = Ring.inverse ↑m ! * x ^ m
Tactic:
simp only [dpow]
Proof state after:
A : Type u_1
inst✝ : CommSemiring A
I✝ I : Ideal A
m : ℕ
x : A
hx : x ∈ I
⊢ (if x ∈ I then Ring.inverse ↑m ! * x ^ m else 0) = Ring.inverse ↑m ! * x ^ m
Theorem: DividedPowers.OfInvertibleFactorial.dpow_eq_of_mem
Proof state before:
A : Type u_1
inst✝ : CommSemiring A
I✝ I : Ideal A
m : ℕ
x : A
hx : x ∈ I
⊢ (if x ∈ I then Ring.inverse ↑m ! * x ^ m else 0) = Ring.inverse ↑m ! * x ^ m
Tactic:
rw [if_pos hx]
Proof state after:
no goals
Theorem: DividedPowers.OfInvertibleFactorial.dpow_eq_of_not_mem
Proof state before:
A : Type u_1
inst✝ : CommSemiring A
I✝ I : Ideal A
m : ℕ
x : A
hx : x ∉ I
⊢ dpow I m x = 0
Tactic:
simp only [dpow]
Proof state after:
A : Type u_1
inst✝ : CommSemiring A
I✝ I : Ideal A
m : ℕ
x : A
hx : x ∉ I
⊢ (if x ∈ I then Ring.inverse ↑m ! * x ^ m else 0) = 0
Theorem: DividedPowers.OfInvertibleFactorial.dpow_eq_of_not_mem
Proof state before:
A : Type u_1
inst✝ : CommSemiring A
I✝ I : Ideal A
m : ℕ
x : A
hx : x ∉ I
⊢ (if x ∈ I then Ring.inverse ↑m ! * x ^ m else 0) = 0
Tactic:
rw [if_neg hx]
Proof state after:
no goals
Theorem: DividedPowers.OfInvertibleFactorial.dpow_null
Proof state before:
A : Type u_1
inst✝ : CommSemiring A
I : Ideal A
m : ℕ
x : A
hx : x ∉ I
⊢ dpow I m x = 0
Tactic:
simp only [dpow]
Proof state after:
A : Type u_1
inst✝ : CommSemiring A
I : Ideal A
m : ℕ
x : A
hx : x ∉ I
⊢ (if x ∈ I then Ring.inverse ↑m ! * x ^ m else 0) = 0
Theorem: DividedPowers.OfInvertibleFactorial.dpow_null
Proof state before:
A : Type u_1
inst✝ : CommSemiring A
I : Ideal A
m : ℕ
x : A
hx : x ∉ I
⊢ (if x ∈ I then Ring.inverse ↑m ! * x ^ m else 0) = 0
Tactic:
rw [if_neg hx]
Proof state after:
no goals
Theorem: DividedPowers.OfInvertibleFactorial.dpow_zero
Proof state before:
A : Type u_1
inst✝ : CommSemiring A
I : Ideal A
x : A
hx : x ∈ I
⊢ dpow I 0 x = 1
Tactic:
simp only [dpow, factorial_zero, cast_one, Ring.inverse_one, _root_.pow_zero, mul_one, if_pos hx]
Proof state after:
no goals
Theorem: DividedPowers.OfInvertibleFactorial.dpow_one
Proof state before:
A : Type u_1
inst✝ : CommSemiring A
I : Ideal A
x : A
hx : x ∈ I
⊢ dpow I 1 x = x
Tactic:
rw [dpow_eq_of_mem 1 hx, pow_one, Nat.factorial_one, Nat.cast_one, Ring.inverse_one, one_mul]
Proof state after:
no goals
Theorem: DividedPowers.OfInvertibleFactorial.dpow_mem
Proof state before:
A : Type u_1
inst✝ : CommSemiring A
I : Ideal A
m : ℕ
hm : m ≠ 0
x : A
hx : x ∈ I
⊢ dpow I m x ∈ I
Tactic:
rw [dpow_eq_of_mem m hx]
Proof state after:
A : Type u_1
inst✝ : CommSemiring A
I : Ideal A
m : ℕ
hm : m ≠ 0
x : A
hx : x ∈ I
⊢ Ring.inverse ↑m ! * x ^ m ∈ I
Theorem: DividedPowers.OfInvertibleFactorial.dpow_mem
Proof state before:
A : Type u_1
inst✝ : CommSemiring A
I : Ideal A
m : ℕ
hm : m ≠ 0
x : A
hx : x ∈ I
⊢ Ring.inverse ↑m ! * x ^ m ∈ I
Tactic:
exact Ideal.mul_mem_left I _ (Ideal.pow_mem_of_mem I hx _ (Nat.pos_of_ne_zero hm))
Proof state after:
no goals
Theorem: DividedPowers.OfInvertibleFactorial.foo
Proof state before:
A : Type u_1
inst✝ : CommSemiring A
I : Ideal A
m : ℕ
k : ℕ × ℕ
hm : IsUnit ↑m !
hk : k ∈ Finset.antidiagonal m
⊢ ↑(m.choose k.1) = ↑m ! * Ring.inverse ↑k.1! * Ring.inverse ↑k.2!
Tactic:
rw [Finset.mem_antidiagonal] at hk
Proof state after:
A : Type u_1
inst✝ : CommSemiring A
I : Ideal A
m : ℕ
k : ℕ × ℕ
hm : IsUnit ↑m !
hk : k.1 + k.2 = m
⊢ ↑(m.choose k.1) = ↑m ! * Ring.inverse ↑k.1! * Ring.inverse ↑k.2!
Theorem: DividedPowers.OfInvertibleFactorial.foo
Proof state before:
A : Type u_1
inst✝ : CommSemiring A
I : Ideal A
m : ℕ
k : ℕ × ℕ
hm : IsUnit ↑m !
hk : k.1 + k.2 = m
⊢ ↑(m.choose k.1) = ↑m ! * Ring.inverse ↑k.1! * Ring.inverse ↑k.2!
Tactic:
rw [Ring.eq_mul_inverse_iff_mul_eq]
Proof state after:
A : Type u_1
inst✝ : CommSemiring A
I : Ideal A
m : ℕ
k : ℕ × ℕ
hm : IsUnit ↑m !
hk : k.1 + k.2 = m
⊢ ↑(m.choose k.1) * ↑k.2! = ↑m ! * Ring.inverse ↑k.1!

case h
A : Type u_1
inst✝ : CommSemiring A
I : Ideal A
m : ℕ
k : ℕ × ℕ
hm : IsUnit ↑m !
hk : k.1 + k.2 = m
⊢ IsUnit ↑k.2!