mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Data.DFinsupp.Sigma

Goal state before:
pp: ι : 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 : (x : ι) × α x), δ i.fst i.snd
i : ι
j : α i
⊢ (f.sigmaCurry i) j = f ⟨i, j⟩

Tactic:
sigmaCurry_apply

Goal state after:
ι : 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 : (x : ι) × α x), δ i.fst i.snd
i : ι
j : α i
⊢ f ⟨i, j⟩ = f ⟨i, j⟩
Module: Mathlib.Data.DFinsupp.BigOperators

Goal state before:
pp: case refine_3
ι : Type u
γ : Type w
β : ι → Type v
β₁ : ι → Type v₁
β₂ : ι → Type v₂
inst✝² : DecidableEq ι
inst✝¹ : (i : ι) → Zero (β i)
inst✝ : AddCommMonoid γ
φ : (i : ι) → ZeroHom (β i) γ
f : Π₀ (i : ι), β i
sx : Multiset ι
hx : ∀ (i : ι), i ∈ sx ∨ f.toFun i = 0
sy : Multiset ι
hy : ∀ (i : ι), i ∈ sy ∨ f.toFun i = 0
H1 : sx.toFinset ∩ sy.toFinset ⊆ sx.toFinset
H2 : sx.toFinset ∩ sy.toFinset ⊆ sy.toFinset
⊢ ∀ x ∈ sy.toFinset, x ∉ sx.toFinset ∩ sy.toFinset → (φ x) (f x) = 0

Tactic:
· intro i H1 H2
        rw [Finset.mem_inter] at H2
        simp only [Multiset.mem_toFinset] at H1 H2
        convert! map_zero (φ i)
        exact (hx i).resolve_left (mt (fun H3 => And.intro H3 H1) H2)

Goal state after:
Module: Mathlib.LinearAlgebra.DFinsupp

Goal state before:
pp: ι : Type u_1
R : Type u_3
N : Type u_6
inst✝³ : DecidableEq ι
inst✝² : Semiring R
inst✝¹ : AddCommMonoid N
inst✝ : Module R N
p : ι → Submodule R N
⊢ iSupIndep p ↔
    ∀ (i : ι) (x : ↥(p i)) (v : Π₀ (i : ι), ↥(p i)), ((lsum ℕ) fun i ↦ (p i).subtype) (erase i v) = ↑x → x = 0

Tactic:
iSupIndep_def,

Goal state after:
ι : Type u_1
R : Type u_3
N : Type u_6
inst✝³ : DecidableEq ι
inst✝² : Semiring R
inst✝¹ : AddCommMonoid N
inst✝ : Module R N
p : ι → Submodule R N
⊢ (∀ (i : ι), Disjoint (p i) (⨆ j, ⨆ (_ : j ≠ i), p j)) ↔
    ∀ (i : ι) (x : ↥(p i)) (v : Π₀ (i : ι), ↥(p i)), ((lsum ℕ) fun i ↦ (p i).subtype) (erase i v) = ↑x → x = 0
Module: Mathlib.LinearAlgebra.DFinsupp

Goal state before:
pp: ι : Type u_1
R : Type u_3
N : Type u_6
inst✝² : Ring R
inst✝¹ : AddCommGroup N
inst✝ : Module R N
p : ι → Submodule R N
⊢ iSupIndep p ↔ ∀ (s : Finset ι) (v : ι → N), (∀ i ∈ s, v i ∈ p i) → ∑ i ∈ s, v i = 0 → ∀ i ∈ s, v i = 0

Tactic:
iSupIndep_def,

Goal state after:
ι : Type u_1
R : Type u_3
N : Type u_6
inst✝² : Ring R
inst✝¹ : AddCommGroup N
inst✝ : Module R N
p : ι → Submodule R N
⊢ (∀ (i : ι), Disjoint (p i) (⨆ j, ⨆ (_ : j ≠ i), p j)) ↔
    ∀ (s : Finset ι) (v : ι → N), (∀ i ∈ s, v i ∈ p i) → ∑ i ∈ s, v i = 0 → ∀ i ∈ s, v i = 0
Module: Mathlib.LinearAlgebra.LinearIndependent.Lemmas

Goal state before:
pp: R : Type u_2
M : Type u_4
inst✝⁹ : Ring R
inst✝⁸ : AddCommGroup M
inst✝⁷ : Module R M
x y : M
S : Type u_6
inst✝⁶ : CommRing S
inst✝⁵ : IsDomain S
inst✝⁴ : Module S R
inst✝³ : Module S M
inst✝² : SMulCommClass S R M
inst✝¹ : IsScalarTower S R M
inst✝ : IsTorsionFree S R
a b c d : S
h : a * d ≠ b * c
h' : ∀ (s t : R), s • x + t • y = 0 → s = 0 ∧ t = 0
⊢ ∀ (s t : R), s • (a • x + b • y) + t • (c • x + d • y) = 0 → s = 0 ∧ t = 0

Tactic:
intro s t hst

Goal state after:
R : Type u_2
M : Type u_4
inst✝⁹ : Ring R
inst✝⁸ : AddCommGroup M
inst✝⁷ : Module R M
x y : M
S : Type u_6
inst✝⁶ : CommRing S
inst✝⁵ : IsDomain S
inst✝⁴ : Module S R
inst✝³ : Module S M
inst✝² : SMulCommClass S R M
inst✝¹ : IsScalarTower S R M
inst✝ : IsTorsionFree S R
a b c d : S
h : a * d ≠ b * c
h' : ∀ (s t : R), s • x + t • y = 0 → s = 0 ∧ t = 0
s t : R
hst : s • (a • x + b • y) + t • (c • x + d • y) = 0
⊢ s = 0 ∧ t = 0
Module: Mathlib.Tactic.Module

Goal state before:
pp: R : Type u_2
M : Type u_3
inst✝² : AddCommMonoid M
inst✝¹ : Semiring R
inst✝ : Module R M
r : R
m n : M
l : NF R M
h1 : 0 = r
h2 : n = l.eval
⊢ n = ((r, m) ::ᵣ l).eval

Tactic:
by
  simp [← h1, h2]

Goal state after:
Module: Mathlib.Algebra.FreeAbelianGroup.Finsupp

Goal state before:
pp: X : Type u_1
a : FreeAbelianGroup X
| a

Tactic:
rw [← toFreeAbelianGroup_toFinsupp a, ← sum_single a.toFinsupp]

Goal state after:
X : Type u_1
a : FreeAbelianGroup X
| toFreeAbelianGroup ((toFinsupp a).sum single)
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 ∧ ∃ y, y ∈ (List.ofFn fun i ↦ s i.succ).prod ∧ x * y = a) ↔
    ∃ a_1 v, ↑a_1 * (List.ofFn fun i ↦ ↑(v i)).prod = a

Tactic:
@ih,

Goal state after:
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 ∧ ∃ y, (∃ f, (List.ofFn fun i ↦ ↑(f i)).prod = y) ∧ x * y = a) ↔
    ∃ a_1 v, ↑a_1 * (List.ofFn fun i ↦ ↑(v i)).prod = a
Module: Mathlib.Algebra.Group.Pointwise.Set.ListOfFn

Goal state before:
pp: case h
α : Type u_1
inst✝ : Monoid α
a : α
n : ℕ
f : Fin n → Set α
⊢ a ∈ (List.ofFn f).prod ↔ ∃ l', (List.map (fun x ↦ ↑x.snd) l').prod = a ∧ List.map Sigma.fst l' = List.ofFn f

Tactic:
simp only [mem_prod_list_ofFn, List.exists_iff_exists_tuple, List.map_ofFn, List.ofFn_inj',
    Sigma.mk.inj_iff, and_left_comm, exists_and_left, exists_eq_left, heq_eq_eq]

Goal state after:
case h
α : Type u_1
inst✝ : Monoid α
a : α
n : ℕ
f : Fin n → Set α
⊢ (∃ f_1, (List.ofFn fun i ↦ ↑(f_1 i)).prod = a) ↔ ∃ x, (List.ofFn ((fun x ↦ ↑x.snd) ∘ x)).prod = a ∧ Sigma.fst ∘ x = f
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
t : Set V
⊢ ∃ b ⊆ t, span K b = span K t ∧ LinearIndependent K Subtype.val

Tactic:
obtain ⟨b, hb₁, -, hb₂, hb₃⟩ :=
    exists_linearIndepOn_id_extension (linearIndependent_empty K V) (Set.empty_subset t)
  exact ⟨b, hb₁, (span_eq_of_le _ hb₂ (Submodule.span_mono hb₁)).symm, hb₃⟩

Goal state after:
Module: Mathlib.Algebra.MonoidAlgebra.MapDomain

Goal state before:
pp: R : Type u_3
M : Type u_6
N : Type u_7
inst✝ : Semiring R
f : M → N
x y : R[M]
⊢ mapDomain f (x + y) = mapDomain f x + mapDomain f y

Tactic:
ext; simp [Finsupp.mapDomain_add]

Goal state after:
Module: Mathlib.Algebra.Group.Pointwise.Finset.Basic

Goal state before:
pp: case h₁
α : Type u_2
inst✝¹ : DecidableEq α
inst✝ : Monoid α
s : Finset α
n : ℕ
⊢ #(s ^ n) ≤ #s ^ n

Tactic:
exact card_pow_le

Goal state after:
Module: Mathlib.Algebra.Group.UniqueProds.Basic

Goal state before:
pp: case refl.inr
G : Type u
inst✝¹ : Mul G
inst✝ : UniqueProds G
a b1 b : G
ha : a ∈ {a}
he : (fun x ↦ a * x) b1 = (fun x ↦ a * x) b
this : b1 ∈ {b1, b}
hu : UniqueMul {a} {b1, b} a b
⊢ b1 = b

Tactic:
exact (hu ha this he).2

Goal state after:
Module: Mathlib.Algebra.Group.Pointwise.Finset.Basic

Goal state before:
pp: case mpr
α : Type u_2
inst✝¹ : DecidableEq α
inst✝ : DivisionMonoid α
a : α
ha : IsUnit a
⊢ IsUnit {a}

Tactic:
exact ha.finset

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

Goal state before:
pp: R : Type u
a b : R
m✝ n✝ : ℕ
inst✝³ : Semiring R
p q : R[X]
S₁ : Type u_1
S₂ : Type u_2
inst✝² : SMulZeroClass S₁ R
inst✝¹ : SMulZeroClass S₂ R
inst✝ : SMulCommClass S₁ S₂ R
m : S₁
n : S₂
f : R[ℕ]
⊢ m • n • { toFinsupp := f } = n • m • { toFinsupp := f }

Tactic:
← ofFinsupp_smul,

Goal state after:
R : Type u
a b : R
m✝ n✝ : ℕ
inst✝³ : Semiring R
p q : R[X]
S₁ : Type u_1
S₂ : Type u_2
inst✝² : SMulZeroClass S₁ R
inst✝¹ : SMulZeroClass S₂ R
inst✝ : SMulCommClass S₁ S₂ R
m : S₁
n : S₂
f : R[ℕ]
⊢ { toFinsupp := m • n • f } = { toFinsupp := n • m • f }
Module: Mathlib.Algebra.Polynomial.Basic

Goal state before:
pp: R : Type u
a b : R
m n : ℕ
inst✝⁴ : Semiring R
p q : R[X]
S₁ : Type u_1
S₂ : Type u_2
inst✝³ : SMul S₁ S₂
inst✝² : SMulZeroClass S₁ R
inst✝¹ : SMulZeroClass S₂ R
inst✝ : IsScalarTower S₁ S₂ R
x✝ : S₁
y✝ : S₂
toFinsupp✝ : R[ℕ]
⊢ (x✝ • y✝) • { toFinsupp := toFinsupp✝ } = x✝ • y✝ • { toFinsupp := toFinsupp✝ }

Tactic:
← ofFinsupp_smul,

Goal state after:
R : Type u
a b : R
m n : ℕ
inst✝⁴ : Semiring R
p q : R[X]
S₁ : Type u_1
S₂ : Type u_2
inst✝³ : SMul S₁ S₂
inst✝² : SMulZeroClass S₁ R
inst✝¹ : SMulZeroClass S₂ R
inst✝ : IsScalarTower S₁ S₂ R
x✝ : S₁
y✝ : S₂
toFinsupp✝ : R[ℕ]
⊢ { toFinsupp := (x✝ • y✝) • toFinsupp✝ } = { toFinsupp := x✝ • y✝ • toFinsupp✝ }
Module: Mathlib.Algebra.Polynomial.Basic

Goal state before:
pp: R : Type u
a b : R
m n : ℕ
inst✝³ : Semiring R
p q : R[X]
α : Type u_1
K : Type u_2
inst✝² : Semiring K
inst✝¹ : DistribSMul α K
inst✝ : IsScalarTower α K K
x✝ : α
toFinsupp✝¹ toFinsupp✝ : K[ℕ]
⊢ x✝ • { toFinsupp := toFinsupp✝¹ } * { toFinsupp := toFinsupp✝ } =
    x✝ • ({ toFinsupp := toFinsupp✝¹ } * { toFinsupp := toFinsupp✝ })

Tactic:
← ofFinsupp_smul,

Goal state after:
R : Type u
a b : R
m n : ℕ
inst✝³ : Semiring R
p q : R[X]
α : Type u_1
K : Type u_2
inst✝² : Semiring K
inst✝¹ : DistribSMul α K
inst✝ : IsScalarTower α K K
x✝ : α
toFinsupp✝¹ toFinsupp✝ : K[ℕ]
⊢ { toFinsupp := x✝ • toFinsupp✝¹ } * { toFinsupp := toFinsupp✝ } =
    x✝ • ({ toFinsupp := toFinsupp✝¹ } * { toFinsupp := toFinsupp✝ })
Module: Mathlib.Algebra.Polynomial.Basic

Goal state before:
pp: R : Type u
a b : R
m n : ℕ
inst✝³ : Semiring R
p q : R[X]
α : Type u_1
K : Type u_2
inst✝² : Semiring K
inst✝¹ : DistribSMul α K
inst✝ : IsScalarTower α K K
x✝ : α
toFinsupp✝¹ toFinsupp✝ : K[ℕ]
⊢ { toFinsupp := x✝ • toFinsupp✝¹ * toFinsupp✝ } = x✝ • { toFinsupp := toFinsupp✝¹ * toFinsupp✝ }

Tactic:
← ofFinsupp_smul,

Goal state after:
R : Type u
a b : R
m n : ℕ
inst✝³ : Semiring R
p q : R[X]
α : Type u_1
K : Type u_2
inst✝² : Semiring K
inst✝¹ : DistribSMul α K
inst✝ : IsScalarTower α K K
x✝ : α
toFinsupp✝¹ toFinsupp✝ : K[ℕ]
⊢ { toFinsupp := x✝ • toFinsupp✝¹ * toFinsupp✝ } = { toFinsupp := x✝ • (toFinsupp✝¹ * toFinsupp✝) }
Module: Mathlib.Algebra.Polynomial.Basic

Goal state before:
pp: R : Type u
a b : R
m n : ℕ
inst✝³ : Semiring R
p q : R[X]
S : Type u_1
inst✝² : SMulZeroClass S R
inst✝¹ : SMulZeroClass Sᵐᵒᵖ R
inst✝ : IsCentralScalar S R
m✝ : S
toFinsupp✝ : R[ℕ]
⊢ MulOpposite.op m✝ • { toFinsupp := toFinsupp✝ } = m✝ • { toFinsupp := toFinsupp✝ }

Tactic:
← ofFinsupp_smul,

Goal state after:
R : Type u
a b : R
m n : ℕ
inst✝³ : Semiring R
p q : R[X]
S : Type u_1
inst✝² : SMulZeroClass S R
inst✝¹ : SMulZeroClass Sᵐᵒᵖ R
inst✝ : IsCentralScalar S R
m✝ : S
toFinsupp✝ : R[ℕ]
⊢ { toFinsupp := MulOpposite.op m✝ • toFinsupp✝ } = { toFinsupp := m✝ • toFinsupp✝ }
Module: Mathlib.Order.Sublattice

Goal state before:
pp: α : Type u_2
β : Type u_3
inst✝¹ : Lattice α
inst✝ : Lattice β
f : LatticeHom α β
h : Surjective ⇑f
⊢ ↑(map f ⊤) = ↑⊤

Tactic:
by simp [h.range_eq]

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

Goal state before:
pp: R : Type u
inst✝ : Semiring R
p : R[X]
n : ℕ
⊢ (p.update n 0).support = p.support.erase n

Tactic:
rw [update_zero_eq_erase, support_erase]

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

Goal state before:
pp: R : Type u_1
M : Type u_2
n : Type u_3
inst✝⁴ : DecidableEq n
inst✝³ : Semiring R
inst✝² : AddCommMonoid M
inst✝¹ : Module R M
inst✝ : Finite n
b : Basis n R M
i : n
⊢ b.equivFun.symm (Pi.single i 1) = b i

Tactic:
cases nonempty_fintype n

Goal state after:
case intro
R : Type u_1
M : Type u_2
n : Type u_3
inst✝⁴ : DecidableEq n
inst✝³ : Semiring R
inst✝² : AddCommMonoid M
inst✝¹ : Module R M
inst✝ : Finite n
b : Basis n R M
i : n
val✝ : Fintype n
⊢ b.equivFun.symm (Pi.single i 1) = b i
Module: Mathlib.RingTheory.Finiteness.Finsupp

Goal state before:
pp: R : Type u_1
M : Type u_2
N : Type u_3
ι : Type u_4
S : Type u_5
inst✝⁸ : Semiring R
inst✝⁷ : AddCommMonoid M
inst✝⁶ : AddCommMonoid N
inst✝⁵ : Module R M
inst✝⁴ : Module R N
inst✝³ : Semiring S
inst✝² : Module S N
inst✝¹ : SMulCommClass R S N
inst✝ : Module.Finite R M
s : Finset M
span_s : Submodule.span R ↑s = ⊤
x : M →ₗ[R] ι →₀ N
i : ι
h : i ∉ s.sup fun m ↦ (x m).support
⊢ Set.EqOn ⇑(lapply i ∘ₗ x) ⇑0 ↑s

Tactic:
by simpa using! h

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

Goal state before:
pp: case a.refine_2.left.h_add
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
x : M
hx : x ∈ s
l : P →₀ R
hl1 : l ∈ supported R R ↑t1
hl2 : (linearCombination R id) l = f x
⊢ ∀ (b : M) (m₁ m₂ : R), (m₁ + m₂) • id b = m₁ • id b + m₂ • id b

Tactic:
exact fun _ _ _ => add_smul _ _ _

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

Goal state before:
pp: case a.refine_2.right.h_add
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
x : M
hx : x ∈ s
l : P →₀ R
hl1 : l ∈ supported R R ↑t1
hl2 : (linearCombination R id) l = f x
⊢ ∀ (b : M) (m₁ m₂ : R), (m₁ + m₂) • id b = m₁ • id b + m₂ • id b

Tactic:
exact fun _ _ _ => add_smul _ _ _

Goal state after:
Module: Mathlib.Algebra.Order.SuccPred.WithBot

Goal state before:
pp: α : Type u_1
inst✝³ : Preorder α
inst✝² : OrderBot α
inst✝¹ : AddMonoidWithOne α
inst✝ : SuccAddOrder α
n : ℕ
⊢ (↑n).succ = ↑n + 1

Tactic:
by
  rw [← WithBot.coe_natCast, succ_coe, Order.succ_eq_add_one]

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

Goal state before:
pp: R : Type u_1
inst✝⁶ : Semiring R
M : Type u_8
N : Type u_9
P : Type u_10
inst✝⁵ : AddCommGroup M
inst✝⁴ : AddCommGroup N
inst✝³ : AddCommMonoid P
inst✝² : Module R N
inst✝¹ : Module R M
inst✝ : Module R P
f : M →ₗ[R] N
⊢ Exact ⇑f ⇑0 ↔ Surjective ⇑f

Tactic:
by
  simp [range_eq_top, exact_iff, eqComm]

Goal state after:
Module: Mathlib.Data.Rel

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
ι : Sort u_5
R✝ R₁✝ R₂✝ : SetRel α β
S✝ : SetRel β γ
s s₁ s₂ : Set α
t t₁ t₂ : Set β
u : Set γ
a✝ a₁ a₂ : α
b✝ : β
c✝ : γ
R R₁ R₂ : SetRel α α
S : SetRel β β
a b c : α
f : α → β
inst✝ : R.IsSymm
⊢ ∀ (a b : β), (a, b) ∈ Prod.map f f '' R → (b, a) ∈ Prod.map f f '' R

Tactic:
simp only [Set.mem_image, Prod.exists, Prod.map_apply, Prod.mk.injEq, forall_exists_index,
      and_imp]
    rintro _ _ a₁ a₂ ha rfl rfl
    exact ⟨_, _, R.symm ha, rfl, rfl⟩

Goal state after:
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.length + 1 = 1

Tactic:
hs,

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

Goal state before:
pp: G : Type u
H : Type v
inst✝³ : Mul G
inst✝² : Mul H
inst✝¹ : TwoUniqueProds G
inst✝ : TwoUniqueProds H
⊢ TwoUniqueProds (G × H)

Tactic:
have : ∀ b, TwoUniqueProds (I G H b) := Bool.rec ?_ ?_
  · exact of_injective_mulHom (downMulHom H) down_injective ‹_›
  · refine of_injective_mulHom (Prod.upMulHom G H) (fun x y he ↦ Prod.ext ?_ ?_)
      (TwoUniqueProds.instForall <| I G H) <;> apply up_injective
    exacts [congr_fun he false, congr_fun he true]
  · exact of_injective_mulHom (downMulHom G) down_injective ‹_›

Goal state after:
Module: Mathlib.Order.KrullDimension

Goal state before:
pp: α : Type u_1
inst✝ : Preorder α
a : α
n : ℕ∞
⊢ ⨆ p, ⨆ (_ : RelSeries.last p ≤ a), ↑p.length ≤ n ↔ ∀ ⦃p : LTSeries α⦄, RelSeries.last p ≤ a → ↑p.length ≤ n

Tactic:
iSup₂_le_iff

Goal state after:
α : Type u_1
inst✝ : Preorder α
a : α
n : ℕ∞
⊢ (∀ (i : LTSeries α), RelSeries.last i ≤ a → ↑i.length ≤ n) ↔ ∀ ⦃p : LTSeries α⦄, RelSeries.last p ≤ a → ↑p.length ≤ n
Module: Mathlib.Order.KrullDimension

Goal state before:
pp: α : Type u_1
inst✝ : Preorder α
a : α
n : ℕ∞
⊢ ⨆ p, ⨆ (_ : a ≤ RelSeries.head p), ↑p.length ≤ n ↔ ∀ ⦃p : LTSeries α⦄, a ≤ RelSeries.head p → ↑p.length ≤ n

Tactic:
iSup₂_le_iff

Goal state after:
α : Type u_1
inst✝ : Preorder α
a : α
n : ℕ∞
⊢ (∀ (i : LTSeries α), a ≤ RelSeries.head i → ↑i.length ≤ n) ↔ ∀ ⦃p : LTSeries α⦄, a ≤ RelSeries.head p → ↑p.length ≤ n
Module: Mathlib.Algebra.Exact.Basic

Goal state before:
pp: R : Type u_1
M : Type u_2
N : Type u_4
P : Type u_6
inst✝⁶ : Ring R
inst✝⁵ : AddCommGroup M
inst✝⁴ : AddCommGroup N
inst✝³ : AddCommGroup P
inst✝² : Module R M
inst✝¹ : Module R N
inst✝ : Module R P
f : M →ₗ[R] N
g : N →ₗ[R] P
hfg : Exact ⇑f ⇑g
p : Submodule R M
q : Submodule R N
r : Submodule R P
hpq : p ≤ comap f q
hqr : q ≤ comap g r
⊢ comap g r = g.ker ⊔ q ↔ g.range ⊓ r ≤ map g q

Tactic:
sup_comm,

Goal state after:
R : Type u_1
M : Type u_2
N : Type u_4
P : Type u_6
inst✝⁶ : Ring R
inst✝⁵ : AddCommGroup M
inst✝⁴ : AddCommGroup N
inst✝³ : AddCommGroup P
inst✝² : Module R M
inst✝¹ : Module R N
inst✝ : Module R P
f : M →ₗ[R] N
g : N →ₗ[R] P
hfg : Exact ⇑f ⇑g
p : Submodule R M
q : Submodule R N
r : Submodule R P
hpq : p ≤ comap f q
hqr : q ≤ comap g r
⊢ comap g r = q ⊔ g.ker ↔ g.range ⊓ r ≤ map g q
Module: Mathlib.Order.KrullDimension

Goal state before:
pp: α : Type u_1
inst✝ : Preorder α
a : α
n : ℕ∞
⊢ (∀ ⦃p : LTSeries α⦄, RelSeries.last p = a → ↑p.length ≤ n) ↔ ⨆ p, ⨆ (_ : RelSeries.last p = a), ↑p.length ≤ n

Tactic:
iSup₂_le_iff

Goal state after:
α : Type u_1
inst✝ : Preorder α
a : α
n : ℕ∞
⊢ (∀ ⦃p : LTSeries α⦄, RelSeries.last p = a → ↑p.length ≤ n) ↔ ∀ (i : LTSeries α), RelSeries.last i = a → ↑i.length ≤ n
Module: Mathlib.Order.KrullDimension

Goal state before:
pp: α : Type u_1
inst✝ : Preorder α
a : α
n : ℕ∞
⊢ ⨆ p, ⨆ (_ : RelSeries.head p = a), ↑p.length ≤ n ↔ ∀ ⦃p : LTSeries α⦄, RelSeries.head p = a → ↑p.length ≤ n

Tactic:
iSup₂_le_iff

Goal state after:
α : Type u_1
inst✝ : Preorder α
a : α
n : ℕ∞
⊢ (∀ (i : LTSeries α), RelSeries.head i = a → ↑i.length ≤ n) ↔ ∀ ⦃p : LTSeries α⦄, RelSeries.head p = a → ↑p.length ≤ n
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
p : Submodule R M
m : M
_hm : m ∈ p
n : N
hn : n = 0
⊢ (f m) n ∈ ⊥

Tactic:
hn,

Goal state after:
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
p : Submodule R M
m : M
_hm : m ∈ p
n : N
hn : n = 0
⊢ (f m) 0 ∈ ⊥
Module: Mathlib.Order.KrullDimension

Goal state before:
pp: α : Type u_1
inst✝ : Preorder α
x y : α
hxy : x < y
hfin : height x < ⊤
⊢ ⨆ p, ⨆ (_ : RelSeries.last p = x), ↑p.length + 1 ≤ height y

Tactic:
iSup₂_le_iff

Goal state after:
α : Type u_1
inst✝ : Preorder α
x y : α
hxy : x < y
hfin : height x < ⊤
⊢ ∀ (i : LTSeries α), RelSeries.last i = x → ↑i.length + 1 ≤ height y
Module: Mathlib.Order.KrullDimension

Goal state before:
pp: case top
α : Type u_1
inst✝ : Preorder α
a : α
n : ℕ
hne : Nonempty { p // RelSeries.last p = a }
ha : ¬BddAbove (Set.range fun x ↦ (↑x).length)
⊢ ∃ p, RelSeries.last p = a ∧ p.length = n

Tactic:
bddAbove_def

Goal state after:
case top
α : Type u_1
inst✝ : Preorder α
a : α
n : ℕ
hne : Nonempty { p // RelSeries.last p = a }
ha : ¬∃ x, ∀ y ∈ Set.range fun x ↦ (↑x).length, y ≤ x
⊢ ∃ p, RelSeries.last p = a ∧ p.length = n
Module: Mathlib.Order.KrullDimension

Goal state before:
pp: α : Type u_1
inst✝ : Preorder α
x : α
n : ℕ
| ⨆ y, ⨆ (_ : y < x), height y + 1 ≤ ↑n

Tactic:
iSup₂_le_iff

Goal state after:
α : Type u_1
inst✝ : Preorder α
x : α
n : ℕ
| ∀ i < x, height i + 1 ≤ ↑n
Module: Mathlib.Order.KrullDimension

Goal state before:
pp: α : Type u_1
inst✝ : Preorder α
x : α
h : ∀ (n : ℕ), ∃ p, RelSeries.last p = x ∧ p.length = n
⊢ ¬BddAbove (Set.range fun x_1 ↦ (↑x_1).length)

Tactic:
bddAbove_def

Goal state after:
α : Type u_1
inst✝ : Preorder α
x : α
h : ∀ (n : ℕ), ∃ p, RelSeries.last p = x ∧ p.length = n
⊢ ¬∃ x_1, ∀ y ∈ Set.range fun x_2 ↦ (↑x_2).length, y ≤ x_1
Module: Mathlib.Order.KrullDimension

Goal state before:
pp: case e'_2
α : Type u_1
inst✝ : Preorder α
x : α
n : ℕ
⊢ (∃ p, RelSeries.head p = x ∧ p.length = n) ↔ ∃ p, RelSeries.last p = x ∧ p.length = n

Tactic:
constructor <;> (intro ⟨p, hp, hl⟩; use p.reverse; constructor <;> simpa)

Goal state after:
Module: Mathlib.Order.RelSeries

Goal state before:
pp: case succ.refine_1.refine_1
α : Type u_3
inst✝² : PartialOrder α
inst✝¹ : WellFoundedLT α
inst✝ : WellFoundedGT α
n : ℕ
IH :
  ∀ (s : Fin (n + 1) → α) (h : ∀ (i : Fin n), (s i.castSucc, s i.succ) ∈ {(a, b) | a < b}),
    ∃ t i,
      t.toFun ∘ ⇑i = { length := n, toFun := s, step := h }.toFun ∧
        i 0 = 0 ∧ i (Fin.last { length := n, toFun := s, step := h }.length) = Fin.last t.length
s : Fin (n + 1 + 1) → α
h : ∀ (i : Fin (n + 1)), (s i.castSucc, s i.succ) ∈ {(a, b) | a < b}
t₁ : RelSeries {(a, b) | a ⋖ b}
i : Fin ({ length := n, toFun := s ∘ Fin.castSucc, step := ⋯ }.length + 1) ↪ Fin (t₁.length + 1)
ht : t₁.toFun ∘ ⇑i = { length := n, toFun := s ∘ Fin.castSucc, step := ⋯ }.toFun
hi₁ : i 0 = 0
hi₂ : i (Fin.last { length := n, toFun := s ∘ Fin.castSucc, step := ⋯ }.length) = Fin.last t₁.length
t₂ : ℕ → α
h₁ : t₂ 0 = s (Fin.last n).castSucc
m : ℕ
h₂ : t₂ m = s (Fin.last n).succ
ht₂ : ∀ i < m, t₂ i ⋖ t₂ (i + 1)
t₃ : RelSeries {(a, b) | a ⋖ b} := { length := m, toFun := fun x ↦ t₂ ↑x, step := ⋯ }
H : t₁.last = t₂ 0
j : Fin { length := n + 1, toFun := s, step := h }.length
eq :
  Fin.snoc (Fin.castLE ⋯ ∘ ⇑i) (Fin.last (t₁.smash t₃ H).length)
      (Fin.last { length := n + 1, toFun := s, step := h }.length) =
    (Fin.castLE ⋯ ∘ ⇑i) j
⊢ Fin.last { length := n + 1, toFun := s, step := h }.length = j.castSucc

Tactic:
obtain rfl : m = 0 := by simpa [t₃] using! (congr_arg Fin.val eq).trans_lt (i j).2

Goal state after:
case succ.refine_1.refine_1
α : Type u_3
inst✝² : PartialOrder α
inst✝¹ : WellFoundedLT α
inst✝ : WellFoundedGT α
n : ℕ
IH :
  ∀ (s : Fin (n + 1) → α) (h : ∀ (i : Fin n), (s i.castSucc, s i.succ) ∈ {(a, b) | a < b}),
    ∃ t i,
      t.toFun ∘ ⇑i = { length := n, toFun := s, step := h }.toFun ∧
        i 0 = 0 ∧ i (Fin.last { length := n, toFun := s, step := h }.length) = Fin.last t.length
s : Fin (n + 1 + 1) → α
h : ∀ (i : Fin (n + 1)), (s i.castSucc, s i.succ) ∈ {(a, b) | a < b}
t₁ : RelSeries {(a, b) | a ⋖ b}
i : Fin ({ length := n, toFun := s ∘ Fin.castSucc, step := ⋯ }.length + 1) ↪ Fin (t₁.length + 1)
ht : t₁.toFun ∘ ⇑i = { length := n, toFun := s ∘ Fin.castSucc, step := ⋯ }.toFun
hi₁ : i 0 = 0
hi₂ : i (Fin.last { length := n, toFun := s ∘ Fin.castSucc, step := ⋯ }.length) = Fin.last t₁.length
t₂ : ℕ → α
h₁ : t₂ 0 = s (Fin.last n).castSucc
H : t₁.last = t₂ 0
j : Fin { length := n + 1, toFun := s, step := h }.length
h₂ : t₂ 0 = s (Fin.last n).succ
ht₂ : ∀ i < 0, t₂ i ⋖ t₂ (i + 1)
t₃ : RelSeries {(a, b) | a ⋖ b} := { length := 0, toFun := fun x ↦ t₂ ↑x, step := ⋯ }
eq :
  Fin.snoc (Fin.castLE ⋯ ∘ ⇑i) (Fin.last (t₁.smash t₃ H).length)
      (Fin.last { length := n + 1, toFun := s, step := h }.length) =
    (Fin.castLE ⋯ ∘ ⇑i) j
⊢ Fin.last { length := n + 1, toFun := s, step := h }.length = j.castSucc