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

Goal state before:
pp: case mk
ι : Type u
γ : Type w
β : ι → Type v
inst✝³ : DecidableEq ι
inst✝² : (i : ι) → AddZeroClass (β i)
inst✝¹ : (i : ι) → (x : β i) → Decidable (x ≠ 0)
inst✝ : AddCommMonoid γ
φ : (i : ι) → ZeroHom (β i) γ
f : (i : ι) → β i
support'✝ : Trunc { s // ∀ (i : ι), i ∈ s ∨ f i = 0 }
s : Multiset ι
hf : ∀ (i : ι), i ∈ s ∨ f i = 0
⊢ ∀ x ∈ (↑⟨s, hf⟩).toFinset,
    (φ x) ({ toFun := f, support' := Quot.mk ⇑trueSetoid ⟨s, hf⟩ } x) =
      if { toFun := f, support' := Quot.mk ⇑trueSetoid ⟨s, hf⟩ } x ≠ 0 then
        (fun x ↦ ⇑(φ x)) x ({ toFun := f, support' := Quot.mk ⇑trueSetoid ⟨s, hf⟩ } x)
      else 0

Tactic:
intro i _

Goal state after:
case mk
ι : Type u
γ : Type w
β : ι → Type v
inst✝³ : DecidableEq ι
inst✝² : (i : ι) → AddZeroClass (β i)
inst✝¹ : (i : ι) → (x : β i) → Decidable (x ≠ 0)
inst✝ : AddCommMonoid γ
φ : (i : ι) → ZeroHom (β i) γ
f : (i : ι) → β i
support'✝ : Trunc { s // ∀ (i : ι), i ∈ s ∨ f i = 0 }
s : Multiset ι
hf : ∀ (i : ι), i ∈ s ∨ f i = 0
i : ι
a✝ : i ∈ (↑⟨s, hf⟩).toFinset
⊢ (φ i) ({ toFun := f, support' := Quot.mk ⇑trueSetoid ⟨s, hf⟩ } i) =
    if { toFun := f, support' := Quot.mk ⇑trueSetoid ⟨s, hf⟩ } i ≠ 0 then
      (fun x ↦ ⇑(φ x)) i ({ toFun := f, support' := Quot.mk ⇑trueSetoid ⟨s, hf⟩ } i)
    else 0
Module: Mathlib.LinearAlgebra.LinearIndependent.Lemmas

Goal state before:
pp: ι : Type u'
R : Type u_2
M : Type u_4
M' : Type u_5
inst✝⁴ : Semiring R
inst✝³ : AddCommMonoid M
inst✝² : AddCommMonoid M'
inst✝¹ : Module R M
inst✝ : Module R M'
f : M →ₗ[R] M'
inj : Injective ⇑f
m : ι → Submodule R M
ind : iSupIndep m
⊢ iSupIndep fun i ↦ map f (m i)

Tactic:
iSupIndep,

Goal state after:
ι : Type u'
R : Type u_2
M : Type u_4
M' : Type u_5
inst✝⁴ : Semiring R
inst✝³ : AddCommMonoid M
inst✝² : AddCommMonoid M'
inst✝¹ : Module R M
inst✝ : Module R M'
f : M →ₗ[R] M'
inj : Injective ⇑f
m : ι → Submodule R M
ind : ∀ (i : ι), Disjoint (m i) (⨆ j, ⨆ (_ : j ≠ i), m j)
⊢ ∀ (i : ι), Disjoint (map f (m i)) (⨆ j, ⨆ (_ : j ≠ i), map f (m j))
Module: Mathlib.LinearAlgebra.BilinearMap

Goal state before:
pp: R✝ : Type u_1
R₂✝ : Type u_2
S : Type u_3
S₂ : Type u_4
inst✝⁴⁶ : Semiring R✝
inst✝⁴⁵ : Semiring R₂✝
inst✝⁴⁴ : Semiring S
inst✝⁴³ : Semiring S₂
M✝ : Type u_5
M₂ : Type u_6
N✝ : Type u_7
N₂ : Type u_8
P✝ : Type u_9
P₂ : Type u_10
Pₗ : Type u_11
inst✝⁴² : AddCommMonoid M✝
inst✝⁴¹ : AddCommMonoid M₂
inst✝⁴⁰ : AddCommMonoid N✝
inst✝³⁹ : AddCommMonoid N₂
inst✝³⁸ : AddCommMonoid P✝
inst✝³⁷ : AddCommMonoid P₂
inst✝³⁶ : AddCommMonoid Pₗ
inst✝³⁵ : Module R✝ M✝
inst✝³⁴ : Module R✝ M₂
inst✝³³ : Module S N✝
inst✝³² : Module S N₂
inst✝³¹ : Module R₂✝ P✝
inst✝³⁰ : Module S₂ P✝
inst✝²⁹ : Module R✝ P₂
inst✝²⁸ : Module S₂ P₂
inst✝²⁷ : Module R✝ Pₗ
inst✝²⁶ : Module S Pₗ
M' : Type u_12
P' : Type u_13
inst✝²⁵ : AddCommGroup M'
inst✝²⁴ : AddCommGroup P'
inst✝²³ : Module R✝ M'
inst✝²² : Module R₂✝ P'
inst✝²¹ : Module S₂ P'
inst✝²⁰ : SMulCommClass S₂ R₂✝ P✝
inst✝¹⁹ : SMulCommClass S R✝ Pₗ
inst✝¹⁸ : SMulCommClass S₂ R₂✝ P'
inst✝¹⁷ : SMulCommClass S₂ R✝ P₂
ρ₁₂ : R✝ →+* R₂✝
σ₁₂✝ : S →+* S₂
R : Type u_14
R₂ : Type u_15
R₃ : Type u_16
R₄ : Type u_17
R₅ : Type u_18
M : Type u_19
N : Type u_20
P : Type u_21
Q : Type u_22
inst✝¹⁶ : Semiring R
inst✝¹⁵ : Semiring R₂
inst✝¹⁴ : Semiring R₃
inst✝¹³ : Semiring R₄
inst✝¹² : Semiring R₅
σ₁₂ : R →+* R₂
σ₂₃ : R₂ →+* R₃
σ₁₃ : R →+* R₃
σ₄₂ : R₄ →+* R₂
σ₄₃ : R₄ →+* R₃
inst✝¹¹ : AddCommMonoid M
inst✝¹⁰ : AddCommMonoid N
inst✝⁹ : AddCommMonoid P
inst✝⁸ : AddCommMonoid Q
inst✝⁷ : Module R M
inst✝⁶ : Module R₂ N
inst✝⁵ : Module R₃ P
inst✝⁴ : Module R₄ Q
inst✝³ : Module R₅ P
inst✝² : RingHomCompTriple σ₁₂ σ₂₃ σ₁₃
inst✝¹ : RingHomCompTriple σ₄₂ σ₂₃ σ₄₃
inst✝ : SMulCommClass R₃ R₅ P
σ₁₅ : R →+* R₅
h : M →ₛₗ[σ₁₅] N →ₛₗ[σ₂₃] P
g : Q →ₛₗ[σ₄₂] N
x✝¹ x✝ : M
⊢ (lcompₛₗ R₅ P σ₂₃ g) (h (x✝¹ + x✝)) = (lcompₛₗ R₅ P σ₂₃ g) (h x✝¹) + (lcompₛₗ R₅ P σ₂₃ g) (h x✝)

Tactic:
by
    simp [map_add]

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

Goal state before:
pp: case inl
ι : 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
f g : ι →₀ R
hsum : (Finsupp.linearCombination R v) f = (Finsupp.linearCombination R v) g
hc : IsChain r ∅
hfsupp : f ∈ Finsupp.supported R R (⋃ I ∈ ∅, ↑I)
hgsupp : g ∈ Finsupp.supported R R (⋃ I ∈ ∅, ↑I)
⊢ f = g

pp: case inr
ι : 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)
hsum : (Finsupp.linearCombination R v) f = (Finsupp.linearCombination R v) g
hn : c.Nonempty
⊢ f = g

Tactic:
· rw [show f = 0 by simpa using! hfsupp, show g = 0 by simpa using! hgsupp]

Goal state after:
case inr
ι : 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)
hsum : (Finsupp.linearCombination R v) f = (Finsupp.linearCombination R v) g
hn : c.Nonempty
⊢ f = g
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
inst✝ : Nontrivial R
⊢ LinearIndependent R ![a • x + b • y, c • x + d • y] ↔ LinearIndependent R ![x, y] ∧ a * d ≠ b * c

Tactic:
by
  rcases eq_or_ne (a * d) (b * c) with h | h
  · suffices ¬ LinearIndependent R ![a • x + b • y, c • x + d • y] by simpa [h]
    rw [pair_iff]
    push Not
    by_cases hbd : b = 0 ∧ d = 0
    · simp only [hbd.1, hbd.2, zero_smul, add_zero]
      by_cases hac : a = 0 ∧ c = 0; · exact ⟨1, 0, by simp [hac.1, hac.2], by simp⟩
      refine ⟨c • 1, -a • 1, ?_, by aesop⟩
      simp only [smul_assoc, one_smul, neg_smul]
      module
    refine ⟨d • 1, -b • 1, ?_, by contrapose! hbd; simp_all⟩
    simp only [smul_add, smul_assoc, one_smul, smul_smul, mul_comm d, h]
    module
  refine ⟨fun h' ↦ ⟨?_, h⟩, fun ⟨h₁, h₂⟩ ↦ pair_add_smul_add_smul_iff_aux _ _ _ _ h₂ h₁⟩
  suffices LinearIndependent R ![(a * d - b * c) • x, (a * d - b * c) • y] by
    rwa [pair_smul_iff (sub_ne_zero_of_ne h)] at this
  convert! pair_add_smul_add_smul_iff_aux d (-b) (-c) a (by simpa [mul_comm d a]) h' using 1
  ext i; fin_cases i <;> simp <;> module

Goal state after:
Module: Mathlib.Algebra.Group.AddChar

Goal state before:
pp: case refine_1
R : Type u_1
M : Type u_2
inst✝¹ : Ring R
inst✝ : CommMonoid M
ψ : AddChar R M
u : R
hu : IsUnit u
h : ψ.mulShift u = 1
⊢ ψ = 1

pp: case refine_2
R : Type u_1
M : Type u_2
inst✝¹ : Ring R
inst✝ : CommMonoid M
ψ : AddChar R M
u : R
hu : IsUnit u
⊢ ψ = 1 → ψ.mulShift u = 1

Tactic:
· ext1 y
    rw [show y = u * (hu.unit⁻¹ * y) by rw [← mul_assoc, IsUnit.mul_val_inv, one_mul]]
    simpa only [mulShift_apply] using! DFunLike.ext_iff.mp h (hu.unit⁻¹ * y)

Goal state after:
case refine_2
R : Type u_1
M : Type u_2
inst✝¹ : Ring R
inst✝ : CommMonoid M
ψ : AddChar R M
u : R
hu : IsUnit u
⊢ ψ = 1 → ψ.mulShift u = 1
Module: Mathlib.Algebra.MonoidAlgebra.Defs

Goal state before:
pp: R : Type u_1
S : Type u_2
G : Type u_3
M : Type u_4
N : Type u_5
O : Type u_6
ι : Type u_7
inst✝¹ : Ring R
inst✝ : MulOneClass M
n : ℕ
⊢ single 1 ↑↑n = ↑n

Tactic:
simp [natCast_def]

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

Goal state before:
pp: R : Type u_1
A : Type u_2
inst✝⁴ : Semiring R
inst✝³ : IsCancelAdd R
inst✝² : IsLeftCancelMulZero R
inst✝¹ : Mul A
inst✝ : UniqueProds A
f : R[A]
hf : f ≠ 0
g₁ g₂ : R[A]
eq : (fun x ↦ f * x) g₁ = (fun x ↦ f * x) g₂
⊢ g₁ = g₂

Tactic:
by
    classical
    induction hg : g₁.coeff.support ∪ g₂.coeff.support
      using Finset.eraseInduction generalizing g₁ g₂ with
    | _ s ih =>
    obtain h | h := s.eq_empty_or_nonempty <;> subst s
    · simp_all
    simp only [ne_eq, ← coeff_eq_zero, ← support_nonempty_iff] at hf
    obtain ⟨af, haf, ag, hag, uniq⟩ := UniqueProds.uniqueMul_of_nonempty hf h
    have h := coeff_mul_mul_of_uniqueMul (uniq.mono subset_rfl Finset.subset_union_left)
    dsimp only at eq
    rw [eq, coeff_mul_mul_of_uniqueMul (uniq.mono subset_rfl Finset.subset_union_right)] at h
    have := mul_left_cancel₀ (mem_support_iff.mp haf) h
    rw [← g₁.erase_add_single ag, ← g₂.erase_add_single ag, this] at eq ⊢
    simp_rw [mul_add, add_right_cancel_iff] at eq
    rw [ih ag hag eq]
    simp [Finset.erase_union_distrib]

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

Goal state before:
pp: G : Type u_1
inst✝ : Mul G
A B : Finset G
a0 b0 : G
h : UniqueMul (map { toFun := op, inj' := ⋯ } B) (map { toFun := op, inj' := ⋯ } A) (op b0) (op a0)
a b : G
aA : a ∈ A
bB : b ∈ B
ab : a * b = a0 * b0
⊢ a = a0 ∧ b = b0

Tactic:
by
  simpa [and_comm] using h (mem_map_of_mem _ bB) (mem_map_of_mem _ aA) (congr_arg op ab)

Goal state after:
Module: Mathlib.Data.Finset.Sort

Goal state before:
pp: α : Type u_1
inst✝ : LinearOrder α
s : Finset α
h : #s = (s.sort fun a b ↦ a ≤ b).length
⊢ List.map (⇑(s.orderEmbOfFin h)) (List.finRange (s.sort fun a b ↦ a ≤ b).length) = s.sort fun a b ↦ a ≤ b

Tactic:
exact List.map_getElem_finRange s.sort

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

Goal state before:
pp: R : Type u_2
M : Type u_3
inst✝³ : Semiring R
inst✝² : AddCommMonoid M
inst✝¹ : Module R M
inst✝ : Free R M
f : End R M
⊢ f ∈ Set.center (End R M) ↔ ∃ α, ∃ (hα : α ∈ Set.center R), f = smulLeft α hα

Tactic:
simp only [Semigroup.mem_center_iff, LinearMap.ext_iff, mul_apply]
  refine ⟨fun h ↦ ?_, by simp_all⟩
  by_cases! Subsingleton M
  · exact ⟨0, by simp, fun _ ↦ Subsingleton.allEq _ _⟩
  let b := Free.chooseBasis R M
  let i := b.index_nonempty.some
  have H x : f x = b.repr (f (b i)) i • x := by simpa using (h ((b.coord i).smulRight x) (b i)).symm
  exact ⟨b.coord i <| f <| b i, fun r ↦ by simpa using congr(b.coord i $(H <| r • b i)), H⟩

Goal state after:
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
y : M
hy : y ∈ MulAction.orbit G x
⊢ y ∈ ⇑(DistribSMul.toLinearMap R M g) ⁻¹' ↑(span R (MulAction.orbit G x))

Tactic:
simp only [Set.mem_preimage, DistribSMul.toLinearMap_apply, SetLike.mem_coe]

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
⊢ g • y ∈ span R (MulAction.orbit G x)
Module: Mathlib.RingTheory.Finiteness.Cardinality

Goal state before:
pp: R : Type u_1
M : Type u_2
inst✝³ : Semiring R
inst✝² : AddCommMonoid M
inst✝¹ : Module R M
inst✝ : Finite R
s : Finset M
⊢ Finite ↑↑(span R ↑s)

Tactic:
← Module.finite_iff_finite (R := R)

Goal state after:
R : Type u_1
M : Type u_2
inst✝³ : Semiring R
inst✝² : AddCommMonoid M
inst✝¹ : Module R M
inst✝ : Finite R
s : Finset M
⊢ Module.Finite R ↑↑(span R ↑s)
Module: Mathlib.Algebra.Group.UniqueProds.Basic

Goal state before:
pp: case refine_2.refine_2
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 : ι
hc :
  (1 < #(image (fun x ↦ x i) A) ∧ ∀ (ai : G i), {x ∈ A | x i = ai} ⊂ A) ∨
    1 < #(image (fun x ↦ x i) B) ∧ ∀ (ai : G i), {x ∈ B | x i = ai} ⊂ B
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 | 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
h2 : ∃ a ∈ {a ∈ A | a i = p2.1}, ∃ b ∈ {a ∈ B | a i = p2.2}, UniqueMul ({a ∈ A | a i = p2.1}) ({a ∈ B | a i = p2.2}) a b
⊢ ∃ p1 ∈ A ×ˢ B, ∃ p2 ∈ A ×ˢ B, p1 ≠ p2 ∧ UniqueMul A B p1.1 p1.2 ∧ UniqueMul A B p2.1 p2.2

Tactic:
obtain ⟨a1, ha1, b1, hb1, hu1⟩ := h1

Goal state after:
case refine_2.refine_2
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 : ι
hc :
  (1 < #(image (fun x ↦ x i) A) ∧ ∀ (ai : G i), {x ∈ A | x i = ai} ⊂ A) ∨
    1 < #(image (fun x ↦ x i) B) ∧ ∀ (ai : G i), {x ∈ B | x i = ai} ⊂ B
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 | a i = p2.1}, ∃ b ∈ {a ∈ B | a i = p2.2}, UniqueMul ({a ∈ A | a i = p2.1}) ({a ∈ B | a i = p2.2}) a b
a1 : (i : ι) → G i
ha1 : a1 ∈ {a ∈ A | a i = p1.1}
b1 : (i : ι) → G i
hb1 : b1 ∈ {a ∈ B | a i = p1.2}
hu1 : UniqueMul ({a ∈ A | a i = p1.1}) ({a ∈ B | a i = p1.2}) a1 b1
⊢ ∃ p1 ∈ A ×ˢ B, ∃ p2 ∈ A ×ˢ B, p1 ≠ p2 ∧ UniqueMul A B p1.1 p1.2 ∧ UniqueMul A B p2.1 p2.2
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
hs1 : (map f s).FG
hs2 : (s ⊓ f.ker).FG
⊢ s.FG

Tactic:
by
  have := Classical.decEq R
  have := Classical.decEq M
  have := Classical.decEq P
  obtain ⟨t1, ht1⟩ := hs1
  obtain ⟨t2, ht2⟩ := hs2
  have : ∀ y ∈ t1, ∃ x ∈ s, f x = y := by
    intro y hy
    have : y ∈ s.map f := by
      rw [← ht1]
      exact subset_span hy
    rcases mem_map.1 this with ⟨x, hx1, hx2⟩
    exact ⟨x, hx1, hx2⟩
  have : ∃ g : P → M, ∀ y ∈ t1, g y ∈ s ∧ f (g y) = y := by
    choose g hg1 hg2 using this
    exists fun y => if H : y ∈ t1 then g y H else 0
    intro y H
    constructor
    · simp only [dif_pos H]
      apply hg1
    · simp only [dif_pos H]
      apply hg2
  obtain ⟨g, hg⟩ := this
  clear this
  exists t1.image g ∪ t2
  rw [Finset.coe_union, span_union, Finset.coe_image]
  apply le_antisymm
  · refine sup_le (span_le.2 <| image_subset_iff.2 ?_) (span_le.2 ?_)
    · intro y hy
      exact (hg y hy).1
    · intro x hx
      have : x ∈ span R t2 := subset_span hx
      rw [ht2] at this
      exact this.1
  intro x hx
  have : f x ∈ s.map f := by
    rw [mem_map]
    exact ⟨x, hx, rfl⟩
  rw [← ht1, ← Set.image_id (t1 : Set P), Finsupp.mem_span_image_iff_linearCombination] at this
  rcases this with ⟨l, hl1, hl2⟩
  refine
    mem_sup.2
      ⟨(linearCombination R id).toFun ((lmapDomain R R g : (P →₀ R) → M →₀ R) l), ?_,
        x - linearCombination R id ((lmapDomain R R g : (P →₀ R) → M →₀ R) l), ?_,
        add_sub_cancel _ _⟩
  · rw [← Set.image_id (g '' ↑t1), Finsupp.mem_span_image_iff_linearCombination]
    refine ⟨_, ?_, rfl⟩
    have : Inhabited P := ⟨0⟩
    rw [← Finsupp.lmapDomain_supported _ _ g, mem_map]
    refine ⟨l, hl1, ?_⟩
    rfl
  rw [ht2, mem_inf]
  constructor
  · apply s.sub_mem hx
    rw [Finsupp.linearCombination_apply, Finsupp.lmapDomain_apply, Finsupp.sum_mapDomain_index]
    · refine s.sum_mem ?_
      intro y hy
      exact s.smul_mem _ (hg y (hl1 hy)).1
    · exact zero_smul _
    · exact fun _ _ _ => add_smul _ _ _
  · rw [LinearMap.mem_ker, f.map_sub, ← hl2]
    rw [Finsupp.linearCombination_apply, Finsupp.linearCombination_apply, Finsupp.lmapDomain_apply]
    rw [Finsupp.sum_mapDomain_index, Finsupp.sum, Finsupp.sum, map_sum]
    · rw [sub_eq_zero]
      refine Finset.sum_congr rfl fun y hy => ?_
      unfold id
      rw [f.map_smul, (hg y (hl1 hy)).2]
    · exact zero_smul _
    · exact fun _ _ _ => add_smul _ _ _

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

Goal state before:
pp: M : Type u_2
N : Type u_4
P : Type u_6
f : M → N
g : N → P
inst✝ : One P
hg : 1 ∈ Set.range g
⊢ MulExact f g ↔ MulExact Subtype.val (Set.rangeFactorization g)

Tactic:
by
  let : One (Set.range g) := ⟨⟨1, hg⟩⟩
  have : ((1 : Set.range g) : P) = 1 := rfl
  simp [MulExact, Subtype.ext_iff, this]

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

Goal state before:
pp: s : Set ℕ∞
⊢ sInf s = 0 ↔ 0 ∈ s

Tactic:
← Order.lt_one_iff,

Goal state after:
s : Set ℕ∞
⊢ sInf s < 1 ↔ 0 ∈ s
Module: Mathlib.Data.ENat.Lattice

Goal state before:
pp: ι : Sort u_2
a : ℕ∞
f : ι → ℕ∞
hne : a ≠ 0
hι : Nonempty ι
d : ℕ
h : ∀ (i : ι), a * f i ≤ ↑d
⊢ ⨆ i, f i ≠ ⊤

Tactic:
intro htop

Goal state after:
ι : Sort u_2
a : ℕ∞
f : ι → ℕ∞
hne : a ≠ 0
hι : Nonempty ι
d : ℕ
h : ∀ (i : ι), a * f i ≤ ↑d
htop : ⨆ i, f i = ⊤
⊢ False
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 : Submodule R E
f : E →ₗ[R] ↥p
hf : ∀ (x : ↥p), f ↑x = x
x : E
⊢ x ∈ p ⊔ f.ker

Tactic:
simp only [(isCompl_of_proj hf).sup_eq_top, mem_top]

Goal state after:
Module: Mathlib.Data.Rel

Goal state before:
pp: case pos
α : Type u_1
β : Type u_2
γ : Type u_3
s : Set α
t₁ t₂ : Set β
u : Set γ
inst✝ : Decidable (Disjoint t₁ t₂)
hst : Disjoint t₁ t₂
⊢ s ×ˢ t₁ ○ t₂ ×ˢ u = ∅

pp: case neg
α : Type u_1
β : Type u_2
γ : Type u_3
s : Set α
t₁ t₂ : Set β
u : Set γ
inst✝ : Decidable (Disjoint t₁ t₂)
hst : ¬Disjoint t₁ t₂
⊢ s ×ˢ t₁ ○ t₂ ×ˢ u = s ×ˢ u

Tactic:
· exact prod_comp_prod_of_disjoint hst ..

Goal state after:
case neg
α : Type u_1
β : Type u_2
γ : Type u_3
s : Set α
t₁ t₂ : Set β
u : Set γ
inst✝ : Decidable (Disjoint t₁ t₂)
hst : ¬Disjoint t₁ t₂
⊢ s ×ˢ t₁ ○ t₂ ×ˢ u = s ×ˢ u
Module: Mathlib.Algebra.Exact.Basic

Goal state before:
pp: case refine_2.left
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✝
R : Type ?u.42
M : Type ?u.44
N : Type ?u.46
P : Type ?u.48
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
hg : Surjective ⇑g
l : { l // l ∘ₗ f = LinearMap.id }
h₁ : ∀ (x : M), ↑l (f x) = x
h₂ : ∀ (x : M), g (f x) = 0
⊢ f = ↑(LinearEquiv.ofBijective ((↑l).prod g) ⋯).symm ∘ₗ inl R M P

Tactic:
rw [LinearEquiv.eq_toLinearMap_symm_comp]
      ext <;> simp [h₁, h₂]

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

Goal state before:
pp: case refine_3
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✝
R : Type ?u.42
M : Type ?u.44
N : Type ?u.46
P : Type ?u.48
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
hg : Surjective ⇑g
e : { e // f = ↑e.symm ∘ₗ inl R M P ∧ g = snd R M P ∘ₗ ↑e }
⊢ (fst R M P ∘ₗ ↑↑e) ∘ₗ f = LinearMap.id

Tactic:
rw [LinearMap.comp_assoc, (LinearEquiv.eq_toLinearMap_symm_comp _ _).mp e.2.1]

Goal state after:
case refine_3
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✝
R : Type ?u.42
M : Type ?u.44
N : Type ?u.46
P : Type ?u.48
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
hg : Surjective ⇑g
e : { e // f = ↑e.symm ∘ₗ inl R M P ∧ g = snd R M P ∘ₗ ↑e }
⊢ fst R M P ∘ₗ inl R M P = LinearMap.id
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 : Function.Exact ⇑f ⇑g
⊢ Function.Injective ⇑(f.range.liftQ g ⋯)

Tactic:
by
  simpa only [← LinearMap.ker_eq_bot, ker_eq_bot_range_liftQ_iff, exact_iff] using h

Goal state after:
Module: Mathlib.Order.KrullDimension

Goal state before:
pp: case mp
α : Type u_1
inst✝ : Preorder α
⊢ (∃ i, 1 < ↑i.length) → ∃ x, (∃ b, b < x) ∧ ∃ b, x < b

Tactic:
rintro ⟨⟨_ | _ | n, l, hl⟩, hl'⟩

Goal state after:
case mp.zero
α : Type u_1
inst✝ : Preorder α
l : Fin (0 + 1) → α
hl : ∀ (i : Fin 0), (l i.castSucc, l i.succ) ∈ {(a, b) | a < b}
hl' : 1 < ↑{ length := 0, toFun := l, step := hl }.length
⊢ ∃ x, (∃ b, b < x) ∧ ∃ b, x < b

case mp.succ.zero
α : Type u_1
inst✝ : Preorder α
l : Fin (0 + 1 + 1) → α
hl : ∀ (i : Fin (0 + 1)), (l i.castSucc, l i.succ) ∈ {(a, b) | a < b}
hl' : 1 < ↑{ length := 0 + 1, toFun := l, step := hl }.length
⊢ ∃ x, (∃ b, b < x) ∧ ∃ b, x < b

case mp.succ.succ
α : Type u_1
inst✝ : Preorder α
n : ℕ
l : Fin (n + 1 + 1 + 1) → α
hl : ∀ (i : Fin (n + 1 + 1)), (l i.castSucc, l i.succ) ∈ {(a, b) | a < b}
hl' : 1 < ↑{ length := n + 1 + 1, toFun := l, step := hl }.length
⊢ ∃ x, (∃ b, b < x) ∧ ∃ b, x < b
Module: Mathlib.Algebra.Algebra.Bilinear

Goal state before:
pp: R : Type u_1
A : Type u_2
inst✝⁴ : CommSemiring R
inst✝³ : NonUnitalNonAssocCommSemiring A
inst✝² : Module R A
inst✝¹ : SMulCommClass R A A
inst✝ : IsScalarTower R A A
⊢ mul' R A ∘ₗ ↑(TensorProduct.comm R A A) = mul' R A

Tactic:
by
  simp [mul', lift_comp_comm_eq]

Goal state after:
Module: Mathlib.Order.KrullDimension

Goal state before:
pp: case ha
α : Type u_1
β : Type u_2
inst✝¹ : Preorder α
inst✝ : PartialOrder β
m : ℕ
f : α →o β
h : ∀ (x : β), krullDim ↑(⇑f ⁻¹' {x}) ≤ ↑m
x : α
⊢ 0 ≤ ↑m + 1

pp: case hbc
α : Type u_1
β : Type u_2
inst✝¹ : Preorder α
inst✝ : PartialOrder β
m : ℕ
f : α →o β
h : ∀ (x : β), krullDim ↑(⇑f ⁻¹' {x}) ≤ ↑m
x : α
⊢ ↑(height (f x)) ≤ ⨆ a, ↑(height a)

Tactic:
exacts [right_eq_inf.mp rfl, le_iSup_iff.mpr fun b a ↦ a (f x)]

Goal state after:
Module: Mathlib.Algebra.Ring.NonZeroDivisors

Goal state before:
pp: R : Type u_1
inst✝¹ : Monoid R
r : R
inst✝ : IsMulTorsionFree R
hx : IsLeftRegular r
hx' : r ≠ 1
n✝ m : ℕ
hnm : (fun n ↦ r ^ n) n✝ = (fun n ↦ r ^ n) m
n l : ℕ
h₁ : n ≤ n + l
h₂ : l = 0
⊢ n = n + 0

Tactic:
Nat.add_zero

Goal state after:
R : Type u_1
inst✝¹ : Monoid R
r : R
inst✝ : IsMulTorsionFree R
hx : IsLeftRegular r
hx' : r ≠ 1
n✝ m : ℕ
hnm : (fun n ↦ r ^ n) n✝ = (fun n ↦ r ^ n) m
n l : ℕ
h₁ : n ≤ n + l
h₂ : l = 0
⊢ n = n