mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.LinearAlgebra.LinearIndependent.Lemmas

Goal state before:
pp: ι : Type u'
R : Type u_2
M : Type u_4
inst✝² : Ring R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
i j : ι
f : ι → M
hij : i ≠ j
⊢ LinearIndepOn R f {i, j} ↔ ∀ (c d : R), c • f i + d • f j = 0 → c = 0 ∧ d = 0

Tactic:
rw [linearIndepOn_iff'']

Goal state after:
ι : Type u'
R : Type u_2
M : Type u_4
inst✝² : Ring R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
i j : ι
f : ι → M
hij : i ≠ j
⊢ (∀ (t : Finset ι) (g : ι → R), ↑t ⊆ {i, j} → (∀ i ∉ t, g i = 0) → ∑ i ∈ t, g i • f i = 0 → ∀ i ∈ t, g i = 0) ↔
    ∀ (c d : R), c • f i + d • f j = 0 → c = 0 ∧ d = 0
Module: Mathlib.LinearAlgebra.DFinsupp

Goal state before:
pp: case mpr
ι : 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 : ι
f : ι →₀ N
hf : ∀ (i_1 : ι), f i_1 ∈ ⨆ (_ : i_1 ≠ i), p i_1
hx : (f.sum fun _i xi ↦ xi) ∈ p i
hsup : (f.sum fun _i xi ↦ xi) ∈ ⨆ j, ⨆ (_ : j ≠ i), p j
h : (f.sum fun _i xi ↦ xi) ≠ 0
⊢ ∃ s v, (∀ i ∈ s, v i ∈ p i) ∧ ∑ i ∈ s, v i = 0 ∧ ∃ i ∈ s, v i ≠ 0

Tactic:
use insert i f.support, fun j ↦ if j = i then -f.sum fun _ x ↦ x else f j

Goal state after:
case h
ι : 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 : ι
f : ι →₀ N
hf : ∀ (i_1 : ι), f i_1 ∈ ⨆ (_ : i_1 ≠ i), p i_1
hx : (f.sum fun _i xi ↦ xi) ∈ p i
hsup : (f.sum fun _i xi ↦ xi) ∈ ⨆ j, ⨆ (_ : j ≠ i), p j
h : (f.sum fun _i xi ↦ xi) ≠ 0
⊢ (∀ i_1 ∈ insert i f.support, (fun j ↦ if j = i then -f.sum fun x x_1 ↦ x_1 else f j) i_1 ∈ p i_1) ∧
    ∑ i_1 ∈ insert i f.support, (fun j ↦ if j = i then -f.sum fun x x_1 ↦ x_1 else f j) i_1 = 0 ∧
      ∃ i_1 ∈ insert i f.support, (fun j ↦ if j = i then -f.sum fun x x_1 ↦ x_1 else f j) i_1 ≠ 0
Module: Mathlib.LinearAlgebra.LinearIndependent.Lemmas

Goal state before:
pp: case left
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
s t : R
hst : s • (a • x + b • y) + t • (c • x + d • y) = 0
h₁ : a • s + c • t = 0
h₂ : b • s + d • t = 0
⊢ s = 0

pp: case right
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
s t : R
hst : s • (a • x + b • y) + t • (c • x + d • y) = 0
h₁ : a • s + c • t = 0
h₂ : b • s + d • t = 0
⊢ t = 0

Tactic:
· suffices (a * d) • s = (b * c) • s by
      by_contra hs; exact h (_root_.smul_left_injective S hs ‹_›)
    calc (a * d) • s
        = d • a • s := by rw [mul_comm, mul_smul]
      _ = -(d • c • t) := by rw [eq_neg_iff_add_eq_zero, ← smul_add, h₁, smul_zero]
      _ = (b * c) • s := ?_
    · rw [mul_comm, mul_smul, neg_eq_iff_add_eq_zero, add_comm, smul_comm d c, ← smul_add, h₂,
        smul_zero]

Goal state after:
case right
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
s t : R
hst : s • (a • x + b • y) + t • (c • x + d • y) = 0
h₁ : a • s + c • t = 0
h₂ : b • s + d • t = 0
⊢ t = 0
Module: Mathlib.LinearAlgebra.LinearIndependent.Lemmas

Goal state before:
pp: ι : Type u'
R : Type u_2
M : Type u_4
inst✝² : Ring R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
f : ι → Set M
hl : ∀ (i : ι), LinearIndepOn R id (f i)
hd : ∀ (i : ι) (t : Set ι), t.Finite → i ∉ t → Disjoint (span R (f i)) (⨆ i ∈ t, span R (f i))
⊢ LinearIndepOn R id (⋃ i, f i)

Tactic:
iUnion_eq_iUnion_finset f

Goal state after:
ι : Type u'
R : Type u_2
M : Type u_4
inst✝² : Ring R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
f : ι → Set M
hl : ∀ (i : ι), LinearIndepOn R id (f i)
hd : ∀ (i : ι) (t : Set ι), t.Finite → i ∉ t → Disjoint (span R (f i)) (⨆ i ∈ t, span R (f i))
⊢ LinearIndepOn R id (⋃ t, ⋃ i ∈ t, f i)
Module: Mathlib.Algebra.Group.AddChar

Goal state before:
pp: A : Type u_1
B : Type u_2
M : Type u_3
inst✝² : AddMonoid A
inst✝¹ : AddMonoid B
inst✝ : Monoid M
f : A →+ B
hf : Surjective ⇑f
⊢ Injective fun ψ ↦ ψ.compAddMonoidHom f

Tactic:
rintro ψ χ h; rw [DFunLike.ext'_iff] at h ⊢; exact hf.injective_comp_right h

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
x : V
n : ℕ
v : Fin n → V
⊢ LinearIndependent K (Fin.cons x v) ↔ LinearIndependent K v ∧ x ∉ span K (range v)

Tactic:
by
  rw [← linearIndependent_equiv (finSuccEquiv n).symm, linearIndependent_option]
  rfl

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

Goal state before:
pp: ι : Type u'
K : Type u_3
V : Type u
inst✝² : DivisionRing K
inst✝¹ : AddCommGroup V
inst✝ : Module K V
v : ι → V
t : Set V
hsp : span K t = span K (range v)
hli : LinearIndependent K Subtype.val
f : ⦃a : V⦄ → a ∈ t → ι
hf : ∀ ⦃a : V⦄ (a_1 : a ∈ t), v (f a_1) = a
s : Set ι := range fun a ↦ f ⋯
hs : ∀ {i : ι}, i ∈ s → v i ∈ t
f' : ↑s → ↑t := fun a ↦ ⟨v ↑a, ⋯⟩
⊢ Subtype.val ∘ f' = v ∘ Subtype.val

Tactic:
ext; simp [f']

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

Goal state before:
pp: R : Type u_1
M : Type u_4
N : Type u_5
inst✝¹ : Semiring R
inst✝ : AddCommMonoid N
m : M
r : R
h : M → R → N
h_zero : h m 0 = 0
⊢ (single m r).coeff.sum h = h m r

Tactic:
simp [h_zero]

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

Goal state before:
pp: R : Type u_1
M : Type u_4
inst✝¹ : Semiring R
r : R
m : M
inst✝ : Mul M
hm : ∀ (m' : M), Commute m m'
hr : ∀ (r' : R), Commute r r'
x : R[M]
⊢ Commute (single m r) x

Tactic:
by
  have : AddMonoidHom.mulLeft (single m r) = AddMonoidHom.mulRight (single m r) := by
    ext m' r' : 2; exact single_commute_single (hm m') (hr r')
  exact congr($this x)

Goal state after:
Module: Mathlib.Algebra.Ring.Action.Rat

Goal state before:
pp: R : Type u_1
inst✝ : DivisionSemiring R
a : ℚ≥0
x y : R
⊢ a • (x + y) = a • x + a • y

Tactic:
by rw [smul_def, smul_def, smul_def, mul_add]

Goal state after:
Module: Mathlib.Algebra.Ring.Action.Rat

Goal state before:
pp: R : Type u_1
inst✝ : DivisionRing R
a : ℚ
x y : R
⊢ a • (x + y) = a • x + a • y

Tactic:
by rw [smul_def, smul_def, smul_def, mul_add]

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

Goal state before:
pp: G : Type u_1
H : Type u_2
inst✝² : Mul G
inst✝¹ : Mul H
A B : Finset G
a0 b0 : G
inst✝ : DecidableEq H
f : G →ₙ* H
hf : ∀ ⦃a b c d : G⦄, a * b = c * d → f a = f c ∧ f b = f d → a = c ∧ b = d
h : UniqueMul (image (⇑f) A) (image (⇑f) B) (f a0) (f b0)
a b : G
ha : a ∈ A
hb : b ∈ B
ab : a * b = a0 * b0
⊢ f a * f b = f a0 * f b0

Tactic:
by simp_rw [← map_mul, ab]

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

Goal state before:
pp: α : Type u_2
inst✝ : Group α
b : α
⊢ preimage 1 (fun x ↦ x * b⁻¹) ⋯ = {b}

Tactic:
rw [preimage_mul_right_one, inv_inv]

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

Goal state before:
pp: case refine_1.add
α : Type u_1
R : Type u_5
inst✝ : Semiring R
β : Type u_7
u : α → β
f g : α →₀ R
hf : (lmapDomain R R u) f ∈ span R (Set.range fun x ↦ single (u x) 1)
hg : (lmapDomain R R u) g ∈ span R (Set.range fun x ↦ single (u x) 1)
⊢ (lmapDomain R R u) (f + g) ∈ span R (Set.range fun x ↦ single (u x) 1)

Tactic:
rw [map_add]

Goal state after:
case refine_1.add
α : Type u_1
R : Type u_5
inst✝ : Semiring R
β : Type u_7
u : α → β
f g : α →₀ R
hf : (lmapDomain R R u) f ∈ span R (Set.range fun x ↦ single (u x) 1)
hg : (lmapDomain R R u) g ∈ span R (Set.range fun x ↦ single (u x) 1)
⊢ (lmapDomain R R u) f + (lmapDomain R R u) g ∈ span R (Set.range fun x ↦ single (u x) 1)
Module: Mathlib.Algebra.Polynomial.Basic

Goal state before:
pp: R : Type u
inst✝ : Semiring R
p : R[X]
h : p.support.Nonempty
⊢ p.coeffs.Nonempty

Tactic:
obtain ⟨n, hn⟩ := h

Goal state after:
R : Type u
inst✝ : Semiring R
p : R[X]
n : ℕ
hn : n ∈ p.support
⊢ p.coeffs.Nonempty
Module: Mathlib.Algebra.Module.Submodule.Invariant

Goal state before:
pp: R : Type u_1
M : Type u_2
inst✝⁵ : Semiring R
inst✝⁴ : AddCommMonoid M
inst✝³ : Module R M
G : Type u_3
inst✝² : Monoid G
inst✝¹ : DistribMulAction G M
inst✝ : SMulCommClass G R M
x : M
g : G
⊢ MulAction.orbit G x ⊆ ⇑(DistribSMul.toLinearMap R M g) ⁻¹' ↑(span R (MulAction.orbit G x))

Tactic:
intro y hy

Goal state after:
R : Type u_1
M : Type u_2
inst✝⁵ : Semiring R
inst✝⁴ : AddCommMonoid M
inst✝³ : Module R M
G : Type u_3
inst✝² : Monoid G
inst✝¹ : DistribMulAction G M
inst✝ : SMulCommClass G R M
x : M
g : G
y : M
hy : y ∈ MulAction.orbit G x
⊢ y ∈ ⇑(DistribSMul.toLinearMap R M g) ⁻¹' ↑(span R (MulAction.orbit G x))
Module: Mathlib.LinearAlgebra.Finsupp.VectorSpace

Goal state before:
pp: ι : Type u_1
R : Type u_2
M : ι → Type u_3
inst✝³ : Semiring R
inst✝² : (i : ι) → AddCommMonoid (M i)
inst✝¹ : (i : ι) → Module R (M i)
inst✝ : DecidableEq ι
φ : ι → Type u_4
f : (i : ι) → φ i → M i
hf : ∀ (i : ι), LinearIndependent R (f i)
this :
  (linearCombination R fun ix ↦ single ix.fst (f ix.fst ix.snd)) =
    (mapRange.linearMap fun i ↦ linearCombination R (f i)) ∘ₗ ↑(sigmaFinsuppLequivDFinsupp R)
⊢ Function.Injective ⇑((mapRange.linearMap fun i ↦ linearCombination R (f i)) ∘ₗ ↑(sigmaFinsuppLequivDFinsupp R))

Tactic:
exact ((DFinsupp.mapRange_injective _ fun _ ↦ map_zero _).mpr hf).comp (Equiv.injective _)

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
⊢ ∀ y ∈ t1, ∃ x ∈ s, f x = y

Tactic:
intro y hy

Goal state after:
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
y : P
hy : y ∈ t1
⊢ ∃ x ∈ s, f x = y
Module: Mathlib.LinearAlgebra.Projection

Goal state before:
pp: case codisjoint
R : Type u_1
inst✝² : Ring R
E : Type u_2
inst✝¹ : AddCommGroup E
inst✝ : Module R E
p : Submodule R E
f : E →ₗ[R] ↥p
hf : ∀ (x : ↥p), f ↑x = x
⊢ Codisjoint p f.ker

Tactic:
codisjoint_iff_le_sup

Goal state after:
case codisjoint
R : Type u_1
inst✝² : Ring R
E : Type u_2
inst✝¹ : AddCommGroup E
inst✝ : Module R E
p : Submodule R E
f : E →ₗ[R] ↥p
hf : ∀ (x : ↥p), f ↑x = x
⊢ ⊤ ≤ p ⊔ f.ker
Module: Mathlib.RingTheory.Finiteness.Finsupp

Goal state before:
pp: case a.refine_1
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
⊢ ↑t1 ⊆ g ⁻¹' ↑s

Tactic:
intro y hy

Goal state after:
case a.refine_1
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
y : P
hy : y ∈ ↑t1
⊢ y ∈ g ⁻¹' ↑s
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
p q : Submodule R E
hpq : IsCompl p q
x : E
⊢ (q.projection p ⋯) x = x - (p.projection q hpq) x

Tactic:
eq_sub_iff_add_eq,

Goal state after:
R : Type u_1
inst✝² : Ring R
E : Type u_2
inst✝¹ : AddCommGroup E
inst✝ : Module R E
p q : Submodule R E
hpq : IsCompl p q
x : E
⊢ (q.projection p ⋯) x + (p.projection q hpq) x = x
Module: Mathlib.RingTheory.Finiteness.Finsupp

Goal state before:
pp: case a.refine_2.left
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
⊢ ∀ c ∈ l.support, (fun a m ↦ m • id (g a)) c (l c) ∈ s

Tactic:
intro y hy

Goal state after:
case a.refine_2.left
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
y : P
hy : y ∈ l.support
⊢ (fun a m ↦ m • id (g a)) y (l y) ∈ s
Module: Mathlib.Algebra.Exact.Basic

Goal state before:
pp: M : Type u_2
N : Type u_4
P : Type u_6
P' : Type u_7
f : M → N
g : N → P
g' : P → P'
inst✝¹ : One P
inst✝ : One P'
mulExact : MulExact f g
inj : Injective g'
h0 : g' 1 = 1
x : N
H : x ∈ Set.range f
⊢ (g' ∘ g) x = 1

Tactic:
rw [Function.comp_apply, mulExact x |>.mpr H, h0]

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

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

Tactic:
intro y hy

Goal state after:
case coe
s : Set ℕ∞
x : ℕ
hx : ↑x < ⊤
h : ∀ a ∈ s, a ≤ ↑x
y : ℕ∞
hy : y ∈ s
⊢ y ∈ (fun n ↦ ↑n) '' {n | n ≤ x}
Module: Mathlib.Data.ENat.Lattice

Goal state before:
pp: ι : Sort u_2
R : Type u_4
inst✝¹ : SMul R ℕ∞
inst✝ : IsScalarTower R ℕ∞ ℕ∞
f : ι → ℕ∞
c : R
⊢ c • ⨆ i, f i = ⨆ i, c • f i

Tactic:
by
  simpa using mul_iSup (c • 1) f

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

Goal state before:
pp: case neg
G✝ : Type u
H : Type v
inst✝³ : Mul G✝
inst✝² : Mul H
ι : Type u_2
G : ι → Type u_1
inst✝¹ : (i : ι) → Mul (G i)
inst✝ : ∀ (i : ι), TwoUniqueProds (G i)
A✝ : Finset ((i : ι) → G i)
x✝ : IsWellFounded (Finset ((i : ι) → G i)) fun x1 x2 ↦ x1 ⊂ x2 := isWellFounded_ssubset
A : Finset ((i : ι) → G i)
ihA :
  ∀ y ⊂ A,
    ∀ {B : Finset ((i : ι) → G i)},
      1 < #y * #B → ∃ p1 ∈ y ×ˢ B, ∃ p2 ∈ y ×ˢ B, p1 ≠ p2 ∧ UniqueMul y B p1.1 p1.2 ∧ UniqueMul y B p2.1 p2.2
B✝ B : Finset ((i : ι) → G i)
ihB : ∀ y ⊂ B, 1 < #A * #y → ∃ p1 ∈ A ×ˢ y, ∃ p2 ∈ A ×ˢ y, p1 ≠ p2 ∧ UniqueMul A y p1.1 p1.2 ∧ UniqueMul A y p2.1 p2.2
hc✝¹ : 1 < #A * #B
hA✝ : A.Nonempty
hB : B.Nonempty
hc✝ : 1 < #A ∨ 1 < #B
i : ι
p1 p2 : G i × G i
hne : p1 ≠ p2
hi1 : UniqueMul (image (fun x ↦ x i) A) (image (fun x ↦ x i) B) p1.1 p1.2
hi2 : UniqueMul (image (fun x ↦ x i) A) (image (fun x ↦ x i) B) p2.1 p2.2
h2 : {a ∈ A | a i = p2.1}.Nonempty ∧ {a ∈ B | a i = p2.2}.Nonempty
h1 : ∃ a ∈ {a ∈ A | a i = p1.1}, ∃ b ∈ {a ∈ B | a i = p1.2}, UniqueMul ({a ∈ A | a i = p1.1}) ({a ∈ B | a i = p1.2}) a b
hc : 1 < #(image (fun x ↦ x i) B) ∧ ∀ (ai : G i), {x ∈ B | x i = ai} ⊂ B
hA : ¬{a ∈ A | a i = p2.1} = A
⊢ 1 < #({a ∈ A | a i = p2.1}) * #({a ∈ B | a i = p2.2}) →
    ∃ p1 ∈ {a ∈ A | a i = p2.1} ×ˢ {a ∈ B | a i = p2.2},
      ∃ p2_1 ∈ {a ∈ A | a i = p2.1} ×ˢ {a ∈ B | a i = p2.2},
        p1 ≠ p2_1 ∧
          UniqueMul ({a ∈ A | a i = p2.1}) ({a ∈ B | a i = p2.2}) p1.1 p1.2 ∧
            UniqueMul ({a ∈ A | a i = p2.1}) ({a ∈ B | a i = p2.2}) p2_1.1 p2_1.2

Tactic:
exact ihA _ ((A.filter_subset _).ssubset_of_ne hA)

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

Goal state before:
pp: case neg
G✝ : Type u
H : Type v
inst✝³ : Mul G✝
inst✝² : Mul H
ι : Type u_2
G : ι → Type u_1
inst✝¹ : (i : ι) → Mul (G i)
inst✝ : ∀ (i : ι), TwoUniqueProds (G i)
A✝ : Finset ((i : ι) → G i)
x✝ : IsWellFounded (Finset ((i : ι) → G i)) fun x1 x2 ↦ x1 ⊂ x2 := isWellFounded_ssubset
A : Finset ((i : ι) → G i)
ihA :
  ∀ y ⊂ A,
    ∀ {B : Finset ((i : ι) → G i)},
      1 < #y * #B → ∃ p1 ∈ y ×ˢ B, ∃ p2 ∈ y ×ˢ B, p1 ≠ p2 ∧ UniqueMul y B p1.1 p1.2 ∧ UniqueMul y B p2.1 p2.2
B✝ B : Finset ((i : ι) → G i)
ihB : ∀ y ⊂ B, 1 < #A * #y → ∃ p1 ∈ A ×ˢ y, ∃ p2 ∈ A ×ˢ y, p1 ≠ p2 ∧ UniqueMul A y p1.1 p1.2 ∧ UniqueMul A y p2.1 p2.2
hc✝¹ : 1 < #A * #B
hA✝ : A.Nonempty
hB : B.Nonempty
hc✝ : 1 < #A ∨ 1 < #B
i : ι
p1 p2 : G i × G i
hne : p1 ≠ p2
hi1 : UniqueMul (image (fun x ↦ x i) A) (image (fun x ↦ x i) B) p1.1 p1.2
hi2 : UniqueMul (image (fun x ↦ x i) A) (image (fun x ↦ x i) B) p2.1 p2.2
h1 : {a ∈ A | a i = p1.1}.Nonempty ∧ {a ∈ B | a i = p1.2}.Nonempty
h2 : {a ∈ A | a i = p2.1}.Nonempty ∧ {a ∈ B | a i = p2.2}.Nonempty
hc : 1 < #(image (fun x ↦ x i) B) ∧ ∀ (ai : G i), {x ∈ B | x i = ai} ⊂ B
hA : ¬{a ∈ A | a i = p1.1} = A
⊢ 1 < #({a ∈ A | a i = p1.1}) * #({a ∈ B | a i = p1.2}) →
    ∃ p1_1 ∈ {a ∈ A | a i = p1.1} ×ˢ {a ∈ B | a i = p1.2},
      ∃ p2 ∈ {a ∈ A | a i = p1.1} ×ˢ {a ∈ B | a i = p1.2},
        p1_1 ≠ p2 ∧
          UniqueMul ({a ∈ A | a i = p1.1}) ({a ∈ B | a i = p1.2}) p1_1.1 p1_1.2 ∧
            UniqueMul ({a ∈ A | a i = p1.1}) ({a ∈ B | a i = p1.2}) p2.1 p2.2

Tactic:
exact ihA _ ((A.filter_subset _).ssubset_of_ne hA)

Goal state after:
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:
by
  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.Algebra.Group.UniqueProds.Basic

Goal state before:
pp: case refine_2
G : Type u
H : Type v
inst✝⁴ : Mul G
inst✝³ : Mul H
inst✝² : IsRightCancelMul G
inst✝¹ : LinearOrder G
inst✝ : MulLeftStrictMono G
A B : Finset G
hc : 1 < #(A ×ˢ B)
hA : A.Nonempty
hB : B.Nonempty
a0 : G
ha0 : a0 ∈ A
b0 : G
hb0 : b0 ∈ B
he0 : a0 * b0 = (A * B).max' ⋯
a1 : G
ha1 : a1 ∈ A
b1 : G
hb1 : b1 ∈ B
he1 : a1 * b1 = (A * B).min' ⋯
this : UniqueMul A B a0 b0
a b : G
ha : a ∈ A
hb : b ∈ B
he : a * b = (a1, b1).1 * (a1, b1).2
⊢ a = (a1, b1).1 ∧ b = (a1, b1).2

Tactic:
obtain hl | rfl | hl := lt_trichotomy b b1

Goal state after:
case refine_2.inl
G : Type u
H : Type v
inst✝⁴ : Mul G
inst✝³ : Mul H
inst✝² : IsRightCancelMul G
inst✝¹ : LinearOrder G
inst✝ : MulLeftStrictMono G
A B : Finset G
hc : 1 < #(A ×ˢ B)
hA : A.Nonempty
hB : B.Nonempty
a0 : G
ha0 : a0 ∈ A
b0 : G
hb0 : b0 ∈ B
he0 : a0 * b0 = (A * B).max' ⋯
a1 : G
ha1 : a1 ∈ A
b1 : G
hb1 : b1 ∈ B
he1 : a1 * b1 = (A * B).min' ⋯
this : UniqueMul A B a0 b0
a b : G
ha : a ∈ A
hb : b ∈ B
he : a * b = (a1, b1).1 * (a1, b1).2
hl : b < b1
⊢ a = (a1, b1).1 ∧ b = (a1, b1).2

case refine_2.inr.inl
G : Type u
H : Type v
inst✝⁴ : Mul G
inst✝³ : Mul H
inst✝² : IsRightCancelMul G
inst✝¹ : LinearOrder G
inst✝ : MulLeftStrictMono G
A B : Finset G
hc : 1 < #(A ×ˢ B)
hA : A.Nonempty
hB : B.Nonempty
a0 : G
ha0 : a0 ∈ A
b0 : G
hb0 : b0 ∈ B
he0 : a0 * b0 = (A * B).max' ⋯
a1 : G
ha1 : a1 ∈ A
this : UniqueMul A B a0 b0
a b : G
ha : a ∈ A
hb hb1 : b ∈ B
he1 : a1 * b = (A * B).min' ⋯
he : a * b = (a1, b).1 * (a1, b).2
⊢ a = (a1, b).1 ∧ b = (a1, b).2

case refine_2.inr.inr
G : Type u
H : Type v
inst✝⁴ : Mul G
inst✝³ : Mul H
inst✝² : IsRightCancelMul G
inst✝¹ : LinearOrder G
inst✝ : MulLeftStrictMono G
A B : Finset G
hc : 1 < #(A ×ˢ B)
hA : A.Nonempty
hB : B.Nonempty
a0 : G
ha0 : a0 ∈ A
b0 : G
hb0 : b0 ∈ B
he0 : a0 * b0 = (A * B).max' ⋯
a1 : G
ha1 : a1 ∈ A
b1 : G
hb1 : b1 ∈ B
he1 : a1 * b1 = (A * B).min' ⋯
this : UniqueMul A B a0 b0
a b : G
ha : a ∈ A
hb : b ∈ B
he : a * b = (a1, b1).1 * (a1, b1).2
hl : b1 < b
⊢ a = (a1, b1).1 ∧ b = (a1, b1).2
Module: Mathlib.Algebra.Algebra.NonUnitalHom

Goal state before:
pp: R : Type u
S : Type u₁
inst✝⁵ : Monoid R
inst✝⁴ : Monoid S
φ : R →* S
A : Type v
B : Type w
inst✝³ : NonUnitalNonAssocSemiring A
inst✝² : DistribMulAction R A
inst✝¹ : NonUnitalNonAssocSemiring B
inst✝ : DistribMulAction S B
f g : A →ₛₙₐ[φ] B
h : ↑f = ↑g
a : A
⊢ f a = g a

Tactic:
exact DFunLike.congr_fun h a

Goal state after:
Module: Mathlib.Order.RelSeries

Goal state before:
pp: α : Type u_1
r : SetRel α α
p : RelSeries r
len_pos : p.length ≠ 0
⊢ (p.tail len_pos).last = p.last

Tactic:
by
  change p _ = p _
  congr
  ext
  simp only [Fin.val_succ, Fin.val_last]
  exact Nat.succ_pred_eq_of_pos (by simpa [Nat.pos_iff_ne_zero] using len_pos)

Goal state after:
Module: Mathlib.Order.RelSeries

Goal state before:
pp: α : Type u_1
r : SetRel α α
p q : RelSeries r
h : p.last = q.head
i : Fin q.length
⊢ (p.smash q h).toFun (Fin.natAdd p.length i).succ = q.toFun i.succ

Tactic:
dsimp only [smash, Fin.succ_natAdd]
  apply Fin.addCases_right

Goal state after:
Module: Mathlib.Order.RelSeries

Goal state before:
pp: α : 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)
i : Fin m
⊢ (t₂ ↑i.castSucc, t₂ ↑i.succ) ∈ {(a, b) | a ⋖ b}

Tactic:
by simpa using! ht₂ i

Goal state after:
Module: Mathlib.Order.KrullDimension

Goal state before:
pp: case a
α : Type u_1
inst✝ : Preorder α
x y : α
hyx : y < x
p : LTSeries α
hp : RelSeries.last p = y
⊢ ↑p.length + 1 ≤ height x

Tactic:
apply le_iSup₂_of_le (p.snoc x (hp ▸ hyx)) (by simp) (by simp)

Goal state after:
Module: Mathlib.Order.KrullDimension

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

Tactic:
rw [WithBot.coe_iSup (by bddDefault)]

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

Goal state before:
pp: α : Type u_1
inst✝¹ : PartialOrder α
inst✝ : BoundedOrder α
⊢ (∀ (x : α), x = ⊥ ∨ x = ⊤) ∧ 0 < krullDim α ↔ IsSimpleOrder α

Tactic:
Order.krullDim_pos_iff_of_orderBot,

Goal state after:
α : Type u_1
inst✝¹ : PartialOrder α
inst✝ : BoundedOrder α
⊢ (∀ (x : α), x = ⊥ ∨ x = ⊤) ∧ Nontrivial α ↔ IsSimpleOrder α
Module: Mathlib.Order.KrullDimension

Goal state before:
pp: ⊢ krullDim ℕ∞ = ⊤

Tactic:
change (krullDim (WithTop ℕ) = ⊤)
  simp [← WithBot.coe_top, ← WithBot.coe_one, ← WithBot.coe_add]

Goal state after: