mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.LinearAlgebra.Matrix.Cartan

Goal state before:
pp: case «1».«1»
h : (fun i ↦ i) ⟨1, ⋯⟩ ≠ (fun i ↦ i) ⟨1, ⋯⟩
⊢ F₄ ((fun i ↦ i) ⟨1, ⋯⟩) ((fun i ↦ i) ⟨1, ⋯⟩) ≤ 0

Tactic:
simp_all [F₄]

Goal state after:
Module: Mathlib.LinearAlgebra.Matrix.Cartan

Goal state before:
pp: case «1».«2»
h : (fun i ↦ i) ⟨1, ⋯⟩ ≠ (fun i ↦ i) ⟨2, ⋯⟩
⊢ F₄ ((fun i ↦ i) ⟨1, ⋯⟩) ((fun i ↦ i) ⟨2, ⋯⟩) ≤ 0

Tactic:
simp_all [F₄]

Goal state after:
Module: Mathlib.LinearAlgebra.Matrix.Cartan

Goal state before:
pp: case «1».«3»
h : (fun i ↦ i) ⟨1, ⋯⟩ ≠ (fun i ↦ i) ⟨3, ⋯⟩
⊢ F₄ ((fun i ↦ i) ⟨1, ⋯⟩) ((fun i ↦ i) ⟨3, ⋯⟩) ≤ 0

Tactic:
simp_all [F₄]

Goal state after:
Module: Mathlib.LinearAlgebra.Matrix.Cartan

Goal state before:
pp: case «2».«0»
h : (fun i ↦ i) ⟨2, ⋯⟩ ≠ (fun i ↦ i) ⟨0, ⋯⟩
⊢ F₄ ((fun i ↦ i) ⟨2, ⋯⟩) ((fun i ↦ i) ⟨0, ⋯⟩) ≤ 0

Tactic:
simp_all [F₄]

Goal state after:
Module: Mathlib.LinearAlgebra.Matrix.Cartan

Goal state before:
pp: case «2».«1»
h : (fun i ↦ i) ⟨2, ⋯⟩ ≠ (fun i ↦ i) ⟨1, ⋯⟩
⊢ F₄ ((fun i ↦ i) ⟨2, ⋯⟩) ((fun i ↦ i) ⟨1, ⋯⟩) ≤ 0

Tactic:
simp_all [F₄]

Goal state after:
Module: Mathlib.LinearAlgebra.Matrix.Cartan

Goal state before:
pp: case «2».«2»
h : (fun i ↦ i) ⟨2, ⋯⟩ ≠ (fun i ↦ i) ⟨2, ⋯⟩
⊢ F₄ ((fun i ↦ i) ⟨2, ⋯⟩) ((fun i ↦ i) ⟨2, ⋯⟩) ≤ 0

Tactic:
simp_all [F₄]

Goal state after:
Module: Mathlib.LinearAlgebra.Matrix.Cartan

Goal state before:
pp: case «2».«3»
h : (fun i ↦ i) ⟨2, ⋯⟩ ≠ (fun i ↦ i) ⟨3, ⋯⟩
⊢ F₄ ((fun i ↦ i) ⟨2, ⋯⟩) ((fun i ↦ i) ⟨3, ⋯⟩) ≤ 0

Tactic:
simp_all [F₄]

Goal state after:
Module: Mathlib.LinearAlgebra.Matrix.Cartan

Goal state before:
pp: case «3».«0»
h : (fun i ↦ i) ⟨3, ⋯⟩ ≠ (fun i ↦ i) ⟨0, ⋯⟩
⊢ F₄ ((fun i ↦ i) ⟨3, ⋯⟩) ((fun i ↦ i) ⟨0, ⋯⟩) ≤ 0

Tactic:
simp_all [F₄]

Goal state after:
Module: Mathlib.LinearAlgebra.Matrix.Cartan

Goal state before:
pp: case «3».«1»
h : (fun i ↦ i) ⟨3, ⋯⟩ ≠ (fun i ↦ i) ⟨1, ⋯⟩
⊢ F₄ ((fun i ↦ i) ⟨3, ⋯⟩) ((fun i ↦ i) ⟨1, ⋯⟩) ≤ 0

Tactic:
simp_all [F₄]

Goal state after:
Module: Mathlib.LinearAlgebra.Matrix.Cartan

Goal state before:
pp: case «3».«2»
h : (fun i ↦ i) ⟨3, ⋯⟩ ≠ (fun i ↦ i) ⟨2, ⋯⟩
⊢ F₄ ((fun i ↦ i) ⟨3, ⋯⟩) ((fun i ↦ i) ⟨2, ⋯⟩) ≤ 0

Tactic:
simp_all [F₄]

Goal state after:
Module: Mathlib.LinearAlgebra.Matrix.Cartan

Goal state before:
pp: case «3».«3»
h : (fun i ↦ i) ⟨3, ⋯⟩ ≠ (fun i ↦ i) ⟨3, ⋯⟩
⊢ F₄ ((fun i ↦ i) ⟨3, ⋯⟩) ((fun i ↦ i) ⟨3, ⋯⟩) ≤ 0

Tactic:
simp_all [F₄]

Goal state after:
Module: Mathlib.RingTheory.FractionalIdeal.Inverse

Goal state before:
pp: K : Type u_3
inst✝⁴ : Field K
R₁ : Type u_6
inst✝³ : CommRing R₁
inst✝² : Algebra R₁ K
inst✝¹ : IsLocalization R₁⁰ K
I : FractionalIdeal R₁⁰ K
inst✝ : (↑I).IsPrincipal
h : I ≠ 0
generator_I_eq_zero : generator ↑I = 0
⊢ False

Tactic:
apply h

Goal state after:
K : Type u_3
inst✝⁴ : Field K
R₁ : Type u_6
inst✝³ : CommRing R₁
inst✝² : Algebra R₁ K
inst✝¹ : IsLocalization R₁⁰ K
I : FractionalIdeal R₁⁰ K
inst✝ : (↑I).IsPrincipal
h : I ≠ 0
generator_I_eq_zero : generator ↑I = 0
⊢ I = 0
Module: Mathlib.RingTheory.FractionalIdeal.Operations

Goal state before:
pp: R : Type u_1
inst✝² : CommRing R
S : Submonoid R
P : Type u_2
inst✝¹ : CommRing P
inst✝ : Algebra R P
I J : FractionalIdeal S P
x : P
hx : x ∈ I * J
⊢ x ∈ ↑I * ↑J

Tactic:
by simpa using mem_coe.mpr hx

Goal state after:
Module: Mathlib.RingTheory.FractionalIdeal.Operations

Goal state before:
pp: R : Type u_1
inst✝⁵ : CommRing R
S : Submonoid R
P : Type u_2
inst✝⁴ : CommRing P
inst✝³ : Algebra R P
R₁ : Type u_3
inst✝² : CommRing R₁
K : Type u_4
inst✝¹ : Field K
inst✝ : Algebra R₁ K
h : 0 = 1
⊢ 1 ∈ 0

Tactic:
rw [← (algebraMap R₁ K).map_one]
        simpa only [h] using coe_mem_one R₁⁰ 1

Goal state after:
Module: Mathlib.RingTheory.FractionalIdeal.Operations

Goal state before:
pp: R₁ : Type u_3
inst✝⁴ : CommRing R₁
K : Type u_4
inst✝³ : Field K
inst✝² : Algebra R₁ K
inst✝¹ : IsFractionRing R₁ K
inst✝ : IsDomain R₁
I : FractionalIdeal R₁⁰ K
⊢ I * (1 / I) ≤ 1

Tactic:
by_cases hI : I = 0
  · rw [hI, div_zero, mul_zero]
    exact zero_le 1
  · rw [← coe_le_coe, coe_mul, coe_div hI, coe_one]
    apply Submodule.mul_one_div_le_one

Goal state after:
Module: Mathlib.Algebra.Lie.Weights.IsSimple

Goal state before:
pp: K : Type u_1
L : Type u_2
inst✝⁷ : Field K
inst✝⁶ : CharZero K
inst✝⁵ : LieRing L
inst✝⁴ : LieAlgebra K L
inst✝³ : FiniteDimensional K L
inst✝² : IsKilling K L
H : LieSubalgebra K L
inst✝¹ : H.IsCartanSubalgebra
inst✝ : IsTriangularizable K (↥H) L
q : Submodule K (Dual K ↥H)
hq : ∀ (i : ↥LieSubalgebra.root), q ∈ End.invtSubmodule ↑((rootSystem H).reflection i)
χ : Weight K (↥H) L
x_χ m_α : L
hx_χ : x_χ ∈ genWeightSpace L ⇑χ
α : Weight K (↥H) L
hαq : Weight.toLinear K (↥H) L α ∈ q
hα₀ : α.IsNonZero
w_plus : Weight.toLinear K (↥H) L χ + Weight.toLinear K (↥H) L α ≠ 0
w_minus : Weight.toLinear K (↥H) L χ - Weight.toLinear K (↥H) L α ≠ 0
w_chi : Weight.toLinear K (↥H) L χ ≠ 0
m_pos m_neg : L
y : ↥H
hy : y ∈ corootSpace ⇑α
h_bracket_sum : ⁅x_χ, m_α⁆ = ⁅x_χ, m_pos⁆ + ⁅x_χ, m_neg⁆ + ⁅x_χ, ↑y⁆
h_pos_containment : ⁅x_χ, m_pos⁆ ∈ genWeightSpace L (⇑χ + ⇑α)
h_neg_containment : ⁅x_χ, m_neg⁆ ∈ genWeightSpace L (⇑χ - ⇑α)
h_chi_not_in_q : Weight.toLinear K (↥H) L χ ∉ q
S : RootPairing (↥LieSubalgebra.root) K (Dual K ↥H) ↥H := rootSystem H
exists_root_index : ∀ (γ : Weight K (↥H) L), γ.IsNonZero → ∃ i, S.root i = Weight.toLinear K (↥H) L γ
h_plus_ne_bot : ¬genWeightSpace L ⇑(Weight.toLinear K (↥H) L χ + Weight.toLinear K (↥H) L α) = ⊥
⊢ False

Tactic:
let γ : Weight K H L := ⟨χ.toLinear + α.toLinear, h_plus_ne_bot⟩

Goal state after:
K : Type u_1
L : Type u_2
inst✝⁷ : Field K
inst✝⁶ : CharZero K
inst✝⁵ : LieRing L
inst✝⁴ : LieAlgebra K L
inst✝³ : FiniteDimensional K L
inst✝² : IsKilling K L
H : LieSubalgebra K L
inst✝¹ : H.IsCartanSubalgebra
inst✝ : IsTriangularizable K (↥H) L
q : Submodule K (Dual K ↥H)
hq : ∀ (i : ↥LieSubalgebra.root), q ∈ End.invtSubmodule ↑((rootSystem H).reflection i)
χ : Weight K (↥H) L
x_χ m_α : L
hx_χ : x_χ ∈ genWeightSpace L ⇑χ
α : Weight K (↥H) L
hαq : Weight.toLinear K (↥H) L α ∈ q
hα₀ : α.IsNonZero
w_plus : Weight.toLinear K (↥H) L χ + Weight.toLinear K (↥H) L α ≠ 0
w_minus : Weight.toLinear K (↥H) L χ - Weight.toLinear K (↥H) L α ≠ 0
w_chi : Weight.toLinear K (↥H) L χ ≠ 0
m_pos m_neg : L
y : ↥H
hy : y ∈ corootSpace ⇑α
h_bracket_sum : ⁅x_χ, m_α⁆ = ⁅x_χ, m_pos⁆ + ⁅x_χ, m_neg⁆ + ⁅x_χ, ↑y⁆
h_pos_containment : ⁅x_χ, m_pos⁆ ∈ genWeightSpace L (⇑χ + ⇑α)
h_neg_containment : ⁅x_χ, m_neg⁆ ∈ genWeightSpace L (⇑χ - ⇑α)
h_chi_not_in_q : Weight.toLinear K (↥H) L χ ∉ q
S : RootPairing (↥LieSubalgebra.root) K (Dual K ↥H) ↥H := rootSystem H
exists_root_index : ∀ (γ : Weight K (↥H) L), γ.IsNonZero → ∃ i, S.root i = Weight.toLinear K (↥H) L γ
h_plus_ne_bot : ¬genWeightSpace L ⇑(Weight.toLinear K (↥H) L χ + Weight.toLinear K (↥H) L α) = ⊥
γ : Weight K (↥H) L :=
  { toFun := ⇑(Weight.toLinear K (↥H) L χ) + ⇑(Weight.toLinear K (↥H) L α), genWeightSpace_ne_bot' := h_plus_ne_bot }
⊢ False
Module: Mathlib.RingTheory.DedekindDomain.Ideal.Lemmas

Goal state before:
pp: A : Type u_2
inst✝¹ : CommRing A
inst✝ : IsDedekindDomain A
I J K : Ideal A
⊢ I * (J ⊓ K) = I * J ⊓ I * K

Tactic:
rw [inf_eq_iInf, mul_iInf, inf_eq_iInf]
  congr! 2 with ⟨⟩

Goal state after:
Module: Mathlib.RingTheory.DedekindDomain.Ideal.Lemmas

Goal state before:
pp: T : Type u_4
inst✝³ : CommRing T
inst✝² : IsDedekindDomain T
R : Type u_5
inst✝¹ : CommRing R
inst✝ : IsDedekindDomain R
f : T ≃+* R
I : Ideal T
hI : Prime I
h : I ≠ ⊥
⊢ Prime (map f I)

Tactic:
rw [prime_iff_isPrime h] at hI

Goal state after:
T : Type u_4
inst✝³ : CommRing T
inst✝² : IsDedekindDomain T
R : Type u_5
inst✝¹ : CommRing R
inst✝ : IsDedekindDomain R
f : T ≃+* R
I : Ideal T
hI : I.IsPrime
h : I ≠ ⊥
⊢ Prime (map f I)
Module: Mathlib.Algebra.Module.LinearMap.Index

Goal state before:
pp: M : Type u_1
inst✝³ : AddCommGroup M
R : Type u_3
inst✝² : Ring R
inst✝¹ : Module R M
inst✝ : StrongRankCondition R
a✝ : Nontrivial R
⊢ id.index = 0

Tactic:
rw [index_eq_finrank_sub, range_id]

Goal state after:
M : Type u_1
inst✝³ : AddCommGroup M
R : Type u_3
inst✝² : Ring R
inst✝¹ : Module R M
inst✝ : StrongRankCondition R
a✝ : Nontrivial R
⊢ ↑(finrank R ↥id.ker) - ↑(finrank R (M ⧸ ⊤)) = 0
Module: Mathlib.RingTheory.DedekindDomain.Ideal.Lemmas

Goal state before:
pp: R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : IsPrincipalIdealRing R
a : R
⊢ Squarefree (span {a}) ↔ Squarefree a

Tactic:
refine ⟨fun h x hx ↦ ?_, fun h I hI ↦ ?_⟩

Goal state after:
case refine_1
R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : IsPrincipalIdealRing R
a : R
h : Squarefree (span {a})
x : R
hx : x * x ∣ a
⊢ IsUnit x

case refine_2
R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : IsPrincipalIdealRing R
a : R
h : Squarefree a
I : Ideal R
hI : I * I ∣ span {a}
⊢ IsUnit I
Module: Mathlib.RingTheory.DedekindDomain.Ideal.Lemmas

Goal state before:
pp: R : Type u_1
inst✝³ : CommRing R
inst✝² : IsDomain R
inst✝¹ : IsPrincipalIdealRing R
inst✝ : NormalizationMonoid R
a b : R
ha : a ∈ normalizedFactors b
hb : ¬b = 0
this : Prime (span {a})
⊢ span {a} ∈ normalizedFactors (span {b})

Tactic:
obtain ⟨c, hc, hc'⟩ := exists_mem_normalizedFactors_of_dvd ?_ this.irreducible
          (dvd_iff_le.mpr (span_singleton_le_span_singleton.mpr (dvd_of_mem_normalizedFactors ha)))
      rwa [associated_iff_eq.mp hc']

Goal state after:
Module: Mathlib.Algebra.Module.Presentation.Cokernel

Goal state before:
pp: A : Type u
inst✝⁸ : Ring A
M₁ : Type v₁
M₂ : Type v₂
M₃ : Type v₃
inst✝⁷ : AddCommGroup M₁
inst✝⁶ : Module A M₁
inst✝⁵ : AddCommGroup M₂
inst✝⁴ : Module A M₂
inst✝³ : AddCommGroup M₃
inst✝² : Module A M₃
pres₂ : Presentation A M₂
f : M₁ →ₗ[A] M₂
ι : Type w₁
g₁ : ι → M₁
data : pres₂.CokernelData f g₁
hg₁ : Submodule.span A (Set.range g₁) = ⊤
N✝ : Type w
inst✝¹ : AddCommGroup N✝
inst✝ : Module A N✝
f✝ f'✝ : M₂ ⧸ f.range →ₗ[A] N✝
h : (pres₂.cokernelSolution data).postcomp f✝ = (pres₂.cokernelSolution data).postcomp f'✝
⊢ f✝ = f'✝

Tactic:
ext : 1

Goal state after:
A : Type u
inst✝⁸ : Ring A
M₁ : Type v₁
M₂ : Type v₂
M₃ : Type v₃
inst✝⁷ : AddCommGroup M₁
inst✝⁶ : Module A M₁
inst✝⁵ : AddCommGroup M₂
inst✝⁴ : Module A M₂
inst✝³ : AddCommGroup M₃
inst✝² : Module A M₃
pres₂ : Presentation A M₂
f : M₁ →ₗ[A] M₂
ι : Type w₁
g₁ : ι → M₁
data : pres₂.CokernelData f g₁
hg₁ : Submodule.span A (Set.range g₁) = ⊤
N✝ : Type w
inst✝¹ : AddCommGroup N✝
inst✝ : Module A N✝
f✝ f'✝ : M₂ ⧸ f.range →ₗ[A] N✝
h : (pres₂.cokernelSolution data).postcomp f✝ = (pres₂.cokernelSolution data).postcomp f'✝
⊢ f✝ ∘ₗ f.range.mkQ = f'✝ ∘ₗ f.range.mkQ
Module: Mathlib.Algebra.MvPolynomial.Supported

Goal state before:
pp: σ : Type u_1
R : Type u
inst✝¹ : CommSemiring R
s t : Set σ
inst✝ : Nontrivial R
⊢ supported R s ≤ supported R t ↔ s ⊆ t

Tactic:
constructor
  · intro h i
    simpa using @h (X i)
  · exact supported_mono

Goal state after:
Module: Mathlib.Algebra.Polynomial.Derivation

Goal state before:
pp: R : Type u_1
inst✝ : CommSemiring R
⊢ (mkDerivation R) 1 = derivative'

Tactic:
ext : 1

Goal state after:
R : Type u_1
inst✝ : CommSemiring R
⊢ ((mkDerivation R) 1) X = derivative' X
Module: Mathlib.Algebra.Module.Presentation.RestrictScalars

Goal state before:
pp: case single_add
B : Type u_1
inst✝⁸ : Ring B
M : Type u_2
inst✝⁷ : AddCommGroup M
inst✝⁶ : Module B M
inst✝⁵ : DecidableEq B
presM : Presentation B M
inst✝⁴ : DecidableEq presM.G
A : Type u_3
inst✝³ : CommRing A
inst✝² : Algebra A B
inst✝¹ : Module A M
inst✝ : IsScalarTower A B M
presB : Presentation A B
data : presM.RestrictScalarsData presB
v : presM.R →₀ B
⊢ ∀ (a : presM.R) (b : B) (f : presM.R →₀ B),
    a ∉ f.support →
      b ≠ 0 →
        f ∈ Submodule.span A (Set.range fun x ↦ presB.var x.1 • Finsupp.single x.2 1) →
          Finsupp.single a b + f ∈ Submodule.span A (Set.range fun x ↦ presB.var x.1 • Finsupp.single x.2 1)

Tactic:
intro r b w _ _ hw
        refine Submodule.add_mem _ ?_ hw
        obtain ⟨β, rfl⟩ := presB.surjective_π b
        apply Finsupp.induction (motive := fun β ↦ Finsupp.single r (presB.π β) ∈ _)
        · simp
        · intro g a f _ _ hf
          rw [map_add, Finsupp.single_add]
          refine Submodule.add_mem _ ?_ hf
          rw [← Finsupp.smul_single_one, ← Finsupp.smul_single_one,
            map_smul, Relations.Solution.π_single, smul_assoc]
          exact Submodule.smul_mem _ _ (Submodule.subset_span ⟨⟨g, r⟩, rfl⟩)

Goal state after:
Module: Mathlib.Algebra.Module.Presentation.Tensor

Goal state before:
pp: A : Type u
inst✝⁶ : CommRing A
M₁ : Type v₁
M₂ : Type v₂
inst✝⁵ : AddCommGroup M₁
inst✝⁴ : AddCommGroup M₂
inst✝³ : Module A M₁
inst✝² : Module A M₂
relations₁ : Relations A
relations₂ : Relations A
solution₁ : relations₁.Solution M₁
solution₂ : relations₂.Solution M₂
h₁ : solution₁.IsPresentation
h₂ : solution₂.IsPresentation
N✝ : Type w
inst✝¹ : AddCommGroup N✝
inst✝ : Module A N✝
s : (relations₁.tensor relations₂).Solution N✝
r₁ : relations₁.R
⊢ solution₂.postcomp
      ((Finsupp.linearCombination A fun g₁ ↦
          h₂.desc { var := fun g₂ ↦ s.var (g₁, g₂), linearCombination_var_relation := ⋯ })
        (relations₁.relation r₁)) =
    solution₂.postcomp 0

Tactic:
by
        ext g₂
        dsimp
        erw [Finsupp.apply_linearCombination A (LinearMap.applyₗ (solution₂.var g₂))]
        have := s.linearCombination_var_relation (.inl ⟨r₁, g₂⟩)
        erw [Finsupp.linearCombination_embDomain] at this
        convert! this
        ext g₁
        simp

Goal state after:
Module: Mathlib.RingTheory.Flat.EquationalCriterion

Goal state before:
pp: R : Type u_1
M : Type u_2
inst✝⁴ : CommRing R
inst✝³ : AddCommGroup M
inst✝² : Module R M
ι : Type u_3
inst✝¹ : Fintype ι
f : ι → R
x : ι → M
κ : Type u_4
inst✝ : Fintype κ
e : κ ≃ ι
⊢ IsTrivialRelation (f ∘ ⇑e) (x ∘ ⇑e) ↔ IsTrivialRelation f x

Tactic:
simp_rw [isTrivialRelation_iff_vanishesTrivially, e.vanishesTrivially_comp]

Goal state after:
Module: Mathlib.RingTheory.Extension.Cotangent.Basic

Goal state before:
pp: R : Type u
S : Type v
inst✝¹⁰ : CommRing R
inst✝⁹ : CommRing S
inst✝⁸ : Algebra R S
P : Extension R S
R' : Type u'
S' : Type v'
inst✝⁷ : CommRing R'
inst✝⁶ : CommRing S'
inst✝⁵ : Algebra R' S'
P' : Extension R' S'
inst✝⁴ : Algebra R R'
inst✝³ : Algebra S S'
inst✝² : Algebra R S'
inst✝¹ : IsScalarTower R R' S'
inst✝ : IsScalarTower R S S'
f g : P.Hom P'
⊢ map f - map g = f.sub g ∘ₗ P.cotangentComplex

Tactic:
by
  ext x
  obtain ⟨x, rfl⟩ := mk_surjective x
  simp only [LinearMap.sub_apply, map_mk, LinearMap.coe_comp, Function.comp_apply,
    cotangentComplex_mk, Hom.sub_tmul, one_smul, val_mk]
  apply (Ideal.cotangentEquivIdeal _).injective
  ext
  simp only [val_sub, val_mk, map_sub, AddSubgroupClass.coe_sub, Ideal.cotangentEquivIdeal_apply,
    Ideal.toCotangent_to_quotient_square, Submodule.mkQ_apply, Ideal.Quotient.mk_eq_mk,
    Hom.subToKer_apply_coe, Hom.toAlgHom_apply]

Goal state after:
Module: Mathlib.LinearAlgebra.TensorProduct.Vanishing

Goal state before:
pp: R : Type u_1
inst✝⁵ : CommRing R
M : Type u_2
inst✝⁴ : AddCommGroup M
inst✝³ : Module R M
N : Type u_3
inst✝² : AddCommGroup N
inst✝¹ : Module R N
ι : Type u_4
inst✝ : Fintype ι
m : ι → M
n : ι → N
hm : Injective ⇑(rTensor N (span R (Set.range m)).subtype)
hmn : ∑ i, m i ⊗ₜ[R] n i = 0
⊢ VanishesTrivially R m n

Tactic:
have mem_M' i : m i ∈ span R (Set.range m) := subset_span ⟨i, rfl⟩
  set m' : ι → span R (Set.range m) := Subtype.coind m mem_M' with m'_eq
  have hm' : span R (Set.range m') = ⊤ := by
    apply map_injective_of_injective (injective_subtype (span R (Set.range m)))
    rw [Submodule.map_span, Submodule.map_top, range_subtype, coe_subtype, ← Set.range_comp]
    rfl
  have hm'n : ∑ i, m' i ⊗ₜ n i = (0 : span R (Set.range m) ⊗[R] N) := by
    apply hm
    simp only [m'_eq, map_sum, rTensor_tmul, coe_subtype, Subtype.coind_coe, map_zero, hmn]
  have : VanishesTrivially R m' n := vanishesTrivially_of_sum_tmul_eq_zero R hm' hm'n
  unfold VanishesTrivially at this ⊢
  convert! this with κ _ a y j
  convert! (injective_iff_map_eq_zero' _).mp (injective_subtype (span R (Set.range m))) _
  simp [m'_eq]

Goal state after:
Module: Mathlib.RingTheory.Extension.Cotangent.Basic

Goal state before:
pp: R : Type u
S : Type v
inst✝¹⁰ : CommRing R
inst✝⁹ : CommRing S
inst✝⁸ : Algebra R S
ι : Type w
P : Generators R S ι
R' : Type u'
S' : Type v'
ι' : Type w'
inst✝⁷ : CommRing R'
inst✝⁶ : CommRing S'
inst✝⁵ : Algebra R' S'
P' : Generators R' S' ι'
inst✝⁴ : Algebra R R'
inst✝³ : Algebra S S'
inst✝² : Algebra R S'
inst✝¹ : IsScalarTower R R' S'
inst✝ : IsScalarTower R S S'
f : P.Hom P'
i : ι
j : ι'
⊢ (P'.cotangentSpaceBasis.repr
        (1 ⊗ₜ[{ Ring := P'.Ring, commRing := AddMonoidAlgebra.commRing, algebra₁ := AddMonoidAlgebra.algebra,
              algebra₂ := P'.instRing, isScalarTower := ⋯, σ := P'.σ, algebraMap_σ := ⋯ }.Ring]
          (D R'
              { Ring := P'.Ring, commRing := AddMonoidAlgebra.commRing, algebra₁ := AddMonoidAlgebra.algebra,
                  algebra₂ := P'.instRing, isScalarTower := ⋯, σ := P'.σ, algebraMap_σ := ⋯ }.Ring)
            (f.toExtensionHom.toAlgHom (X i))))
      j =
    (aeval P'.val) ((pderiv j) (f.val i))

Tactic:
erw [cotangentSpaceBasis_repr_one_tmul, Hom.toAlgHom_X]

Goal state after:
Module: Mathlib.RingTheory.Localization.Finiteness

Goal state before:
pp: R : Type u_1
inst✝⁷ : CommSemiring R
M : Submonoid R
R' : Type u_3
inst✝⁶ : CommSemiring R'
inst✝⁵ : Algebra R R'
N : Type u_5
inst✝⁴ : AddCommMonoid N
inst✝³ : Module R N
inst✝² : Module R' N
inst✝¹ : IsScalarTower R R' N
inst✝ : IsLocalization M R'
x : N
s' : Finset N
hs' : x ∈ Submodule.span R' ↑s'
⊢ ∃ t, t • x ∈ Submodule.span R ↑s'

Tactic:
induction s' using Finset.induction_on generalizing x with

Goal state after:
Module: Mathlib.LinearAlgebra.Alternating.Uncurry.Fin

Goal state before:
pp: R : Type u_1
M : Type u_2
M₂ : Type u_3
N : Type u_4
N₂ : Type u_5
inst✝⁸ : CommRing R
inst✝⁷ : AddCommGroup M
inst✝⁶ : AddCommGroup M₂
inst✝⁵ : AddCommGroup N
inst✝⁴ : AddCommGroup N₂
inst✝³ : Module R M
inst✝² : Module R M₂
inst✝¹ : Module R N
inst✝ : Module R N₂
n : ℕ
f : M →ₗ[R] M [⋀^Fin n]→ₗ[R] N
⊢ ∀ (v : Fin (n + 1) → M) (i j : Fin (n + 1)),
    v i = v j → i ≠ j → (∑ p, (-1) ^ ↑p • LinearMap.uncurryMid p (toMultilinearMapLM ∘ₗ f)).toFun v = 0

Tactic:
by
    intro v i j hvij hij
    suffices ∑ k : Fin (n + 1), (-1) ^ (k : ℕ) • f (v k) (k.removeNth v) = 0 by simpa
    calc
      _ = (-1) ^ (i : ℕ) • f (v i) (i.removeNth v) + (-1) ^ (j : ℕ) • f (v j) (j.removeNth v) := by
        refine Fintype.sum_eq_add _ _ hij fun k ⟨hki, hkj⟩ ↦ ?_
        rcases exists_succAbove_eq hki.symm with ⟨i, rfl⟩
        rcases exists_succAbove_eq hkj.symm with ⟨j, rfl⟩
        rw [(f (v k)).map_eq_zero_of_eq _ hvij (ne_of_apply_ne _ hij), smul_zero]
      _ = 0 := by
        rw [hvij, neg_one_pow_smul_map_removeNth_add_eq_zero_of_eq] <;> assumption

Goal state after:
Module: Mathlib.LinearAlgebra.ExteriorPower.Pairing

Goal state before:
pp: R : Type u_1
M : Type u_2
inst✝³ : CommRing R
inst✝² : AddCommGroup M
inst✝¹ : Module R M
ι : Type u_3
inst✝ : LinearOrder ι
x : ι → M
f : ι → Module.Dual R M
h₀ : ∀ ⦃i j : ι⦄, i ≠ j → (f i) (x j) = 0
n : ℕ
a b : Fin n ↪o ι
h : a ≠ b
σ : Equiv.Perm (Fin n)
x✝ : σ ∈ Finset.univ
h' : ¬∏ i, (f (a i)) (x (b (σ i))) = 0
⊢ False

Tactic:
apply h

Goal state after:
R : Type u_1
M : Type u_2
inst✝³ : CommRing R
inst✝² : AddCommGroup M
inst✝¹ : Module R M
ι : Type u_3
inst✝ : LinearOrder ι
x : ι → M
f : ι → Module.Dual R M
h₀ : ∀ ⦃i j : ι⦄, i ≠ j → (f i) (x j) = 0
n : ℕ
a b : Fin n ↪o ι
h : a ≠ b
σ : Equiv.Perm (Fin n)
x✝ : σ ∈ Finset.univ
h' : ¬∏ i, (f (a i)) (x (b (σ i))) = 0
⊢ a = b
Module: Mathlib.LinearAlgebra.ExteriorPower.Basis

Goal state before:
pp: K : Type u_2
E : Type u_4
n : ℕ
inst✝³ : Field K
inst✝² : AddCommGroup E
inst✝¹ : Module K E
I : Type u_5
inst✝ : LinearOrder I
v : I → E
hv : LinearIndependent K v
W : Submodule K E := Submodule.span K (range v)
b : Basis I K ↥W
hb : v = ⇑W.subtype ∘ ⇑b
⊢ LinearIndependent (ι := ↑(powersetCard I n)) K (⇑(map n W.subtype) ∘ ιMulti_family K n ⇑b)

Tactic:
exact LinearIndependent.map' (coe_basis K n b ▸ (b.exteriorPower n).linearIndependent)
      _ (LinearMap.ker_eq_bot.mpr (map_injective_field (Submodule.subtype_injective _)))

Goal state after:
Module: Mathlib.LinearAlgebra.LinearDisjoint

Goal state before:
pp: R : Type u
S : Type v
inst✝³ : CommRing R
inst✝² : Ring S
inst✝¹ : Algebra R S
M N : Submodule R S
H : M.LinearDisjoint N
inst✝ : Flat R ↥N
ι : Type u_1
m : ι → ↥M
hm : LinearIndependent R m
⊢ Function.Injective ⇑(mulLeftMap N m)

Tactic:
classical simp_rw [mulLeftMap_eq_mulMap_comp, LinearMap.coe_comp, LinearEquiv.coe_coe,
    ← Function.comp_assoc, EquivLike.injective_comp]

Goal state after:
R : Type u
S : Type v
inst✝³ : CommRing R
inst✝² : Ring S
inst✝¹ : Algebra R S
M N : Submodule R S
H : M.LinearDisjoint N
inst✝ : Flat R ↥N
ι : Type u_1
m : ι → ↥M
hm : LinearIndependent R m
⊢ Function.Injective (⇑(M.mulMap N) ∘ ⇑(LinearMap.rTensor (↥N) (Finsupp.linearCombination R m)))
Module: Mathlib.LinearAlgebra.LinearDisjoint

Goal state before:
pp: R : Type u
S : Type v
inst✝⁴ : CommRing R
inst✝³ : Ring S
inst✝² : Algebra R S
M N : Submodule R S
H : M.LinearDisjoint N
inst✝¹ : Nontrivial R
inst✝ : Flat R ↥M
a b : ↥(M ⊓ N)
hc : Commute ↑a ↑b
h : LinearIndependent R ![a, b]
n : Fin 2 → ↥N := ⇑(inclusion ⋯) ∘ ![a, b]
hn : LinearIndependent R n
this : AddCommGroup (Fin 2 →₀ ↥M) := Finsupp.instAddCommGroup
m : Fin 2 →₀ ↥M := Finsupp.single 0 ⟨↑b, ⋯⟩ - Finsupp.single 1 ⟨↑a, ⋯⟩
hm : m = 0
⊢ False

Tactic:
simp only [Fin.isValue, sub_eq_zero, Finsupp.single_eq_single_iff, zero_ne_one, Subtype.mk.injEq,
    SetLike.coe_eq_coe, false_and, false_or, m] at hm

Goal state after:
R : Type u
S : Type v
inst✝⁴ : CommRing R
inst✝³ : Ring S
inst✝² : Algebra R S
M N : Submodule R S
H : M.LinearDisjoint N
inst✝¹ : Nontrivial R
inst✝ : Flat R ↥M
a b : ↥(M ⊓ N)
hc : Commute ↑a ↑b
h : LinearIndependent R ![a, b]
n : Fin 2 → ↥N := ⇑(inclusion ⋯) ∘ ![a, b]
hn : LinearIndependent R n
this : AddCommGroup (Fin 2 →₀ ↥M) := Finsupp.instAddCommGroup
m : Fin 2 →₀ ↥M := Finsupp.single 0 ⟨↑b, ⋯⟩ - Finsupp.single 1 ⟨↑a, ⋯⟩
hm : ⟨↑b, ⋯⟩ = 0 ∧ ⟨↑a, ⋯⟩ = 0
⊢ False
Module: Mathlib.LinearAlgebra.PiTensorProduct.Basic

Goal state before:
pp: ι : Type u_1
ι₂ : Type u_2
R : Type u_4
inst✝² : CommSemiring R
M : Type u_8
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
e : ι ≃ ι₂
⊢ (reindex R (fun x ↦ M) e).symm = reindex R (fun x ↦ M) e.symm

Tactic:
ext x
  simp [reindex]

Goal state after:
Module: Mathlib.RingTheory.Ideal.AssociatedPrime.Basic

Goal state before:
pp: case neg
R : Type u_1
inst✝⁶ : CommSemiring R
M : Type u_2
inst✝⁵ : AddCommMonoid M
inst✝⁴ : Module R M
M' : Type u_3
inst✝³ : AddCommMonoid M'
inst✝² : Module R M'
f : M →ₗ[R] M'
M'' : Type u_4
inst✝¹ : AddCommMonoid M''
inst✝ : Module R M''
g : M' →ₗ[R] M''
hf : Function.Injective ⇑f
hfg : Function.Exact ⇑f ⇑g
p : Ideal R
toIsPrime✝ : p.IsPrime
x : M'
hx : p = (⊥.colon {x}).radical
h : ∀ a ∈ p.primeCompl, ∀ (y : M) (k : ℕ), f y ≠ a ^ k • x
⊢ p ∈ associatedPrimes R M ∪ associatedPrimes R M''

Tactic:
right
    refine ⟨‹_›, g x, le_antisymm (fun b hb ↦ ?_) (fun b ⟨n, hb⟩ ↦ ?_)⟩
    · rw [hx] at hb
      refine Ideal.radical_mono (fun b hb ↦ ?_) hb
      rw [mem_colon_singleton, mem_bot] at hb ⊢
      rw [← map_smul, hb, map_zero]
    · rw [mem_colon_singleton, mem_bot, ← map_smul, ← LinearMap.mem_ker,
        hfg.linearMap_ker_eq] at hb
      obtain ⟨y, hy⟩ := hb
      by_contra H
      exact h b H y n hy

Goal state after: