mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Data.Fintype.Quotient

Goal state before:
pp: ι : Type u_1
inst✝ : DecidableEq ι
α : ι → Sort u_2
S : (i : ι) → Setoid (α i)
l✝ : List ι
i : ι
l : List ι
C : ((i_1 : ι) → i_1 ∈ i :: l → Quotient (S i_1)) → Prop
f : ∀ (a : (i_1 : ι) → i_1 ∈ i :: l → α i_1), C fun x1 x2 ↦ ⟦a x1 x2⟧
q : (i_1 : ι) → i_1 ∈ i :: l → Quotient (S i_1)
⊢ C (List.Pi.cons i l (List.Pi.head q) (List.Pi.tail q))

Tactic:
induction List.Pi.head q using Quotient.ind with | _ a
     =>  _ 

Goal state after:
case a
ι : Type u_1
inst✝ : DecidableEq ι
α : ι → Sort u_2
S : (i : ι) → Setoid (α i)
l✝ : List ι
i : ι
l : List ι
C : ((i_1 : ι) → i_1 ∈ i :: l → Quotient (S i_1)) → Prop
f : ∀ (a : (i_1 : ι) → i_1 ∈ i :: l → α i_1), C fun x1 x2 ↦ ⟦a x1 x2⟧
q : (i_1 : ι) → i_1 ∈ i :: l → Quotient (S i_1)
a : α i
⊢ C (List.Pi.cons i l ⟦a⟧ (List.Pi.tail q))
Module: Mathlib.Data.DFinsupp.Sigma

Goal state before:
pp: case inl.inr
ι : Type u
γ : Type w
β : ι → Type v
β₁ : ι → Type v₁
β₂ : ι → Type v₂
κ : Type u_1
α : ι → Type u_2
δ : (i : ι) → α i → Type v
inst✝¹ : DecidableEq ι
inst✝ : (i : ι) → (j : α i) → Zero (δ i j)
f : Π₀ (i : ι) (j : α i), δ i j
s : { s // ∀ (i : ι), i ∈ s ∨ f.toFun i = 0 }
fs : (i : ↥(↑s).toFinset) → { s_1 // ∀ (i_1 : α ↑i), i_1 ∈ s_1 ∨ (f ↑i).toFun i_1 = 0 }
i : ι
a : α i
hi : i ∈ ↑s
ha : (f ↑⟨i, ⋯⟩).toFun a = 0
⊢ (⟨i, a⟩ ∈ (↑s).toFinset.attach.val.bind fun i ↦ Multiset.map (Sigma.mk ↑i) ↑(fs i)) ∨ (f ⟨i, a⟩.fst) ⟨i, a⟩.snd = 0

Tactic:
right; simp [toFun_eq_coe (f i) ▸ ha]

Goal state after:
Module: Mathlib.LinearAlgebra.DFinsupp

Goal state before:
pp: ι : Type u_1
R : Type u_3
N : Type u_6
inst✝³ : Semiring R
inst✝² : AddCommMonoid N
inst✝¹ : Module R N
inst✝ : DecidableEq ι
p : ι → Submodule R N
⊢ iSup p = ((lsum ℕ) fun i ↦ (p i).subtype).range

Tactic:
apply le_antisymm

Goal state after:
case a
ι : Type u_1
R : Type u_3
N : Type u_6
inst✝³ : Semiring R
inst✝² : AddCommMonoid N
inst✝¹ : Module R N
inst✝ : DecidableEq ι
p : ι → Submodule R N
⊢ iSup p ≤ ((lsum ℕ) fun i ↦ (p i).subtype).range

case a
ι : Type u_1
R : Type u_3
N : Type u_6
inst✝³ : Semiring R
inst✝² : AddCommMonoid N
inst✝¹ : Module R N
inst✝ : DecidableEq ι
p : ι → Submodule R N
⊢ ((lsum ℕ) fun i ↦ (p i).subtype).range ≤ iSup p
Module: Mathlib.LinearAlgebra.DFinsupp

Goal state before:
pp: ι : Type u_1
R : Type u_3
N : Type u_6
inst✝⁴ : Semiring R
inst✝³ : AddCommMonoid N
inst✝² : Module R N
inst✝¹ : DecidableEq ι
p : ι → Prop
inst✝ : DecidablePred p
S : ι → Submodule R N
⊢ ⨆ i, ⨆ (_ : p i), S i = (((lsum ℕ) fun i ↦ (S i).subtype) ∘ₗ filterLinearMap R (fun i ↦ ↥(S i)) p).range

Tactic:
apply le_antisymm

Goal state after:
case a
ι : Type u_1
R : Type u_3
N : Type u_6
inst✝⁴ : Semiring R
inst✝³ : AddCommMonoid N
inst✝² : Module R N
inst✝¹ : DecidableEq ι
p : ι → Prop
inst✝ : DecidablePred p
S : ι → Submodule R N
⊢ ⨆ i, ⨆ (_ : p i), S i ≤ (((lsum ℕ) fun i ↦ (S i).subtype) ∘ₗ filterLinearMap R (fun i ↦ ↥(S i)) p).range

case a
ι : Type u_1
R : Type u_3
N : Type u_6
inst✝⁴ : Semiring R
inst✝³ : AddCommMonoid N
inst✝² : Module R N
inst✝¹ : DecidableEq ι
p : ι → Prop
inst✝ : DecidablePred p
S : ι → Submodule R N
⊢ (((lsum ℕ) fun i ↦ (S i).subtype) ∘ₗ filterLinearMap R (fun i ↦ ↥(S i)) p).range ≤ ⨆ i, ⨆ (_ : p i), S i
Module: Mathlib.LinearAlgebra.LinearIndependent.Lemmas

Goal state before:
pp: ι : Type u'
R : Type u_2
M : Type u_4
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
v : ι → M
indep : Set ι → Prop := fun s ↦ LinearIndepOn R v s
X : Type (max 0 u') := { I // indep I }
r : X → X → Prop := fun I J ↦ ↑I ⊆ ↑J
c : Set X
hc : IsChain r c
f : ι →₀ R
hfsupp : f ∈ Finsupp.supported R R (⋃ I ∈ c, ↑I)
g : ι →₀ R
⊢ g ∈ Finsupp.supported R R (⋃ I ∈ c, ↑I) →
    (Finsupp.linearCombination R v) f = (Finsupp.linearCombination R v) g → f = g

Tactic:
hgsupp

Goal state after:
ι : Type u'
R : Type u_2
M : Type u_4
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
v : ι → M
indep : Set ι → Prop := fun s ↦ LinearIndepOn R v s
X : Type (max 0 u') := { I // indep I }
r : X → X → Prop := fun I J ↦ ↑I ⊆ ↑J
c : Set X
hc : IsChain r c
f : ι →₀ R
hfsupp : f ∈ Finsupp.supported R R (⋃ I ∈ c, ↑I)
g : ι →₀ R
hgsupp : g ∈ Finsupp.supported R R (⋃ I ∈ c, ↑I)
⊢ (Finsupp.linearCombination R v) f = (Finsupp.linearCombination R v) g → f = g
Module: Mathlib.LinearAlgebra.DFinsupp

Goal state before:
pp: case mpr
ι : Type u_1
R : Type u_3
N : Type u_6
inst✝² : Semiring R
inst✝¹ : AddCommMonoid N
inst✝ : Module R N
s : Finset ι
p : ι → Submodule R N
a : N
μ : (i : ι) → ↥(p i)
hμ : ∑ i ∈ s, ↑(μ i) = a
⊢ ∃ f, (f.sum fun x xi ↦ ↑xi) = a

Tactic:
refine ⟨DFinsupp.mk s ?_, ?_⟩
      · rintro ⟨i, hi⟩
        refine ⟨μ i, ?_⟩
        rw [iSup_pos]
        · exact coe_mem _
        · exact hi
      simp only [DFinsupp.sum]
      rw [Finset.sum_subset support_mk_subset, ← hμ]
      · exact Finset.sum_congr rfl fun x hx => by rw [mk_of_mem hx]
      · intro x _ hx
        rw [mem_support_iff, not_ne_iff] at hx
        rw [hx]
        rfl

Goal state after:
Module: Mathlib.Algebra.Group.Pointwise.Set.ListOfFn

Goal state before:
pp: case succ
α : Type u_1
inst✝ : Monoid α
n✝ n : ℕ
ih : ∀ {a : α} {s : Fin n → Set α}, a ∈ (List.ofFn s).prod ↔ ∃ f, (List.ofFn fun i ↦ ↑(f i)).prod = a
a : α
s : Fin (n + 1) → Set α
⊢ (∃ x, x ∈ s 0 ∧ ∃ a_1, x * (List.ofFn fun i ↦ ↑(a_1 i)).prod = a) ↔ ∃ x h v, x * (List.ofFn fun i ↦ ↑(v i)).prod = a

Tactic:
exists_prop

Goal state after:
Module: Mathlib.LinearAlgebra.LinearIndependent.Lemmas

Goal state before:
pp: K : Type u_3
V : Type u
inst✝² : DivisionRing K
inst✝¹ : AddCommGroup V
inst✝ : Module K V
f : Fin 2 → V
⊢ (Fin.tail f default ≠ 0 ∧ ¬∃ a, a • Fin.tail f default = f 0) ↔ f 1 ≠ 0 ∧ ∀ (a : K), a • f 1 ≠ f 0

Tactic:
not_exists,

Goal state after:
K : Type u_3
V : Type u
inst✝² : DivisionRing K
inst✝¹ : AddCommGroup V
inst✝ : Module K V
f : Fin 2 → V
⊢ (Fin.tail f default ≠ 0 ∧ ∀ (x : K), ¬x • Fin.tail f default = f 0) ↔ f 1 ≠ 0 ∧ ∀ (a : K), a • f 1 ≠ f 0
Module: Mathlib.Algebra.MonoidAlgebra.MapDomain

Goal state before:
pp: R : Type u_3
S : Type u_4
M : Type u_6
inst✝¹ : Semiring R
inst✝ : Semiring S
f : R →+ S
he : Injective ⇑f
⊢ Injective (map f)

Tactic:
have : map (M := M) f = coeffEquiv.symm ∘ Finsupp.mapRange f (map_zero f) ∘ coeffEquiv := by
    ext; simp [ofCoeff_mapRange]

Goal state after:
R : Type u_3
S : Type u_4
M : Type u_6
inst✝¹ : Semiring R
inst✝ : Semiring S
f : R →+ S
he : Injective ⇑f
this : map f = ⇑coeffEquiv.symm ∘ mapRange ⇑f ⋯ ∘ ⇑coeffEquiv
⊢ Injective (map f)
Module: Mathlib.Algebra.MonoidAlgebra.MapDomain

Goal state before:
pp: R : Type u_3
S : Type u_4
M : Type u_6
inst✝¹ : Semiring R
inst✝ : Semiring S
f : R →+ S
he : Surjective ⇑f
⊢ Surjective (map f)

Tactic:
have : map (M := M) f = coeffEquiv.symm ∘ Finsupp.mapRange f (map_zero f) ∘ coeffEquiv := by
    ext; simp [ofCoeff_mapRange]

Goal state after:
R : Type u_3
S : Type u_4
M : Type u_6
inst✝¹ : Semiring R
inst✝ : Semiring S
f : R →+ S
he : Surjective ⇑f
this : map f = ⇑coeffEquiv.symm ∘ mapRange ⇑f ⋯ ∘ ⇑coeffEquiv
⊢ Surjective (map f)
Module: Mathlib.Data.Finset.Sort

Goal state before:
pp: α : Type u_1
inst✝ : LinearOrder α
s : Finset α
h : 0 < (s.sort fun a b ↦ a ≤ b).length
H : s.Nonempty
l : List α := s.sort fun a b ↦ a ≤ b
⊢ (s.sort fun a b ↦ a ≤ b).get ⟨0, h⟩ = s.min' H

Tactic:
apply le_antisymm

Goal state after:
case a
α : Type u_1
inst✝ : LinearOrder α
s : Finset α
h : 0 < (s.sort fun a b ↦ a ≤ b).length
H : s.Nonempty
l : List α := ⋯
⊢ (s.sort fun a b ↦ a ≤ b).get ⟨0, h⟩ ≤ s.min' H

case a
α : Type u_1
inst✝ : LinearOrder α
s : Finset α
h : 0 < (s.sort fun a b ↦ a ≤ b).length
H : s.Nonempty
l : List α := ⋯
⊢ s.min' H ≤ (s.sort fun a b ↦ a ≤ b).get ⟨0, h⟩
Module: Mathlib.Data.Finset.Sort

Goal state before:
pp: α : Type u_1
inst✝ : LinearOrder α
s : Finset α
h : (s.sort fun a b ↦ a ≤ b).length - 1 < (s.sort fun a b ↦ a ≤ b).length
H : s.Nonempty
l : List α := s.sort fun a b ↦ a ≤ b
⊢ (s.sort fun a b ↦ a ≤ b)[(s.sort fun a b ↦ a ≤ b).length - 1] = s.max' H

Tactic:
apply le_antisymm

Goal state after:
case a
α : Type u_1
inst✝ : LinearOrder α
s : Finset α
h : (s.sort fun a b ↦ a ≤ b).length - 1 < (s.sort fun a b ↦ a ≤ b).length
H : s.Nonempty
l : List α := ⋯
⊢ (s.sort fun a b ↦ a ≤ b)[(s.sort fun a b ↦ a ≤ b).length - 1] ≤ s.max' H

case a
α : Type u_1
inst✝ : LinearOrder α
s : Finset α
h : (s.sort fun a b ↦ a ≤ b).length - 1 < (s.sort fun a b ↦ a ≤ b).length
H : s.Nonempty
l : List α := ⋯
⊢ s.max' H ≤ (s.sort fun a b ↦ a ≤ b)[(s.sort fun a b ↦ a ≤ b).length - 1]
Module: Mathlib.Order.Sublattice

Goal state before:
pp: κ : Type u_5
π : κ → Type u_6
inst✝ : (i : κ) → Lattice (π i)
s : Set κ
hs : s.Nonempty
a : (i : κ) → π i
⊢ (a ∈ pi s fun x ↦ ⊥) ↔ a ∈ ⊥

Tactic:
simpa [mem_pi] using! hs

Goal state after:
Module: Mathlib.LinearAlgebra.Finsupp.VectorSpace

Goal state before:
pp: R : Type u_1
M : Type u_2
ι : Type u_3
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
φ : ι → Type u_4
f : (i : ι) → φ i → M
hf : ∀ (i : ι), LinearIndependent R (f i)
⊢ LinearIndependent R fun ix ↦ single ix.fst (f ix.fst ix.snd)

Tactic:
convert!
    (DFinsupp.linearIndependent_single _ hf).map_injOn _
      (finsuppLequivDFinsupp R).symm.injective.injOn
  simp

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

Goal state before:
pp: R : Type u_1
M : Type u_2
P : Type u_4
inst✝⁴ : Ring R
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : AddCommGroup P
inst✝ : Module R P
f : M →ₗ[R] P
s : Submodule R M
this✝¹ : DecidableEq R
this✝ : DecidableEq M
this : DecidableEq P
t1 : Finset P
ht1 : span R ↑t1 = map f s
t2 : Finset M
ht2 : span R ↑t2 = s ⊓ f.ker
g : P → M
hg : ∀ y ∈ t1, g y ∈ s ∧ f (g y) = y
⊢ span R (g '' ↑t1) ⊔ span R ↑t2 = s

Tactic:
apply le_antisymm

Goal state after:
case a
R : Type u_1
M : Type u_2
P : Type u_4
inst✝⁴ : Ring R
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : AddCommGroup P
inst✝ : Module R P
f : M →ₗ[R] P
s : Submodule R M
this✝¹ : DecidableEq R
this✝ : DecidableEq M
this : DecidableEq P
t1 : Finset P
ht1 : span R ↑t1 = map f s
t2 : Finset M
ht2 : span R ↑t2 = s ⊓ f.ker
g : P → M
hg : ∀ y ∈ t1, g y ∈ s ∧ f (g y) = y
⊢ span R (g '' ↑t1) ⊔ span R ↑t2 ≤ s

case a
R : Type u_1
M : Type u_2
P : Type u_4
inst✝⁴ : Ring R
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : AddCommGroup P
inst✝ : Module R P
f : M →ₗ[R] P
s : Submodule R M
this✝¹ : DecidableEq R
this✝ : DecidableEq M
this : DecidableEq P
t1 : Finset P
ht1 : span R ↑t1 = map f s
t2 : Finset M
ht2 : span R ↑t2 = s ⊓ f.ker
g : P → M
hg : ∀ y ∈ t1, g y ∈ s ∧ f (g y) = y
⊢ s ≤ span R (g '' ↑t1) ⊔ span R ↑t2
Module: Mathlib.LinearAlgebra.Projection

Goal state before:
pp: R : Type u_1
inst✝⁴ : Ring R
E : Type u_2
inst✝³ : AddCommGroup E
inst✝² : Module R E
F : Type u_3
inst✝¹ : AddCommGroup F
inst✝ : Module R F
p q : Submodule R E
hpq : IsCompl p q
φ : ↥p →ₗ[R] F
ψ : ↥q →ₗ[R] F
⊢ (φ ∘ₗ p.projectionOnto q hpq + ψ ∘ₗ q.projectionOnto p ⋯).range = φ.range ⊔ ψ.range

Tactic:
apply le_antisymm

Goal state after:
case a
R : Type u_1
inst✝⁴ : Ring R
E : Type u_2
inst✝³ : AddCommGroup E
inst✝² : Module R E
F : Type u_3
inst✝¹ : AddCommGroup F
inst✝ : Module R F
p q : Submodule R E
hpq : IsCompl p q
φ : ↥p →ₗ[R] F
ψ : ↥q →ₗ[R] F
⊢ (φ ∘ₗ p.projectionOnto q hpq + ψ ∘ₗ q.projectionOnto p ⋯).range ≤ φ.range ⊔ ψ.range

case a
R : Type u_1
inst✝⁴ : Ring R
E : Type u_2
inst✝³ : AddCommGroup E
inst✝² : Module R E
F : Type u_3
inst✝¹ : AddCommGroup F
inst✝ : Module R F
p q : Submodule R E
hpq : IsCompl p q
φ : ↥p →ₗ[R] F
ψ : ↥q →ₗ[R] F
⊢ φ.range ⊔ ψ.range ≤ (φ ∘ₗ p.projectionOnto q hpq + ψ ∘ₗ q.projectionOnto p ⋯).range
Module: Mathlib.Data.ENat.Lattice

Goal state before:
pp: ι : Sort u_1
f : ι → ℕ
⊢ ⨅ i, ↑(f i) ≠ ⊤ ↔ Nonempty ι

Tactic:
by
  rw [Ne, iInf_natCast_eq_top, not_isEmpty_iff]

Goal state after:
Module: Mathlib.Data.ENat.Lattice

Goal state before:
pp: case coe
s : Set ℕ∞
x : ℕ
hx : ↑x < ⊤
y : ℕ∞
h : y ≤ ↑x
hy : y ∈ s
hxt : y < ⊤
⊢ y ∈ (fun n ↦ ↑n) '' {n | n ≤ x}

Tactic:
use y.toNat

Goal state after:
case h
s : Set ℕ∞
x : ℕ
hx : ↑x < ⊤
y : ℕ∞
h : y ≤ ↑x
hy : y ∈ s
hxt : y < ⊤
⊢ y.toNat ∈ {n | n ≤ x} ∧ (fun n ↦ ↑n) y.toNat = y
Module: Mathlib.Data.ENat.Lattice

Goal state before:
pp: ι : Sort u_2
f : ι → ℕ∞
a : ℕ∞
inst✝ : Nonempty ι
b : ι
hb : f b = ⨅ x, f x
⊢ ⨅ i, a * f i ≤ a * ⨅ i, f i

Tactic:
rw [← hb, iInf_le_iff]

Goal state after:
ι : Sort u_2
f : ι → ℕ∞
a : ℕ∞
inst✝ : Nonempty ι
b : ι
hb : f b = ⨅ x, f x
⊢ ∀ (b_1 : ℕ∞), (∀ (i : ι), b_1 ≤ a * f i) → b_1 ≤ a * f b
Module: Mathlib.Data.ENat.Lattice

Goal state before:
pp: case inr
ι : Sort u_2
f : ι → ℕ∞
a : ℕ∞
inst✝ : Nonempty ι
ha : a ≠ ⊤
h : ¬∃ i, a < f i
⊢ a - ⨆ i, f i = ⨅ i, a - f i

Tactic:
not_exists,

Goal state after:
case inr
ι : Sort u_2
f : ι → ℕ∞
a : ℕ∞
inst✝ : Nonempty ι
ha : a ≠ ⊤
h : ∀ (x : ι), ¬a < f x
⊢ a - ⨆ i, f i = ⨅ i, a - f i
Module: Mathlib.Order.RelSeries

Goal state before:
pp: α : Type u_1
r : SetRel α α
s : RelSeries r
hs : s.length = 0
i j : Fin (s.length + 1)
⊢ s.toFun i = s.toFun j

Tactic:
congr!

Goal state after:
α : Type u_1
r : SetRel α α
s : RelSeries r
hs : s.length = 0
i j : Fin (s.length + 1)
⊢ i = j
Module: Mathlib.Algebra.Module.Submodule.Bilinear

Goal state before:
pp: R : Type u_1
M : Type u_2
N : Type u_3
P : Type u_4
inst✝⁶ : CommSemiring R
inst✝⁵ : AddCommMonoid M
inst✝⁴ : AddCommMonoid N
inst✝³ : AddCommMonoid P
inst✝² : Module R M
inst✝¹ : Module R N
inst✝ : Module R P
f : M →ₗ[R] N →ₗ[R] P
s : Set M
t : Set N
⊢ map₂ f (span R s) (span R t) = span R (image2 (fun m n ↦ (f m) n) s t)

Tactic:
apply le_antisymm

Goal state after:
case a
R : Type u_1
M : Type u_2
N : Type u_3
P : Type u_4
inst✝⁶ : CommSemiring R
inst✝⁵ : AddCommMonoid M
inst✝⁴ : AddCommMonoid N
inst✝³ : AddCommMonoid P
inst✝² : Module R M
inst✝¹ : Module R N
inst✝ : Module R P
f : M →ₗ[R] N →ₗ[R] P
s : Set M
t : Set N
⊢ map₂ f (span R s) (span R t) ≤ span R (image2 (fun m n ↦ (f m) n) s t)

case a
R : Type u_1
M : Type u_2
N : Type u_3
P : Type u_4
inst✝⁶ : CommSemiring R
inst✝⁵ : AddCommMonoid M
inst✝⁴ : AddCommMonoid N
inst✝³ : AddCommMonoid P
inst✝² : Module R M
inst✝¹ : Module R N
inst✝ : Module R P
f : M →ₗ[R] N →ₗ[R] P
s : Set M
t : Set N
⊢ span R (image2 (fun m n ↦ (f m) n) s t) ≤ map₂ f (span R s) (span R t)
Module: Mathlib.Order.KrullDimension

Goal state before:
pp: α : Type u_1
inst✝ : Preorder α
a : α
⊢ height a = ⨆ p, ⨆ (_ : RelSeries.last p = a), ↑p.length

Tactic:
by
  apply eq_of_forall_ge_iff
  intro n
  rw [height_le_iff', iSup₂_le_iff]

Goal state after:
Module: Mathlib.Algebra.Exact.Basic

Goal state before:
pp: R : Type u_1
inst✝¹² : Ring R
M₁ : Type u_8
M₂ : Type u_9
M₃ : Type u_10
N₁ : Type u_11
N₂ : Type u_12
N₃ : Type u_13
inst✝¹¹ : AddCommMonoid M₁
inst✝¹⁰ : AddCommMonoid M₂
inst✝⁹ : AddCommMonoid M₃
inst✝⁸ : AddCommMonoid N₁
inst✝⁷ : AddCommMonoid N₂
inst✝⁶ : AddCommMonoid N₃
inst✝⁵ : Module R M₁
inst✝⁴ : Module R M₂
inst✝³ : Module R M₃
inst✝² : Module R N₁
inst✝¹ : Module R N₂
inst✝ : Module R N₃
f : M₁ →ₗ[R] M₂
g : M₂ →ₗ[R] M₃
f' : N₁ →ₗ[R] N₂
g' : N₂ →ₗ[R] N₃
τ₁ : M₁ →ₗ[R] N₁
τ₂ : M₂ →ₗ[R] N₂
τ₃ : M₃ →ₗ[R] N₃
comm₁₂ : f' ∘ₗ τ₁ = τ₂ ∘ₗ f
comm₂₃ : g' ∘ₗ τ₂ = τ₃ ∘ₗ g
h₁ : Function.Surjective ⇑τ₁
h₂ : Function.Bijective ⇑τ₂
h₃ : Function.Injective ⇑τ₃
⊢ g'.toAddMonoidHom.comp τ₂.toAddMonoidHom = τ₃.toAddMonoidHom.comp g.toAddMonoidHom

Tactic:
by ext; apply DFunLike.congr_fun comm₂₃

Goal state after:
Module: Mathlib.Order.KrullDimension

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝¹ : Preorder α
inst✝ : Preorder β
f : α ≃o β
x : α
⊢ height (f x) = height x

Tactic:
apply le_antisymm

Goal state after:
case a
α : Type u_1
β : Type u_2
inst✝¹ : Preorder α
inst✝ : Preorder β
f : α ≃o β
x : α
⊢ height (f x) ≤ height x

case a
α : Type u_1
β : Type u_2
inst✝¹ : Preorder α
inst✝ : Preorder β
f : α ≃o β
x : α
⊢ height x ≤ height (f x)
Module: Mathlib.Order.KrullDimension

Goal state before:
pp: α : Type u_1
inst✝ : Preorder α
x : α
⊢ height x = ⨆ y, ⨆ (_ : y < x), height y + 1

Tactic:
apply le_antisymm

Goal state after:
case a
α : Type u_1
inst✝ : Preorder α
x : α
⊢ height x ≤ ⨆ y, ⨆ (_ : y < x), height y + 1

case a
α : Type u_1
inst✝ : Preorder α
x : α
⊢ ⨆ y, ⨆ (_ : y < x), height y + 1 ≤ height x
Module: Mathlib.Order.KrullDimension

Goal state before:
pp: α : Type u_1
inst✝¹ : Preorder α
inst✝ : InfiniteDimensionalOrder α
m : WithBot ℕ∞
hm✝ : ∀ (i : LTSeries α), ↑i.length ≤ m
hm : ∀ (i : LTSeries α), ↑i.length ≤ ⊥
this : Inhabited α
⊢ False

Tactic:
exact not_le_of_gt (WithBot.bot_lt_coe _ : ⊥ < (0 : WithBot (WithTop ℕ))) <| hm default

Goal state after:
Module: Mathlib.Order.KrullDimension

Goal state before:
pp: α : Type u_1
inst✝¹ : Preorder α
inst✝ : Nonempty α
⊢ krullDim α = ↑(⨆ a, height a)

Tactic:
apply le_antisymm

Goal state after:
case a
α : Type u_1
inst✝¹ : Preorder α
inst✝ : Nonempty α
⊢ krullDim α ≤ ↑(⨆ a, height a)

case a
α : Type u_1
inst✝¹ : Preorder α
inst✝ : Nonempty α
⊢ ↑(⨆ a, height a) ≤ krullDim α
Module: Mathlib.Order.KrullDimension

Goal state before:
pp: α : Type u_1
inst✝¹ : Preorder α
inst✝ : Nonempty α
⊢ krullDim α = ↑(⨆ a, height a + coheight a)

Tactic:
apply le_antisymm

Goal state after:
case a
α : Type u_1
inst✝¹ : Preorder α
inst✝ : Nonempty α
⊢ krullDim α ≤ ↑(⨆ a, height a + coheight a)

case a
α : Type u_1
inst✝¹ : Preorder α
inst✝ : Nonempty α
⊢ ↑(⨆ a, height a + coheight a) ≤ krullDim α
Module: Mathlib.Order.KrullDimension

Goal state before:
pp: α : Type u_1
inst✝¹ : Preorder α
inst✝ : OrderTop α
⊢ height ⊤ = ⨆ p, ↑p.length

Tactic:
apply le_antisymm

Goal state after:
case a
α : Type u_1
inst✝¹ : Preorder α
inst✝ : OrderTop α
⊢ height ⊤ ≤ ⨆ p, ↑p.length

case a
α : Type u_1
inst✝¹ : Preorder α
inst✝ : OrderTop α
⊢ ⨆ p, ↑p.length ≤ height ⊤
Module: Mathlib.Order.KrullDimension

Goal state before:
pp: α : Type u_1
inst✝ : Preorder α
x : α
⊢ ⨆ p, ⨆ (_ : RelSeries.last p ≤ x), ↑p.length = ⨆ p, ⨆ (_ : RelSeries.last p ≤ ⊤), ↑p.length

Tactic:
apply le_antisymm

Goal state after:
case a
α : Type u_1
inst✝ : Preorder α
x : α
⊢ ⨆ p, ⨆ (_ : RelSeries.last p ≤ x), ↑p.length ≤ ⨆ p, ⨆ (_ : RelSeries.last p ≤ ⊤), ↑p.length

case a
α : Type u_1
inst✝ : Preorder α
x : α
⊢ ⨆ p, ⨆ (_ : RelSeries.last p ≤ ⊤), ↑p.length ≤ ⨆ p, ⨆ (_ : RelSeries.last p ≤ x), ↑p.length
Module: Mathlib.Order.KrullDimension

Goal state before:
pp: case ind
n : ℕ
ih : ∀ m < n, height m = ↑m
⊢ height n = ↑n

Tactic:
apply le_antisymm

Goal state after:
case ind.a
n : ℕ
ih : ∀ m < n, height m = ↑m
⊢ height n ≤ ↑n

case a
n : ℕ
ih : ∀ m < n, height m = ↑m
⊢ ↑n ≤ height n
Module: Mathlib.Order.KrullDimension

Goal state before:
pp: α : Type u_1
inst✝ : Preorder α
x : α
⊢ height ↑x = height x + 1

Tactic:
apply le_antisymm

Goal state after:
case a
α : Type u_1
inst✝ : Preorder α
x : α
⊢ height ↑x ≤ height x + 1

case a
α : Type u_1
inst✝ : Preorder α
x : α
⊢ height x + 1 ≤ height ↑x
Module: Mathlib.Order.KrullDimension

Goal state before:
pp: α : Type u_1
inst✝ : Preorder α
x : α
⊢ height ↑x = height x

Tactic:
apply le_antisymm

Goal state after:
case a
α : Type u_1
inst✝ : Preorder α
x : α
⊢ height ↑x ≤ height x

case a
α : Type u_1
inst✝ : Preorder α
x : α
⊢ height x ≤ height ↑x
Module: Mathlib.Order.KrullDimension

Goal state before:
pp: case top
⊢ height ⊤ = ⊤

Tactic:
simp only [← WithBot.coe_eq_coe, height_top_eq_krullDim, krullDim_enat, WithBot.coe_top]

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

Goal state before:
pp: R : Type u_1
inst✝⁴ : CommSemiring R
M : Type u_2
N : Type u_3
inst✝³ : AddCommGroup M
inst✝² : AddCommMonoid N
inst✝¹ : Module R M
inst✝ : Module R N
x✝ x y : M ⊗[R] N
hx : -x + x = 0
hy : -y + y = 0
⊢ -(x + y) + (x + y) = 0

Tactic:
by
    suffices -x + x + (-y + y) = 0 by
      rw [← this]
      unfold Neg.neg neg
      simp only
      rw [map_add]
      abel
    rw [hx, hy, add_zero]

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

Goal state before:
pp: R : Type u_1
R₂ : Type u_2
R₃ : Type u_3
R' : Type u_4
R'' : Type u_5
inst✝⁴¹ : CommSemiring R
inst✝⁴⁰ : CommSemiring R₂
inst✝³⁹ : CommSemiring R₃
inst✝³⁸ : Monoid R'
inst✝³⁷ : Semiring R''
σ₁₂ : R →+* R₂
σ₂₃ : R₂ →+* R₃
σ₁₃ : R →+* R₃
A : Type u_6
M : Type u_7
N : Type u_8
P : Type u_9
Q : Type u_10
S : Type u_11
M₂ : Type u_12
M₃ : Type u_13
N₂ : Type u_14
N₃ : Type u_15
P' : Type u_16
P₂ : Type u_17
P₃ : Type u_18
Q' : Type u_19
Q₂ : Type u_20
Q₃ : Type u_21
inst✝³⁶ : AddCommMonoid M
inst✝³⁵ : AddCommMonoid N
inst✝³⁴ : AddCommMonoid P
inst✝³³ : AddCommMonoid Q
inst✝³² : AddCommMonoid S
inst✝³¹ : AddCommMonoid P'
inst✝³⁰ : AddCommMonoid Q'
inst✝²⁹ : AddCommMonoid M₂
inst✝²⁸ : AddCommMonoid N₂
inst✝²⁷ : AddCommMonoid P₂
inst✝²⁶ : AddCommMonoid Q₂
inst✝²⁵ : AddCommMonoid M₃
inst✝²⁴ : AddCommMonoid N₃
inst✝²³ : AddCommMonoid P₃
inst✝²² : AddCommMonoid Q₃
inst✝²¹ : DistribMulAction R' M
inst✝²⁰ : Module R'' M
inst✝¹⁹ : Module R M
inst✝¹⁸ : Module R N
inst✝¹⁷ : Module R S
inst✝¹⁶ : Module R P'
inst✝¹⁵ : Module R Q'
inst✝¹⁴ : Module R₂ M₂
inst✝¹³ : Module R₂ N₂
inst✝¹² : Module R₂ P₂
inst✝¹¹ : Module R₂ Q₂
inst✝¹⁰ : Module R₃ M₃
inst✝⁹ : Module R₃ N₃
inst✝⁸ : Module R₃ P₃
inst✝⁷ : Module R₃ Q₃
inst✝⁶ : SMulCommClass R R' M
inst✝⁵ : SMulCommClass R R'' M
R'₂ : Type u_22
inst✝⁴ : Monoid R'₂
inst✝³ : DistribMulAction R'₂ M
inst✝² : SMulCommClass R R'₂ M
inst✝¹ : SMul R'₂ R'
inst✝ : IsScalarTower R'₂ R' M
s : R'₂
r : R'
x✝ x y : M ⊗[R] N
ihx : (s • r) • x = s • r • x
ihy : (s • r) • y = s • r • y
⊢ (s • r) • (x + y) = s • r • (x + y)

Tactic:
rw [smul_add, smul_add, smul_add, ihx, ihy]

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

Goal state before:
pp: R : Type u_1
R₂ : Type u_2
R₃ : Type u_3
R' : Type u_4
R'' : Type u_5
inst✝⁴⁵ : CommSemiring R
inst✝⁴⁴ : CommSemiring R₂
inst✝⁴³ : CommSemiring R₃
inst✝⁴² : Monoid R'
inst✝⁴¹ : Semiring R''
σ₁₂ : R →+* R₂
σ₂₃ : R₂ →+* R₃
σ₁₃ : R →+* R₃
A : Type u_6
M : Type u_7
N : Type u_8
P : Type u_9
Q : Type u_10
S : Type u_11
M₂ : Type u_12
M₃ : Type u_13
N₂ : Type u_14
N₃ : Type u_15
P' : Type u_16
P₂ : Type u_17
P₃ : Type u_18
Q' : Type u_19
Q₂ : Type u_20
Q₃ : Type u_21
inst✝⁴⁰ : AddCommMonoid M
inst✝³⁹ : AddCommMonoid N
inst✝³⁸ : AddCommMonoid P
inst✝³⁷ : AddCommMonoid Q
inst✝³⁶ : AddCommMonoid S
inst✝³⁵ : AddCommMonoid P'
inst✝³⁴ : AddCommMonoid Q'
inst✝³³ : AddCommMonoid M₂
inst✝³² : AddCommMonoid N₂
inst✝³¹ : AddCommMonoid P₂
inst✝³⁰ : AddCommMonoid Q₂
inst✝²⁹ : AddCommMonoid M₃
inst✝²⁸ : AddCommMonoid N₃
inst✝²⁷ : AddCommMonoid P₃
inst✝²⁶ : AddCommMonoid Q₃
inst✝²⁵ : DistribMulAction R' M
inst✝²⁴ : Module R'' M
inst✝²³ : Module R M
inst✝²² : Module R N
inst✝²¹ : Module R S
inst✝²⁰ : Module R P'
inst✝¹⁹ : Module R Q'
inst✝¹⁸ : Module R₂ M₂
inst✝¹⁷ : Module R₂ N₂
inst✝¹⁶ : Module R₂ P₂
inst✝¹⁵ : Module R₂ Q₂
inst✝¹⁴ : Module R₃ M₃
inst✝¹³ : Module R₃ N₃
inst✝¹² : Module R₃ P₃
inst✝¹¹ : Module R₃ Q₃
inst✝¹⁰ : SMulCommClass R R' M
inst✝⁹ : SMulCommClass R R'' M
R'₂ : Type u_22
inst✝⁸ : Monoid R'₂
inst✝⁷ : DistribMulAction R'₂ M
inst✝⁶ : SMulCommClass R R'₂ M
inst✝⁵ : SMul R'₂ R'
inst✝⁴ : DistribMulAction R'₂ N
inst✝³ : DistribMulAction R' N
inst✝² : CompatibleSMul R R'₂ M N
inst✝¹ : CompatibleSMul R R' M N
inst✝ : IsScalarTower R'₂ R' N
s : R'₂
r : R'
x✝ x y : M ⊗[R] N
ihx : (s • r) • x = s • r • x
ihy : (s • r) • y = s • r • y
⊢ (s • r) • (x + y) = s • r • (x + y)

Tactic:
rw [smul_add, smul_add, smul_add, ihx, ihy]

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

Goal state before:
pp: case h
R : Type u_1
inst✝⁴ : CommSemiring R
M : Type u_7
N : Type u_8
inst✝³ : AddCommMonoid M
inst✝² : AddCommMonoid N
inst✝¹ : Module R M
inst✝ : Module R N
h : ∀ (m₁ m₂ : M) (n₁ n₂ : N), ∃ m n, m₁ ⊗ₜ[R] n₁ + m₂ ⊗ₜ[R] n₂ = m ⊗ₜ[R] n
⊢ 0 = 0 ⊗ₜ[R] 0

Tactic:
rw [TensorProduct.zero_tmul]

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

Goal state before:
pp: case zero
R : Type u_1
inst✝⁴ : CommSemiring R
M : Type u_7
N : Type u_8
inst✝³ : AddCommMonoid M
inst✝² : AddCommMonoid N
inst✝¹ : Module R M
inst✝ : Module R N
f : M →ₗ[R] M
g : N →ₗ[R] N
⊢ map f g ^ 0 = map (f ^ 0) (g ^ 0)

Tactic:
simp only [pow_zero, TensorProduct.map_one]

Goal state after: