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

Goal state before:
pp: case some.inr
ι : Type u
α : Option ι → Type v
inst✝¹ : DecidableEq ι
inst✝ : (i : Option ι) → Zero (α i)
i : ι
x : α (some i)
j : ι
hij : j ≠ i
⊢ (single i x) j = (single (some i) x) (some j)

Tactic:
rw [single_eq_of_ne hij, single_eq_of_ne ((Option.some_injective _).ne hij)]

Goal state after:
Module: Mathlib.Data.DFinsupp.Defs

Goal state before:
pp: ι : Type u
α : Option ι → Type v
inst✝¹ : DecidableEq ι
inst✝ : (i : Option ι) → Zero (α i)
i : ι
x : α (some i)
⊢ extendWith 0 (single i x) = single (some i) x

Tactic:
ext (_ | j)
  · rw [extendWith_none, single_eq_of_ne (Option.some_ne_none _).symm]
  · rw [extendWith_some]
    obtain rfl | hij := Decidable.eq_or_ne j i
    · rw [single_eq_same, single_eq_same]
    · rw [single_eq_of_ne hij, single_eq_of_ne ((Option.some_injective _).ne hij)]

Goal state after:
Module: Mathlib.LinearAlgebra.DFinsupp

Goal state before:
pp: case h.hf
ι : 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 : ι), ↥(⨆ (_ : i ∈ s), p i)
hμ : (μ.sum fun x xi ↦ ↑xi) = a
x : ι
a✝ : x ∈ s
hx : μ x = 0
⊢ (fun x xi ↦ ↑xi) x (μ x) = 0

Tactic:
rw [hx]

Goal state after:
case h.hf
ι : 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 : ι), ↥(⨆ (_ : i ∈ s), p i)
hμ : (μ.sum fun x xi ↦ ↑xi) = a
x : ι
a✝ : x ∈ s
hx : μ x = 0
⊢ (fun x xi ↦ ↑xi) x 0 = 0
Module: Mathlib.LinearAlgebra.DFinsupp

Goal state before:
pp: case mpr.refine_2
ι : 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
x : ι
a✝ : x ∈ s
hx : (DFinsupp.mk s fun i ↦ ⟨↑(μ ↑i), ⋯⟩) x = 0
⊢ ↑((DFinsupp.mk s fun i ↦ ⟨↑(μ ↑i), ⋯⟩) x) = 0

Tactic:
rw [hx]

Goal state after:
case mpr.refine_2
ι : 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
x : ι
a✝ : x ∈ s
hx : (DFinsupp.mk s fun i ↦ ⟨↑(μ ↑i), ⋯⟩) x = 0
⊢ ↑0 = 0
Module: Mathlib.LinearAlgebra.LinearIndependent.Lemmas

Goal state before:
pp: ι : Type u'
R : Type u_2
M : Type u_4
inst✝³ : DecidableEq ι
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
f : ι → M
hf : LinearIndependent R f
i : ι
m : M
hg : ∃ r ∈ nonZeroDivisors R, ∃ l, l i ∈ nonZeroDivisors R ∧ r • m = (linearCombination R f) l
⊢ LinearIndependent R (Function.update f i m)

Tactic:
rw [linearIndependent_iff] at hf ⊢
  obtain ⟨r, hr, l, hl, hg⟩ := hg
  intros l' hl'
  apply_fun (r • ·) at hl'
  simp_rw [Pi.update_eq_sub_add_single, ← bilinearCombination_apply _ (S := R), map_add, map_sub,
    bilinearCombination_apply, LinearMap.add_apply, LinearMap.sub_apply,
    linearCombination_single_index, smul_add, smul_sub, smul_zero, smul_comm r (l' i) m,
    hg, ← LinearMap.map_smul, smul_smul, ← linearCombination_single, ← map_sub, ← map_add] at hl'
  replace hl' : ∀ j, (r * l' j - (single i (r * l' i)) j) + l' i * l j = 0 :=
    fun j ↦ DFunLike.congr_fun (hf _ hl') j
  grind [mem_nonZeroDivisors_iff]

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

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

Tactic:
rintro ⟨fi, rfl, rfl⟩

Goal state after:
case h.mpr
α : Type u_1
inst✝ : Monoid α
n : ℕ
fi : Fin n → (s : Set α) × ↑s
⊢ ∃ f, (List.ofFn fun i ↦ ↑(f i)).prod = (List.ofFn ((fun x ↦ ↑x.snd) ∘ fi)).prod
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
s : Set V
t✝¹ : Finset V
hs : LinearIndepOn K id s
hst✝¹ : s ⊆ ↑(span K ↑t✝¹)
t✝ : Finset V
b₁ : V
t : Finset V
hb₁t : b₁ ∉ t
ih :
  ∀ (s' : Finset V),
    ↑s' ⊆ s → s ∩ ↑t = ∅ → s ⊆ ↑(span K ↑(s' ∪ t)) → ∃ t', ↑t' ⊆ s ∪ ↑t ∧ s ⊆ ↑t' ∧ t'.card = (s' ∪ t).card
s' : Finset V
hs' : ↑s' ⊆ s
hst✝ : s ∩ ↑(insert b₁ t) = ∅
hss' : s ⊆ ↑(span K ↑(s' ∪ insert b₁ t))
hb₁s : b₁ ∉ s
hb₁s' : b₁ ∉ s'
hst : s ∩ ↑t = ∅
this✝¹ : ¬s ⊆ ↑(span K ↑(s' ∪ t))
b₂ : V
hb₂s : b₂ ∈ s
hb₂t : b₂ ∉ ↑(span K ↑(s' ∪ t))
hb₂t' : b₂ ∉ s' ∪ t
b₃ : V
hb₃✝ : b₃ ∈ s
this✝ : ↑(s' ∪ insert b₁ t) ⊆ insert b₁ (insert b₂ ↑(s' ∪ t))
hb₃ : b₃ ∈ span K (insert b₁ (insert b₂ ↑(s' ∪ t)))
this : s ⊆ ↑(span K (insert b₁ ↑(s' ∪ t)))
⊢ b₃ ∈ ↑(span K ↑(insert b₂ s' ∪ t))

Tactic:
have hb₁ : b₁ ∈ span K (insert b₂ ↑(s' ∪ t)) :=
            mem_span_insert_exchange (this hb₂s) hb₂t

Goal state after:
K : Type u_3
V : Type u
inst✝² : DivisionRing K
inst✝¹ : AddCommGroup V
inst✝ : Module K V
s : Set V
t✝¹ : Finset V
hs : LinearIndepOn K id s
hst✝¹ : s ⊆ ↑(span K ↑t✝¹)
t✝ : Finset V
b₁ : V
t : Finset V
hb₁t : b₁ ∉ t
ih :
  ∀ (s' : Finset V),
    ↑s' ⊆ s → s ∩ ↑t = ∅ → s ⊆ ↑(span K ↑(s' ∪ t)) → ∃ t', ↑t' ⊆ s ∪ ↑t ∧ s ⊆ ↑t' ∧ t'.card = (s' ∪ t).card
s' : Finset V
hs' : ↑s' ⊆ s
hst✝ : s ∩ ↑(insert b₁ t) = ∅
hss' : s ⊆ ↑(span K ↑(s' ∪ insert b₁ t))
hb₁s : b₁ ∉ s
hb₁s' : b₁ ∉ s'
hst : s ∩ ↑t = ∅
this✝¹ : ¬s ⊆ ↑(span K ↑(s' ∪ t))
b₂ : V
hb₂s : b₂ ∈ s
hb₂t : b₂ ∉ ↑(span K ↑(s' ∪ t))
hb₂t' : b₂ ∉ s' ∪ t
b₃ : V
hb₃✝ : b₃ ∈ s
this✝ : ↑(s' ∪ insert b₁ t) ⊆ insert b₁ (insert b₂ ↑(s' ∪ t))
hb₃ : b₃ ∈ span K (insert b₁ (insert b₂ ↑(s' ∪ t)))
this : s ⊆ ↑(span K (insert b₁ ↑(s' ∪ t)))
hb₁ : b₁ ∈ span K (insert b₂ ↑(s' ∪ t))
⊢ b₃ ∈ ↑(span K ↑(insert b₂ s' ∪ t))
Module: Mathlib.Algebra.MonoidAlgebra.Defs

Goal state before:
pp: R : Type u_1
M : Type u_4
inst✝² : Semiring R
inst✝¹ : Monoid M
inst✝ : Subsingleton M
r : R
m : M
⊢ ((uniqueRingEquiv M).symm r).coeff m = r

Tactic:
simp [Subsingleton.elim m 1]

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 : Function.Injective ⇑f
h : UniqueMul A B a0 b0
x✝¹ x✝ : H
⊢ x✝¹ ∈ image (⇑f) A → x✝ ∈ image (⇑f) B → x✝¹ * x✝ = f a0 * f b0 → x✝¹ = f a0 ∧ x✝ = f b0

Tactic:
simp_rw [Finset.mem_image]
    rintro ⟨a, aA, rfl⟩ ⟨b, bB, rfl⟩ ab
    simp_rw [← map_mul, hf.eq_iff] at ab ⊢
    exact h aA bB ab

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

Goal state before:
pp: case neg
G : Type u_1
inst✝ : Mul G
A B : Finset G
h : 1 < #A * #B → ∃ p1 ∈ A ×ˢ B, ∃ p2 ∈ A ×ˢ B, p1 ≠ p2 ∧ UniqueMul A B p1.1 p1.2 ∧ UniqueMul A B p2.1 p2.2
hA : A.Nonempty
hB : B.Nonempty
hc : 1 < #A ∨ 1 < #B
⊢ ∃ a ∈ A, ∃ b ∈ B, UniqueMul A B a b

Tactic:
rw [← Finset.card_pos] at hA hB

Goal state after:
case neg
G : Type u_1
inst✝ : Mul G
A B : Finset G
h : 1 < #A * #B → ∃ p1 ∈ A ×ˢ B, ∃ p2 ∈ A ×ˢ B, p1 ≠ p2 ∧ UniqueMul A B p1.1 p1.2 ∧ UniqueMul A B p2.1 p2.2
hA : 0 < #A
hB : 0 < #B
hc : 1 < #A ∨ 1 < #B
⊢ ∃ a ∈ A, ∃ b ∈ B, UniqueMul A B a b
Module: Mathlib.Data.Finset.Sort

Goal state before:
pp: α : Type u_1
inst✝ : LinearOrder α
s : Finset α
k : ℕ
h : #s = k
hz : 0 < k
⊢ (s.orderEmbOfFin h) ⟨0, hz⟩ = s.min' ⋯

Tactic:
by
  simp only [orderEmbOfFin_apply, Fin.getElem_fin, sorted_zero_eq_min']

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

Goal state before:
pp: α : Type u_1
M : Type u_2
R : Type u_5
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
⊢ span R {x | ∃ i x_1, single i x_1 = x} = ⊤

Tactic:
by
  refine eq_top_iff'.mpr fun x ↦ ?_
  induction x using Finsupp.induction_linear with
  | zero => exact Submodule.zero_mem ..
  | add f g f_in g_in => exact add_mem f_in g_in
  | single a b => exact mem_span_of_mem ⟨a, b, rfl⟩

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

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

Tactic:
rw [← support_nonempty] at h

Goal state after:
R : Type u
inst✝ : Semiring R
p : R[X]
h : p.support.Nonempty
⊢ p.coeffs.Nonempty
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
G : Type u_4
inst✝⁴ : AddCommGroup G
inst✝³ : Module R G
p q : Submodule R E
S : Type u_5
inst✝² : Semiring S
M : Type u_6
inst✝¹ : AddCommMonoid M
inst✝ : Module S M
m : Submodule S M
h : IsCompl p q
⊢ (↥p × ↥q) ≃ₗ[R] E

Tactic:
apply LinearEquiv.ofBijective (p.subtype.coprod q.subtype)

Goal state after:
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
G : Type u_4
inst✝⁴ : AddCommGroup G
inst✝³ : Module R G
p q : Submodule R E
S : Type u_5
inst✝² : Semiring S
M : Type u_6
inst✝¹ : AddCommMonoid M
inst✝ : Module S M
m : Submodule S M
h : IsCompl p q
⊢ Function.Bijective ⇑(p.subtype.coprod q.subtype)
Module: Mathlib.Algebra.Group.UniqueProds.Basic

Goal state before:
pp: case pos
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:
rw [hA]

Goal state after:
case pos
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 ∈ B | a i = p2.2}) →
    ∃ p1 ∈ A ×ˢ {a ∈ B | a i = p2.2},
      ∃ p2_1 ∈ A ×ˢ {a ∈ B | a i = p2.2},
        p1 ≠ p2_1 ∧ UniqueMul A ({a ∈ B | a i = p2.2}) p1.1 p1.2 ∧ UniqueMul A ({a ∈ B | a i = p2.2}) p2_1.1 p2_1.2
Module: Mathlib.Algebra.Exact.Basic

Goal state before:
pp: R : Type u_1
M : Type u_2
M' : Type u_3
N : Type u_4
N' : Type u_5
P : Type u_6
P' : Type u_7
inst✝⁶ : Semiring 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
h : Exact ⇑f ⇑g
hf : Injective ⇑f
l : { l // g ∘ₗ l = LinearMap.id }
h₁ : ∀ (x : P), g (↑l x) = x
h₂ : ∀ (x : M), g (f x) = 0
x : N
y : M
hy : f y = x - ↑l (g x)
⊢ (f ∘ₗ fst R M P + ↑l ∘ₗ snd R M P) (y, g x) = x

Tactic:
simp [hy]

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

Goal state before:
pp: case pos
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:
rw [hA]

Goal state after:
case pos
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 ∈ B | a i = p1.2}) →
    ∃ p1_1 ∈ A ×ˢ {a ∈ B | a i = p1.2},
      ∃ p2 ∈ A ×ˢ {a ∈ B | a i = p1.2},
        p1_1 ≠ p2 ∧ UniqueMul A ({a ∈ B | a i = p1.2}) p1_1.1 p1_1.2 ∧ UniqueMul A ({a ∈ B | a i = p1.2}) p2.1 p2.2
Module: Mathlib.Order.RelSeries

Goal state before:
pp: α : Type u_1
r : SetRel α α
l : List α
l_ne_nil : l ≠ []
hl : List.IsChain (fun x1 x2 ↦ (x1, x2) ∈ r) l
⊢ (fromListIsChain l l_ne_nil hl).head = l.head l_ne_nil

Tactic:
by
  simp [← apply_zero, List.getElem_zero_eq_head]

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

Goal state before:
pp: case refine_5
G : Type u
inst✝ : Mul G
h : TwoUniqueProds Gᵐᵒᵖ
A✝ B✝ : Finset G
f : G ↪ Gᵐᵒᵖ := { toFun := op, inj' := ⋯ }
hc : 1 < #(map f B✝) * #(map f A✝)
p1 p2 : Gᵐᵒᵖ × Gᵐᵒᵖ
hne : p1 ≠ p2
hu1 : UniqueMul (map f B✝) (map f A✝) p1.1 p1.2
hu2 : UniqueMul (map f B✝) (map f A✝) p2.1 p2.2
h1 : p1.1 ∈ map f B✝ ∧ p1.2 ∈ map f A✝
h2 : p2.1 ∈ map f B✝ ∧ p2.2 ∈ map f A✝
⊢ (p1.2.1, p1.1.1) ≠ (p2.2.1, p2.1.1)

Tactic:
contrapose hne; rw [Prod.ext_iff] at hne ⊢
      exact ⟨unop_injective hne.2, unop_injective hne.1⟩

Goal state after:
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
h : f.range ≤ g.ker
⊢ (f.range.liftQ g h).ker = ⊥ ↔ g.ker = f.range

Tactic:
simp only [Submodule.ext_iff, mem_ker, Submodule.mem_bot, mem_range]
  constructor
  · intro hfg x
    simpa using hfg (Submodule.Quotient.mk x)
  · intro hfg x
    obtain ⟨x, rfl⟩ := Submodule.Quotient.mk_surjective _ x
    simpa using hfg x

Goal state after:
Module: Mathlib.Order.RelSeries

Goal state before:
pp: α : Type u_1
r : SetRel α α
β : Type u_2
s : SetRel β β
inst✝¹ : Preorder α
inst✝ : Preorder β
n : ℕ
f g : { f // StrictMono f.snd }
e : (fun f ↦ mk (↑(↑f).fst) (↑f).snd ⋯) f = (fun f ↦ mk (↑(↑f).fst) (↑f).snd ⋯) g
⊢ f = g

Tactic:
obtain ⟨⟨lf, f⟩, mf⟩ := f

Goal state after:
α : Type u_1
r : SetRel α α
β : Type u_2
s : SetRel β β
inst✝¹ : Preorder α
inst✝ : Preorder β
n : ℕ
g : { f // StrictMono f.snd }
lf : Fin n
f : Fin (↑lf + 1) → α
mf : StrictMono ⟨lf, f⟩.snd
e : (fun f ↦ mk (↑(↑f).fst) (↑f).snd ⋯) ⟨⟨lf, f⟩, mf⟩ = (fun f ↦ mk (↑(↑f).fst) (↑f).snd ⋯) g
⊢ ⟨⟨lf, f⟩, mf⟩ = g
Module: Mathlib.Order.KrullDimension

Goal state before:
pp: α✝ : Type u_1
inst✝¹ : Preorder α✝
α : Type u_1
inst✝ : Preorder α
x : α
n : ℕ
hfin : height x < ⊤
⊢ height x = ↑n + 1 ↔ height x < ⊤ ∧ (∃ y < x, height y = ↑n) ∧ ∀ y < x, height y ≤ ↑n

Tactic:
simp only [hfin, true_and]

Goal state after:
α✝ : Type u_1
inst✝¹ : Preorder α✝
α : Type u_1
inst✝ : Preorder α
x : α
n : ℕ
hfin : height x < ⊤
⊢ height x = ↑n + 1 ↔ (∃ y < x, height y = ↑n) ∧ ∀ y < x, height y ≤ ↑n
Module: Mathlib.Order.KrullDimension

Goal state before:
pp: α✝ : Type u_1
inst✝¹ : Preorder α✝
α : Type u_1
inst✝ : Preorder α
x : α
n : ℕ
hfin : height x < ⊤
⊢ height x = ↑n ↔ height x < ⊤ ∧ (n = 0 ∨ ∃ y < x, height y = ↑n - 1) ∧ ∀ y < x, height y < ↑n

Tactic:
simp only [hfin, true_and]

Goal state after:
α✝ : Type u_1
inst✝¹ : Preorder α✝
α : Type u_1
inst✝ : Preorder α
x : α
n : ℕ
hfin : height x < ⊤
⊢ height x = ↑n ↔ (n = 0 ∨ ∃ y < x, height y = ↑n - 1) ∧ ∀ y < x, height y < ↑n
Module: Mathlib.Order.KrullDimension

Goal state before:
pp: α✝ : Type u_1
inst✝¹ : Preorder α✝
α : Type u_1
inst✝ : Preorder α
x : α
hfin : height x < ⊤
n : ℕ
⊢ (height x < ⊤ ∧ (∃ y < x, height y = ↑n) ∧ ∀ y < x, height y ≤ ↑n) ↔
    (∃ y < x, height y = ↑n + 1 - 1) ∧ ∀ y < x, height y < ↑n + 1

Tactic:
simp only [hfin, true_and]

Goal state after:
α✝ : Type u_1
inst✝¹ : Preorder α✝
α : Type u_1
inst✝ : Preorder α
x : α
hfin : height x < ⊤
n : ℕ
⊢ ((∃ y < x, height y = ↑n) ∧ ∀ y < x, height y ≤ ↑n) ↔ (∃ y < x, height y = ↑n + 1 - 1) ∧ ∀ y < x, height y < ↑n + 1
Module: Mathlib.Order.KrullDimension

Goal state before:
pp: α : Type u_1
inst✝ : Preorder α
n : ℕ
⊢ krullDim α < ↑n ↔ ∀ (l : LTSeries α), l.length < n

Tactic:
rw [krullDim, ← WithBot.coe_natCast]
  rcases n with - | n
  · rw [ENat.natCast_zero, ← bot_eq_zero, WithBot.lt_coe_bot]
    simp
  · simp [ENat.WithBot.lt_add_one_iff, WithBot.coe_natCast]

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 : M ⊗[R] N
m : M
n : N
⊢ (s • r) • m ⊗ₜ[R] n = s • r • m ⊗ₜ[R] n

Tactic:
by rw [smul_tmul', smul_tmul', smul_tmul', smul_assoc]

Goal state after:
Module: Mathlib.Order.KrullDimension

Goal state before:
pp: case coe.h
α : Type u_1
β : Type u_2
inst✝¹ : Preorder α
inst✝ : PartialOrder β
m : ℕ
f : α →o β
h : ∀ (x : β), krullDim ↑(⇑f ⁻¹' {x}) ≤ ↑m
n : ℕ
ih : ∀ m_1 < n, ∀ (x : α), height (f x) = ↑m_1 → height x ≤ (↑m + 1) * ↑m_1 + ↑m
x : α
h' : height (f x) = ↑n
⊢ height x ≤ (↑m + 1) * ↑n + ↑m

Tactic:
| h n ih =>

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

Goal state before:
pp: case closed_under_smul
R : Type u_2
M : Type u_3
inst✝³ : Semiring R
inst✝² : AddCommMonoid M
inst✝¹ : Module R M
sR : Set R
N : Submodule R M
inst✝ : SMulCommClass R R ↥N
⊢ ∀ ⦃r : R⦄ ⦃n : M⦄,
    r ∈ sR →
      n ∈ N → r • n ∈ map (N.subtype ∘ₗ (Finsupp.lsum R) (DistribSMul.toLinearMap R ↥N)) (Finsupp.supported (↥N) R sR)

Tactic:
intro r n hr hn

Goal state after:
case closed_under_smul
R : Type u_2
M : Type u_3
inst✝³ : Semiring R
inst✝² : AddCommMonoid M
inst✝¹ : Module R M
sR : Set R
N : Submodule R M
inst✝ : SMulCommClass R R ↥N
r : R
n : M
hr : r ∈ sR
hn : n ∈ N
⊢ r • n ∈ map (N.subtype ∘ₗ (Finsupp.lsum R) (DistribSMul.toLinearMap R ↥N)) (Finsupp.supported (↥N) R sR)
Module: Mathlib.LinearAlgebra.TensorProduct.Map

Goal state before:
pp: 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 : N →ₗ[R] N
n : ℕ
⊢ lTensor M f ^ n = lTensor M (f ^ n)

Tactic:
have h := TensorProduct.map_pow (id : M →ₗ[R] M) f n

Goal state after:
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 : N →ₗ[R] N
n : ℕ
h : map id f ^ n = map (id ^ n) (f ^ n)
⊢ lTensor M f ^ n = lTensor M (f ^ n)
Module: Mathlib.Algebra.Ring.Submonoid.Pointwise

Goal state before:
pp: M✝ : Type u_1
R : Type u_2
A : Type u_3
inst✝ : NonAssocSemiring R
M : AddSubmonoid R
⊢ closure 1 * M = M

Tactic:
← closure_eq M,

Goal state after:
M✝ : Type u_1
R : Type u_2
A : Type u_3
inst✝ : NonAssocSemiring R
M : AddSubmonoid R
⊢ closure 1 * closure ↑M = closure ↑M
Module: Mathlib.Algebra.Ring.Submonoid.Pointwise

Goal state before:
pp: M✝ : Type u_1
R : Type u_2
A : Type u_3
inst✝ : NonAssocSemiring R
M : AddSubmonoid R
⊢ M * closure 1 = M

Tactic:
← closure_eq M,

Goal state after:
M✝ : Type u_1
R : Type u_2
A : Type u_3
inst✝ : NonAssocSemiring R
M : AddSubmonoid R
⊢ closure ↑M * closure 1 = closure ↑M