internlm/Lean-Github huggingface dataset:
Theorem: DividedPowerAlgebra.grade_one_eq_span
Proof state before:
case a.intro
R : Type u_1
inst✝⁶ : CommRing R
M : Type u_2
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
inst✝³ : DecidableEq R
inst✝² : DecidableEq M
inst✝¹ : Module Rᵐᵒᵖ M
inst✝ : IsCentralScalar R M
p : DividedPowerAlgebra R M
hp : p ∈ Set.range (dp R 1)
m : M
hm : dp R 1 m = p
⊢ dp R 1 m ∈ ↑(grade R M 1)
Tactic:
exact dp_mem_grade R M 1 m
Proof state after:
no goals
Theorem: DividedPowerAlgebra.grade_one_eq_span'
Proof state before:
R : Type u_1
inst✝⁶ : CommRing R
M : Type u_2
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
inst✝³ : DecidableEq R
inst✝² : DecidableEq M
inst✝¹ : Module Rᵐᵒᵖ M
inst✝ : IsCentralScalar R M
⊢ ⊤ = Submodule.span R (Set.range fun m => ⟨dp R 1 m, ⋯⟩)
Tactic:
apply Submodule.map_injective_of_injective (grade R M 1).injective_subtype
Proof state after:
case a
R : Type u_1
inst✝⁶ : CommRing R
M : Type u_2
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
inst✝³ : DecidableEq R
inst✝² : DecidableEq M
inst✝¹ : Module Rᵐᵒᵖ M
inst✝ : IsCentralScalar R M
⊢ Submodule.map (grade R M 1).subtype ⊤ =
    Submodule.map (grade R M 1).subtype (Submodule.span R (Set.range fun m => ⟨dp R 1 m, ⋯⟩))
Theorem: DividedPowerAlgebra.grade_one_eq_span'
Proof state before:
case a
R : Type u_1
inst✝⁶ : CommRing R
M : Type u_2
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
inst✝³ : DecidableEq R
inst✝² : DecidableEq M
inst✝¹ : Module Rᵐᵒᵖ M
inst✝ : IsCentralScalar R M
⊢ Submodule.map (grade R M 1).subtype ⊤ =
    Submodule.map (grade R M 1).subtype (Submodule.span R (Set.range fun m => ⟨dp R 1 m, ⋯⟩))
Tactic:
rw [Submodule.map_subtype_top, Submodule.map_span]
Proof state after:
case a
R : Type u_1
inst✝⁶ : CommRing R
M : Type u_2
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
inst✝³ : DecidableEq R
inst✝² : DecidableEq M
inst✝¹ : Module Rᵐᵒᵖ M
inst✝ : IsCentralScalar R M
⊢ grade R M 1 = Submodule.span R (⇑(grade R M 1).subtype '' Set.range fun m => ⟨dp R 1 m, ⋯⟩)
Theorem: DividedPowerAlgebra.grade_one_eq_span'
Proof state before:
case a
R : Type u_1
inst✝⁶ : CommRing R
M : Type u_2
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
inst✝³ : DecidableEq R
inst✝² : DecidableEq M
inst✝¹ : Module Rᵐᵒᵖ M
inst✝ : IsCentralScalar R M
⊢ grade R M 1 = Submodule.span R (⇑(grade R M 1).subtype '' Set.range fun m => ⟨dp R 1 m, ⋯⟩)
Tactic:
simp_rw [grade_one_eq_span R M]
Proof state after:
case a
R : Type u_1
inst✝⁶ : CommRing R
M : Type u_2
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
inst✝³ : DecidableEq R
inst✝² : DecidableEq M
inst✝¹ : Module Rᵐᵒᵖ M
inst✝ : IsCentralScalar R M
⊢ Submodule.span R (Set.range (dp R 1)) = Submodule.span R (⇑(grade R M 1).subtype '' Set.range fun m => ⟨dp R 1 m, ⋯⟩)
Theorem: DividedPowerAlgebra.grade_one_eq_span'
Proof state before:
case a
R : Type u_1
inst✝⁶ : CommRing R
M : Type u_2
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
inst✝³ : DecidableEq R
inst✝² : DecidableEq M
inst✝¹ : Module Rᵐᵒᵖ M
inst✝ : IsCentralScalar R M
⊢ Submodule.span R (Set.range (dp R 1)) = Submodule.span R (⇑(grade R M 1).subtype '' Set.range fun m => ⟨dp R 1 m, ⋯⟩)
Tactic:
rw [← Set.range_comp]
Proof state after:
case a
R : Type u_1
inst✝⁶ : CommRing R
M : Type u_2
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
inst✝³ : DecidableEq R
inst✝² : DecidableEq M
inst✝¹ : Module Rᵐᵒᵖ M
inst✝ : IsCentralScalar R M
⊢ Submodule.span R (Set.range (dp R 1)) = Submodule.span R (Set.range (⇑(grade R M 1).subtype ∘ fun m => ⟨dp R 1 m, ⋯⟩))
Theorem: DividedPowerAlgebra.grade_one_eq_span'
Proof state before:
case a
R : Type u_1
inst✝⁶ : CommRing R
M : Type u_2
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
inst✝³ : DecidableEq R
inst✝² : DecidableEq M
inst✝¹ : Module Rᵐᵒᵖ M
inst✝ : IsCentralScalar R M
⊢ Submodule.span R (Set.range (dp R 1)) = Submodule.span R (Set.range (⇑(grade R M 1).subtype ∘ fun m => ⟨dp R 1 m, ⋯⟩))
Tactic:
rfl
Proof state after:
no goals
Theorem: DividedPowerAlgebra.deg_one_right_inv
Proof state before:
R : Type u_1
inst✝⁶ : CommRing R
M : Type u_2
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
inst✝³ : DecidableEq R
inst✝² : DecidableEq M
inst✝¹ : Module Rᵐᵒᵖ M
inst✝ : IsCentralScalar R M
⊢ Function.RightInverse (⇑(sndHom R M) ∘ ⇑(toTrivSqZeroExt R M).toLinearMap ∘ ⇑(grade R M 1).subtype)
    (⇑(proj' R M 1) ∘ ⇑(ι R M))
Tactic:
simp only [Function.rightInverse_iff_comp, ← LinearMap.coe_comp, ← @LinearMap.id_coe R]
Proof state after:
R : Type u_1
inst✝⁶ : CommRing R
M : Type u_2
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
inst✝³ : DecidableEq R
inst✝² : DecidableEq M
inst✝¹ : Module Rᵐᵒᵖ M
inst✝ : IsCentralScalar R M
⊢ ⇑((proj' R M 1 ∘ₗ ι R M) ∘ₗ sndHom R M ∘ₗ (toTrivSqZeroExt R M).toLinearMap ∘ₗ (grade R M 1).subtype) = ⇑LinearMap.id
Theorem: DividedPowerAlgebra.deg_one_right_inv
Proof state before:
R : Type u_1
inst✝⁶ : CommRing R
M : Type u_2
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
inst✝³ : DecidableEq R
inst✝² : DecidableEq M
inst✝¹ : Module Rᵐᵒᵖ M
inst✝ : IsCentralScalar R M
⊢ ⇑((proj' R M 1 ∘ₗ ι R M) ∘ₗ sndHom R M ∘ₗ (toTrivSqZeroExt R M).toLinearMap ∘ₗ (grade R M 1).subtype) = ⇑LinearMap.id
Tactic:
rw [DFunLike.coe_injective.eq_iff]
Proof state after:
R : Type u_1
inst✝⁶ : CommRing R
M : Type u_2
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
inst✝³ : DecidableEq R
inst✝² : DecidableEq M
inst✝¹ : Module Rᵐᵒᵖ M
inst✝ : IsCentralScalar R M
⊢ (proj' R M 1 ∘ₗ ι R M) ∘ₗ sndHom R M ∘ₗ (toTrivSqZeroExt R M).toLinearMap ∘ₗ (grade R M 1).subtype = LinearMap.id
Theorem: DividedPowerAlgebra.deg_one_right_inv
Proof state before:
R : Type u_1
inst✝⁶ : CommRing R
M : Type u_2
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
inst✝³ : DecidableEq R
inst✝² : DecidableEq M
inst✝¹ : Module Rᵐᵒᵖ M
inst✝ : IsCentralScalar R M
⊢ (proj' R M 1 ∘ₗ ι R M) ∘ₗ sndHom R M ∘ₗ (toTrivSqZeroExt R M).toLinearMap ∘ₗ (grade R M 1).subtype = LinearMap.id
Tactic:
apply LinearMap.ext_on_range (grade_one_eq_span' R M).symm
Proof state after:
R : Type u_1
inst✝⁶ : CommRing R
M : Type u_2
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
inst✝³ : DecidableEq R
inst✝² : DecidableEq M
inst✝¹ : Module Rᵐᵒᵖ M
inst✝ : IsCentralScalar R M
⊢ ∀ (i : M),
    ((proj' R M 1 ∘ₗ ι R M) ∘ₗ sndHom R M ∘ₗ (toTrivSqZeroExt R M).toLinearMap ∘ₗ (grade R M 1).subtype) ⟨dp R 1 i, ⋯⟩ =
      LinearMap.id ⟨dp R 1 i, ⋯⟩
Theorem: DividedPowerAlgebra.deg_one_right_inv
Proof state before:
R : Type u_1
inst✝⁶ : CommRing R
M : Type u_2
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
inst✝³ : DecidableEq R
inst✝² : DecidableEq M
inst✝¹ : Module Rᵐᵒᵖ M
inst✝ : IsCentralScalar R M
⊢ ∀ (i : M),
    ((proj' R M 1 ∘ₗ ι R M) ∘ₗ sndHom R M ∘ₗ (toTrivSqZeroExt R M).toLinearMap ∘ₗ (grade R M 1).subtype) ⟨dp R 1 i, ⋯⟩ =
      LinearMap.id ⟨dp R 1 i, ⋯⟩
Tactic:
intro m
Proof state after:
R : Type u_1
inst✝⁶ : CommRing R
M : Type u_2
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
inst✝³ : DecidableEq R
inst✝² : DecidableEq M
inst✝¹ : Module Rᵐᵒᵖ M
inst✝ : IsCentralScalar R M
m : M
⊢ ((proj' R M 1 ∘ₗ ι R M) ∘ₗ sndHom R M ∘ₗ (toTrivSqZeroExt R M).toLinearMap ∘ₗ (grade R M 1).subtype) ⟨dp R 1 m, ⋯⟩ =
    LinearMap.id ⟨dp R 1 m, ⋯⟩
Theorem: DividedPowerAlgebra.deg_one_right_inv
Proof state before:
R : Type u_1
inst✝⁶ : CommRing R
M : Type u_2
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
inst✝³ : DecidableEq R
inst✝² : DecidableEq M
inst✝¹ : Module Rᵐᵒᵖ M
inst✝ : IsCentralScalar R M
m : M
⊢ ((proj' R M 1 ∘ₗ ι R M) ∘ₗ sndHom R M ∘ₗ (toTrivSqZeroExt R M).toLinearMap ∘ₗ (grade R M 1).subtype) ⟨dp R 1 m, ⋯⟩ =
    LinearMap.id ⟨dp R 1 m, ⋯⟩
Tactic:
simp only [proj', proj, ι, LinearMap.coe_comp, LinearMap.coe_mk, AddHom.coe_mk,
  Submodule.coeSubtype, comp_apply, AlgHom.toLinearMap_apply, sndHom_apply,
  LinearMap.id_coe, id_eq]
Proof state after:
R : Type u_1
inst✝⁶ : CommRing R
M : Type u_2
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
inst✝³ : DecidableEq R
inst✝² : DecidableEq M
inst✝¹ : Module Rᵐᵒᵖ M
inst✝ : IsCentralScalar R M
m : M
⊢ ((DirectSum.decompose (grade R M)) (dp R 1 ((toTrivSqZeroExt R M) (dp R 1 m)).snd)) 1 = ⟨dp R 1 m, ⋯⟩
Theorem: DividedPowerAlgebra.deg_one_right_inv
Proof state before:
R : Type u_1
inst✝⁶ : CommRing R
M : Type u_2
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
inst✝³ : DecidableEq R
inst✝² : DecidableEq M
inst✝¹ : Module Rᵐᵒᵖ M
inst✝ : IsCentralScalar R M
m : M
⊢ ((DirectSum.decompose (grade R M)) (dp R 1 ((toTrivSqZeroExt R M) (dp R 1 m)).snd)) 1 = ⟨dp R 1 m, ⋯⟩
Tactic:
ext
Proof state after:
case a
R : Type u_1
inst✝⁶ : CommRing R
M : Type u_2
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
inst✝³ : DecidableEq R
inst✝² : DecidableEq M
inst✝¹ : Module Rᵐᵒᵖ M
inst✝ : IsCentralScalar R M
m : M
⊢ ↑(((DirectSum.decompose (grade R M)) (dp R 1 ((toTrivSqZeroExt R M) (dp R 1 m)).snd)) 1) = ↑⟨dp R 1 m, ⋯⟩
Theorem: DividedPowerAlgebra.deg_one_right_inv
Proof state before:
case a
R : Type u_1
inst✝⁶ : CommRing R
M : Type u_2
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
inst✝³ : DecidableEq R
inst✝² : DecidableEq M
inst✝¹ : Module Rᵐᵒᵖ M
inst✝ : IsCentralScalar R M
m : M
⊢ ↑(((DirectSum.decompose (grade R M)) (dp R 1 ((toTrivSqZeroExt R M) (dp R 1 m)).snd)) 1) = ↑⟨dp R 1 m, ⋯⟩
Tactic:
dsimp only
Proof state after:
case a
R : Type u_1
inst✝⁶ : CommRing R
M : Type u_2
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
inst✝³ : DecidableEq R
inst✝² : DecidableEq M
inst✝¹ : Module Rᵐᵒᵖ M
inst✝ : IsCentralScalar R M
m : M
⊢ ↑(((DirectSum.decompose (grade R M)) (dp R 1 ((toTrivSqZeroExt R M) (dp R 1 m)).snd)) 1) = dp R 1 m
Theorem: DividedPowerAlgebra.deg_one_right_inv
Proof state before:
case a
R : Type u_1
inst✝⁶ : CommRing R
M : Type u_2
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
inst✝³ : DecidableEq R
inst✝² : DecidableEq M
inst✝¹ : Module Rᵐᵒᵖ M
inst✝ : IsCentralScalar R M
m : M
⊢ ↑(((DirectSum.decompose (grade R M)) (dp R 1 ((toTrivSqZeroExt R M) (dp R 1 m)).snd)) 1) = dp R 1 m
Tactic:
rw [← ι_def R M m, toTrivSqZeroExt_ι, ← ι_def, snd_inr, decompose_of_mem_same]
Proof state after:
case a.hx
R : Type u_1
inst✝⁶ : CommRing R
M : Type u_2
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
inst✝³ : DecidableEq R
inst✝² : DecidableEq M
inst✝¹ : Module Rᵐᵒᵖ M
inst✝ : IsCentralScalar R M
m : M
⊢ (ι R M) m ∈ grade R M 1
Theorem: DividedPowerAlgebra.deg_one_right_inv
Proof state before:
case a.hx
R : Type u_1
inst✝⁶ : CommRing R
M : Type u_2
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
inst✝³ : DecidableEq R
inst✝² : DecidableEq M
inst✝¹ : Module Rᵐᵒᵖ M
inst✝ : IsCentralScalar R M
m : M
⊢ (ι R M) m ∈ grade R M 1
Tactic:
apply ι_mem_grade_one
Proof state after:
no goals
Theorem: DividedPowerAlgebra.deg_one_left_inv
Proof state before:
R : Type u_1
inst✝⁶ : CommRing R
M : Type u_2
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
inst✝³ : DecidableEq R
inst✝² : DecidableEq M
inst✝¹ : Module Rᵐᵒᵖ M
inst✝ : IsCentralScalar R M
⊢ LeftInverse (fun x => ((toTrivSqZeroExt R M) ↑x).snd) (⇑(proj' R M 1) ∘ ⇑(ι R M))
Tactic:
intro m
Proof state after:
R : Type u_1
inst✝⁶ : CommRing R
M : Type u_2
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
inst✝³ : DecidableEq R
inst✝² : DecidableEq M
inst✝¹ : Module Rᵐᵒᵖ M
inst✝ : IsCentralScalar R M
m : M
⊢ (fun x => ((toTrivSqZeroExt R M) ↑x).snd) ((⇑(proj' R M 1) ∘ ⇑(ι R M)) m) = m
Theorem: DividedPowerAlgebra.deg_one_left_inv
Proof state before:
R : Type u_1
inst✝⁶ : CommRing R
M : Type u_2
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
inst✝³ : DecidableEq R
inst✝² : DecidableEq M
inst✝¹ : Module Rᵐᵒᵖ M
inst✝ : IsCentralScalar R M
m : M
⊢ (fun x => ((toTrivSqZeroExt R M) ↑x).snd) ((⇑(proj' R M 1) ∘ ⇑(ι R M)) m) = m
Tactic:
simp only [proj', proj, LinearMap.coe_mk, AddHom.coe_mk, ι, Function.comp_apply]
Proof state after:
R : Type u_1
inst✝⁶ : CommRing R
M : Type u_2
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
inst✝³ : DecidableEq R
inst✝² : DecidableEq M
inst✝¹ : Module Rᵐᵒᵖ M
inst✝ : IsCentralScalar R M
m : M
⊢ ((toTrivSqZeroExt R M) ↑(((DirectSum.decompose (grade R M)) (dp R 1 m)) 1)).snd = m
Theorem: DividedPowerAlgebra.deg_one_left_inv
Proof state before:
R : Type u_1
inst✝⁶ : CommRing R
M : Type u_2
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
inst✝³ : DecidableEq R
inst✝² : DecidableEq M
inst✝¹ : Module Rᵐᵒᵖ M
inst✝ : IsCentralScalar R M
m : M
⊢ ((toTrivSqZeroExt R M) ↑(((DirectSum.decompose (grade R M)) (dp R 1 m)) 1)).snd = m
Tactic:
rw [← TrivSqZeroExt.snd_inr R m, ← ι_def]
Proof state after:
R : Type u_1
inst✝⁶ : CommRing R
M : Type u_2
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
inst✝³ : DecidableEq R
inst✝² : DecidableEq M
inst✝¹ : Module Rᵐᵒᵖ M
inst✝ : IsCentralScalar R M
m : M
⊢ ((toTrivSqZeroExt R M) ↑(((DirectSum.decompose (grade R M)) ((ι R M) (inr m).snd)) 1)).snd = (inr m).snd
Theorem: DividedPowerAlgebra.deg_one_left_inv
Proof state before:
R : Type u_1
inst✝⁶ : CommRing R
M : Type u_2
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
inst✝³ : DecidableEq R
inst✝² : DecidableEq M
inst✝¹ : Module Rᵐᵒᵖ M
inst✝ : IsCentralScalar R M
m : M
⊢ ((toTrivSqZeroExt R M) ↑(((DirectSum.decompose (grade R M)) ((ι R M) (inr m).snd)) 1)).snd = (inr m).snd
Tactic:
apply congr_arg
Proof state after:
case h
R : Type u_1
inst✝⁶ : CommRing R
M : Type u_2
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
inst✝³ : DecidableEq R
inst✝² : DecidableEq M
inst✝¹ : Module Rᵐᵒᵖ M
inst✝ : IsCentralScalar R M
m : M
⊢ (toTrivSqZeroExt R M) ↑(((DirectSum.decompose (grade R M)) ((ι R M) (inr m).snd)) 1) = inr m
Theorem: DividedPowerAlgebra.deg_one_left_inv
Proof state before:
case h
R : Type u_1
inst✝⁶ : CommRing R
M : Type u_2
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
inst✝³ : DecidableEq R
inst✝² : DecidableEq M
inst✝¹ : Module Rᵐᵒᵖ M
inst✝ : IsCentralScalar R M
m : M
⊢ (toTrivSqZeroExt R M) ↑(((DirectSum.decompose (grade R M)) ((ι R M) (inr m).snd)) 1) = inr m
Tactic:
rw [snd_inr, decompose_of_mem_same, toTrivSqZeroExt_ι]
Proof state after:
case h.hx
R : Type u_1
inst✝⁶ : CommRing R
M : Type u_2
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
inst✝³ : DecidableEq R
inst✝² : DecidableEq M
inst✝¹ : Module Rᵐᵒᵖ M
inst✝ : IsCentralScalar R M
m : M
⊢ (ι R M) m ∈ grade R M 1
Theorem: DividedPowerAlgebra.deg_one_left_inv
Proof state before:
case h.hx
R : Type u_1
inst✝⁶ : CommRing R
M : Type u_2
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
inst✝³ : DecidableEq R
inst✝² : DecidableEq M
inst✝¹ : Module Rᵐᵒᵖ M
inst✝ : IsCentralScalar R M
m : M
⊢ (ι R M) m ∈ grade R M 1
Tactic:
apply ι_mem_grade_one
Proof state after:
no goals
Theorem: DividedPowerAlgebra.ι_toTrivSqZeroExt_of_mem_grade_one
Proof state before:
R : Type u_1
inst✝⁶ : CommRing R
M : Type u_2
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
inst✝³ : DecidableEq R
inst✝² : DecidableEq M
inst✝¹ : Module Rᵐᵒᵖ M
inst✝ : IsCentralScalar R M
a : DividedPowerAlgebra R M
ha : a ∈ grade R M 1
⊢ (ι R M) ((sndHom R M) ((toTrivSqZeroExt R M) a)) = a
Tactic:
suffices ⟨(ι R M) ((sndHom R M) ((toTrivSqZeroExt R M) a)), ι_mem_grade_one R _⟩ =
  (⟨a, ha⟩ : grade R M 1) by
  simpa only [sndHom_apply, Subtype.mk.injEq] using this
Proof state after:
R : Type u_1
inst✝⁶ : CommRing R
M : Type u_2
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
inst✝³ : DecidableEq R
inst✝² : DecidableEq M
inst✝¹ : Module Rᵐᵒᵖ M
inst✝ : IsCentralScalar R M
a : DividedPowerAlgebra R M
ha : a ∈ grade R M 1
⊢ ⟨(ι R M) ((sndHom R M) ((toTrivSqZeroExt R M) a)), ⋯⟩ = ⟨a, ha⟩
Theorem: DividedPowerAlgebra.ι_toTrivSqZeroExt_of_mem_grade_one
Proof state before:
R : Type u_1
inst✝⁶ : CommRing R
M : Type u_2
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
inst✝³ : DecidableEq R
inst✝² : DecidableEq M
inst✝¹ : Module Rᵐᵒᵖ M
inst✝ : IsCentralScalar R M
a : DividedPowerAlgebra R M
ha : a ∈ grade R M 1
⊢ ⟨(ι R M) ((sndHom R M) ((toTrivSqZeroExt R M) a)), ⋯⟩ = ⟨a, ha⟩
Tactic:
apply (linearEquivDegreeOne R M).symm.injective
Proof state after:
case a
R : Type u_1
inst✝⁶ : CommRing R
M : Type u_2
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
inst✝³ : DecidableEq R
inst✝² : DecidableEq M
inst✝¹ : Module Rᵐᵒᵖ M
inst✝ : IsCentralScalar R M
a : DividedPowerAlgebra R M
ha : a ∈ grade R M 1
⊢ (linearEquivDegreeOne R M).symm ⟨(ι R M) ((sndHom R M) ((toTrivSqZeroExt R M) a)), ⋯⟩ =
    (linearEquivDegreeOne R M).symm ⟨a, ha⟩
Theorem: DividedPowerAlgebra.ι_toTrivSqZeroExt_of_mem_grade_one
Proof state before:
case a
R : Type u_1
inst✝⁶ : CommRing R
M : Type u_2
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
inst✝³ : DecidableEq R
inst✝² : DecidableEq M
inst✝¹ : Module Rᵐᵒᵖ M
inst✝ : IsCentralScalar R M
a : DividedPowerAlgebra R M
ha : a ∈ grade R M 1
⊢ (linearEquivDegreeOne R M).symm ⟨(ι R M) ((sndHom R M) ((toTrivSqZeroExt R M) a)), ⋯⟩ =
    (linearEquivDegreeOne R M).symm ⟨a, ha⟩
Tactic:
rw [← LinearEquiv.invFun_eq_symm]
Proof state after:
case a
R : Type u_1
inst✝⁶ : CommRing R
M : Type u_2
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
inst✝³ : DecidableEq R
inst✝² : DecidableEq M
inst✝¹ : Module Rᵐᵒᵖ M
inst✝ : IsCentralScalar R M
a : DividedPowerAlgebra R M
ha : a ∈ grade R M 1
⊢ (linearEquivDegreeOne R M).invFun ⟨(ι R M) ((sndHom R M) ((toTrivSqZeroExt R M) a)), ⋯⟩ =
    (linearEquivDegreeOne R M).invFun ⟨a, ha⟩
Theorem: DividedPowerAlgebra.ι_toTrivSqZeroExt_of_mem_grade_one
Proof state before:
case a
R : Type u_1
inst✝⁶ : CommRing R
M : Type u_2
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
inst✝³ : DecidableEq R
inst✝² : DecidableEq M
inst✝¹ : Module Rᵐᵒᵖ M
inst✝ : IsCentralScalar R M
a : DividedPowerAlgebra R M
ha : a ∈ grade R M 1
⊢ (linearEquivDegreeOne R M).invFun ⟨(ι R M) ((sndHom R M) ((toTrivSqZeroExt R M) a)), ⋯⟩ =
    (linearEquivDegreeOne R M).invFun ⟨a, ha⟩
Tactic:
simp only [linearEquivDegreeOne, toTrivSqZeroExt_ι, sndHom_apply, snd_inr]
Proof state after:
no goals
Theorem: DividedPowerAlgebra.ι_toTrivSqZeroExt_of_mem_grade_one
Proof state before:
R : Type u_1
inst✝⁶ : CommRing R
M : Type u_2
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
inst✝³ : DecidableEq R
inst✝² : DecidableEq M
inst✝¹ : Module Rᵐᵒᵖ M
inst✝ : IsCentralScalar R M
a : DividedPowerAlgebra R M
ha : a ∈ grade R M 1
this : ⟨(ι R M) ((sndHom R M) ((toTrivSqZeroExt R M) a)), ⋯⟩ = ⟨a, ha⟩
⊢ (ι R M) ((sndHom R M) ((toTrivSqZeroExt R M) a)) = a
Tactic:
simpa only [sndHom_apply, Subtype.mk.injEq] using this
Proof state after:
no goals
Theorem: DividedPowerAlgebra.mem_grade_one_iff
Proof state before:
R : Type u_1
inst✝⁶ : CommRing R
M : Type u_2
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
inst✝³ : DecidableEq R
inst✝² : DecidableEq M
inst✝¹ : Module Rᵐᵒᵖ M
inst✝ : IsCentralScalar R M
a : DividedPowerAlgebra R M
⊢ a ∈ grade R M 1 ↔ ∃ m, a = (ι R M) m
Tactic:
constructor
Proof state after:
case mp
R : Type u_1
inst✝⁶ : CommRing R
M : Type u_2
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
inst✝³ : DecidableEq R
inst✝² : DecidableEq M
inst✝¹ : Module Rᵐᵒᵖ M
inst✝ : IsCentralScalar R M
a : DividedPowerAlgebra R M
⊢ a ∈ grade R M 1 → ∃ m, a = (ι R M) m

case mpr
R : Type u_1
inst✝⁶ : CommRing R
M : Type u_2
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
inst✝³ : DecidableEq R
inst✝² : DecidableEq M
inst✝¹ : Module Rᵐᵒᵖ M
inst✝ : IsCentralScalar R M
a : DividedPowerAlgebra R M
⊢ (∃ m, a = (ι R M) m) → a ∈ grade R M 1
Theorem: DividedPowerAlgebra.mem_grade_one_iff
Proof state before:
case mp
R : Type u_1
inst✝⁶ : CommRing R
M : Type u_2
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
inst✝³ : DecidableEq R
inst✝² : DecidableEq M
inst✝¹ : Module Rᵐᵒᵖ M
inst✝ : IsCentralScalar R M
a : DividedPowerAlgebra R M
⊢ a ∈ grade R M 1 → ∃ m, a = (ι R M) m

case mpr
R : Type u_1
inst✝⁶ : CommRing R
M : Type u_2
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
inst✝³ : DecidableEq R
inst✝² : DecidableEq M
inst✝¹ : Module Rᵐᵒᵖ M
inst✝ : IsCentralScalar R M
a : DividedPowerAlgebra R M
⊢ (∃ m, a = (ι R M) m) → a ∈ grade R M 1
Tactic:
. intro ha
  use ((sndHom R M) ((toTrivSqZeroExt R M) a))
  rw [ι_toTrivSqZeroExt_of_mem_grade_one R M ha]
Proof state after:
case mpr
R : Type u_1
inst✝⁶ : CommRing R
M : Type u_2
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
inst✝³ : DecidableEq R
inst✝² : DecidableEq M
inst✝¹ : Module Rᵐᵒᵖ M
inst✝ : IsCentralScalar R M
a : DividedPowerAlgebra R M
⊢ (∃ m, a = (ι R M) m) → a ∈ grade R M 1
Theorem: DividedPowerAlgebra.mem_grade_one_iff
Proof state before:
case mpr
R : Type u_1
inst✝⁶ : CommRing R
M : Type u_2
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
inst✝³ : DecidableEq R
inst✝² : DecidableEq M
inst✝¹ : Module Rᵐᵒᵖ M
inst✝ : IsCentralScalar R M
a : DividedPowerAlgebra R M
⊢ (∃ m, a = (ι R M) m) → a ∈ grade R M 1
Tactic:
. rintro ⟨m, rfl⟩
  apply ι_mem_grade_one
Proof state after:
no goals
Theorem: DividedPowerAlgebra.mem_grade_one_iff
Proof state before:
case mp
R : Type u_1
inst✝⁶ : CommRing R
M : Type u_2
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
inst✝³ : DecidableEq R
inst✝² : DecidableEq M
inst✝¹ : Module Rᵐᵒᵖ M
inst✝ : IsCentralScalar R M
a : DividedPowerAlgebra R M
⊢ a ∈ grade R M 1 → ∃ m, a = (ι R M) m
Tactic:
intro ha
Proof state after:
case mp
R : Type u_1
inst✝⁶ : CommRing R
M : Type u_2
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
inst✝³ : DecidableEq R
inst✝² : DecidableEq M
inst✝¹ : Module Rᵐᵒᵖ M
inst✝ : IsCentralScalar R M
a : DividedPowerAlgebra R M
ha : a ∈ grade R M 1
⊢ ∃ m, a = (ι R M) m
Theorem: DividedPowerAlgebra.mem_grade_one_iff
Proof state before:
case mp
R : Type u_1
inst✝⁶ : CommRing R
M : Type u_2
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
inst✝³ : DecidableEq R
inst✝² : DecidableEq M
inst✝¹ : Module Rᵐᵒᵖ M
inst✝ : IsCentralScalar R M
a : DividedPowerAlgebra R M
ha : a ∈ grade R M 1
⊢ ∃ m, a = (ι R M) m
Tactic:
use ((sndHom R M) ((toTrivSqZeroExt R M) a))
Proof state after:
case h
R : Type u_1
inst✝⁶ : CommRing R
M : Type u_2
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
inst✝³ : DecidableEq R
inst✝² : DecidableEq M
inst✝¹ : Module Rᵐᵒᵖ M
inst✝ : IsCentralScalar R M
a : DividedPowerAlgebra R M
ha : a ∈ grade R M 1
⊢ a = (ι R M) ((sndHom R M) ((toTrivSqZeroExt R M) a))
Theorem: DividedPowerAlgebra.mem_grade_one_iff
Proof state before:
case h
R : Type u_1
inst✝⁶ : CommRing R
M : Type u_2
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
inst✝³ : DecidableEq R
inst✝² : DecidableEq M
inst✝¹ : Module Rᵐᵒᵖ M
inst✝ : IsCentralScalar R M
a : DividedPowerAlgebra R M
ha : a ∈ grade R M 1
⊢ a = (ι R M) ((sndHom R M) ((toTrivSqZeroExt R M) a))
Tactic:
rw [ι_toTrivSqZeroExt_of_mem_grade_one R M ha]
Proof state after:
no goals
Theorem: DividedPowerAlgebra.mem_grade_one_iff
Proof state before:
case mpr
R : Type u_1
inst✝⁶ : CommRing R
M : Type u_2
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
inst✝³ : DecidableEq R
inst✝² : DecidableEq M
inst✝¹ : Module Rᵐᵒᵖ M
inst✝ : IsCentralScalar R M
a : DividedPowerAlgebra R M
⊢ (∃ m, a = (ι R M) m) → a ∈ grade R M 1
Tactic:
rintro ⟨m, rfl⟩
Proof state after:
case mpr.intro
R : Type u_1
inst✝⁶ : CommRing R
M : Type u_2
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
inst✝³ : DecidableEq R
inst✝² : DecidableEq M
inst✝¹ : Module Rᵐᵒᵖ M
inst✝ : IsCentralScalar R M
m : M
⊢ (ι R M) m ∈ grade R M 1
Theorem: DividedPowerAlgebra.mem_grade_one_iff
Proof state before:
case mpr.intro
R : Type u_1
inst✝⁶ : CommRing R
M : Type u_2
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
inst✝³ : DecidableEq R
inst✝² : DecidableEq M
inst✝¹ : Module Rᵐᵒᵖ M
inst✝ : IsCentralScalar R M
m : M
⊢ (ι R M) m ∈ grade R M 1
Tactic:
apply ι_mem_grade_one
Proof state after:
no goals
Theorem: Finset.prod_one_add
Proof state before:
ι : Type u_1
α : Type u_2
inst✝¹ : DecidableEq ι
inst✝ : CommRing α
f : ι → α
s : Finset ι
⊢ ∏ i ∈ s, (1 + f i) = ∑ t ∈ s.powerset, t.prod f
Tactic:
simp_rw [add_comm, Finset.prod_add]
Proof state after:
ι : Type u_1
α : Type u_2
inst✝¹ : DecidableEq ι
inst✝ : CommRing α
f : ι → α
s : Finset ι
⊢ ∑ t ∈ s.powerset, (∏ i ∈ t, f i) * ∏ i ∈ s \ t, 1 = ∑ t ∈ s.powerset, t.prod f
Theorem: Finset.prod_one_add
Proof state before:
ι : Type u_1
α : Type u_2
inst✝¹ : DecidableEq ι
inst✝ : CommRing α
f : ι → α
s : Finset ι
⊢ ∑ t ∈ s.powerset, (∏ i ∈ t, f i) * ∏ i ∈ s \ t, 1 = ∑ t ∈ s.powerset, t.prod f
Tactic:
congr
Proof state after:
case e_f
ι : Type u_1
α : Type u_2
inst✝¹ : DecidableEq ι
inst✝ : CommRing α
f : ι → α
s : Finset ι
⊢ (fun t => (∏ i ∈ t, f i) * ∏ i ∈ s \ t, 1) = fun t => t.prod f
Theorem: Finset.prod_one_add
Proof state before:
case e_f
ι : Type u_1
α : Type u_2
inst✝¹ : DecidableEq ι
inst✝ : CommRing α
f : ι → α
s : Finset ι
⊢ (fun t => (∏ i ∈ t, f i) * ∏ i ∈ s \ t, 1) = fun t => t.prod f
Tactic:
ext t
Proof state after:
case e_f.h
ι : Type u_1
α : Type u_2
inst✝¹ : DecidableEq ι
inst✝ : CommRing α
f : ι → α
s t : Finset ι
⊢ (∏ i ∈ t, f i) * ∏ i ∈ s \ t, 1 = t.prod f