mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Algebra.Order.Module.Defs

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝⁸ : Semiring α
inst✝⁷ : PartialOrder α
inst✝⁶ : IsStrictOrderedRing α
inst✝⁵ : ExistsAddOfLE α
inst✝⁴ : AddCommMonoid β
inst✝³ : PartialOrder β
inst✝² : IsOrderedCancelAddMonoid β
inst✝¹ : Module α β
inst✝ : PosSMulMono α β
a₁ a₂ : α
b₁ b₂ : β
ha : a₁ ≤ a₂
hb : b₁ ≤ b₂
⊢ a₁ • b₂ + a₂ • b₁ ≤ a₁ • b₁ + a₂ • b₂

Tactic:
obtain ⟨a, ha₀, rfl⟩ := exists_nonneg_add_of_le ha

Goal state after:
α : Type u_1
β : Type u_2
inst✝⁸ : Semiring α
inst✝⁷ : PartialOrder α
inst✝⁶ : IsStrictOrderedRing α
inst✝⁵ : ExistsAddOfLE α
inst✝⁴ : AddCommMonoid β
inst✝³ : PartialOrder β
inst✝² : IsOrderedCancelAddMonoid β
inst✝¹ : Module α β
inst✝ : PosSMulMono α β
a₁ : α
b₁ b₂ : β
hb : b₁ ≤ b₂
a : α
ha₀ : 0 ≤ a
ha : a₁ ≤ a₁ + a
⊢ a₁ • b₂ + (a₁ + a) • b₁ ≤ a₁ • b₁ + (a₁ + a) • b₂
Module: Mathlib.Algebra.Order.Module.Defs

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
inst✝⁶ : Preorder α
inst✝⁵ : Preorder β
inst✝⁴ : Preorder γ
inst✝³ : SMul α β
inst✝² : SMul α γ
f : β → γ
inst✝¹ : Zero α
inst✝ : PosSMulReflectLT α γ
hf : ∀ {b₁ b₂ : β}, f b₁ ≤ f b₂ ↔ b₁ ≤ b₂
smul : ∀ (a : α) (b : β), f (a • b) = a • f b
a : α
ha : 0 ≤ a
b₁ b₂ : β
h : a • b₁ < a • b₂
⊢ b₁ < b₂

Tactic:
by
    simp only [← lt_iff_lt_of_le_iff_le' hf hf, smul] at *; exact lt_of_smul_lt_smul_left h ha

Goal state after:
Module: Mathlib.SetTheory.Ordinal.Basic

Goal state before:
pp: a : Ordinal.{u_1}
o₁ o₂ : ↑(Iio (typeLT a.ToType))
⊢ (enum fun x1 x2 ↦ x1 < x2) o₁ ≤ (enum fun x1 x2 ↦ x1 < x2) o₂ ↔ o₁ ≤ o₂

Tactic:
rw [← enum_le_enum, not_lt]

Goal state after:
Module: Mathlib.SetTheory.Ordinal.Family

Goal state before:
pp: α : Type u_3
β : Type u_4
f : α ⊕ β → Ordinal.{u}
inst✝¹ : Small.{u, u_3} α
inst✝ : Small.{u, u_4} β
⊢ (range fun a ↦ f (Sum.inl a)) ⊆ range fun i ↦ f i

Tactic:
rintro i ⟨a, rfl⟩

Goal state after:
α : Type u_3
β : Type u_4
f : α ⊕ β → Ordinal.{u}
inst✝¹ : Small.{u, u_3} α
inst✝ : Small.{u, u_4} β
a : α
⊢ (fun a ↦ f (Sum.inl a)) a ∈ range fun i ↦ f i
Module: Mathlib.SetTheory.Ordinal.Family

Goal state before:
pp: α : Type u_3
β : Type u_4
f : α ⊕ β → Ordinal.{u}
inst✝¹ : Small.{u, u_3} α
inst✝ : Small.{u, u_4} β
⊢ (range fun b ↦ f (Sum.inr b)) ⊆ range fun i ↦ f i

Tactic:
rintro i ⟨a, rfl⟩

Goal state after:
α : Type u_3
β : Type u_4
f : α ⊕ β → Ordinal.{u}
inst✝¹ : Small.{u, u_3} α
inst✝ : Small.{u, u_4} β
a : β
⊢ (fun b ↦ f (Sum.inr b)) a ∈ range fun i ↦ f i
Module: Mathlib.SetTheory.Ordinal.Family

Goal state before:
pp: case neg
s : Set Cardinal.{u_3}
hn : s.Nonempty
hs : ¬BddAbove s
⊢ (sSup s).ord = sSup (ord '' s)

Tactic:
rw [csSup_of_not_bddAbove hs, csSup_of_not_bddAbove (bddAbove_ord_image_iff.not.2 hs)]

Goal state after:
case neg
s : Set Cardinal.{u_3}
hn : s.Nonempty
hs : ¬BddAbove s
⊢ (sSup ∅).ord = sSup ∅
Module: Mathlib.SetTheory.Ordinal.Family

Goal state before:
pp: case neg
β : Type u_3
inst✝¹ : LinearOrder β
inst✝ : NoMaxOrder β
f : β → Ordinal.{u}
hf : StrictMono f
hf' : ¬BddAbove (range f)
⊢ ⨆ i, f i + 1 ≤ ⨆ i, f i

Tactic:
ciSup_of_not_bddAbove hf',

Goal state after:
case neg
β : Type u_3
inst✝¹ : LinearOrder β
inst✝ : NoMaxOrder β
f : β → Ordinal.{u}
hf : StrictMono f
hf' : ¬BddAbove (range f)
⊢ ⨆ i, f i + 1 ≤ sSup ∅
Module: Mathlib.SetTheory.Ordinal.Basic

Goal state before:
pp: x : ToType 1
⊢ (typein fun x1 x2 ↦ x1 < x2).toRelEmbedding x = 0

Tactic:
by
  rw [one_toType_eq x, typein_enum]

Goal state after:
Module: Mathlib.SetTheory.Ordinal.Arithmetic

Goal state before:
pp: a b : Ordinal.{u_4}
hb : IsSuccLimit b
⊢ IsSuccPrelimit (a * b)

Tactic:
obtain rfl | ha := eq_zero_or_pos a

Goal state after:
case inl
b : Ordinal.{u_4}
hb : IsSuccLimit b
⊢ IsSuccPrelimit (0 * b)

case inr
a b : Ordinal.{u_4}
hb : IsSuccLimit b
ha : 0 < a
⊢ IsSuccPrelimit (a * b)
Module: Mathlib.SetTheory.Ordinal.Basic

Goal state before:
pp: o : Ordinal.{0}
ho : o < typeLT ℕ
h : Ordinal.lift.{u, 0} o < ω
⊢ lift.{u, 0} o.card < ℵ₀

Tactic:
lift_lt_aleph0,

Goal state after:
o : Ordinal.{0}
ho : o < typeLT ℕ
h : Ordinal.lift.{u, 0} o < ω
⊢ o.card < ℵ₀
Module: Mathlib.SetTheory.Ordinal.Exponential

Goal state before:
pp: case inr
a : Ordinal.{u_1}
h : a ≠ 0
⊢ a ^ 0 = 1

Tactic:
· rw [opow_of_ne_zero h, limitRecOn_zero]

Goal state after:
Module: Mathlib.SetTheory.Ordinal.Arithmetic

Goal state before:
pp: a : Ordinal.{u_4}
⊢ a % 0 = a

Tactic:
simp [mod_def]

Goal state after:
Module: Mathlib.SetTheory.Ordinal.Arithmetic

Goal state before:
pp: b : Ordinal.{u_4}
⊢ 0 % b = 0

Tactic:
simp [mod_def]

Goal state after:
Module: Mathlib.SetTheory.Ordinal.Arithmetic

Goal state before:
pp: a : Ordinal.{u_4}
⊢ a % 1 = 0

Tactic:
simp [mod_def]

Goal state after:
Module: Mathlib.SetTheory.Ordinal.Exponential

Goal state before:
pp: a b c : Ordinal.{u_1}
⊢ a ^ (b + c) = a ^ b * a ^ c

Tactic:
obtain rfl | ha := eq_zero_or_pos a

Goal state after:
case inl
b c : Ordinal.{u_1}
⊢ 0 ^ (b + c) = 0 ^ b * 0 ^ c

case inr
a b c : Ordinal.{u_1}
ha : 0 < a
⊢ a ^ (b + c) = a ^ b * a ^ c
Module: Mathlib.SetTheory.Ordinal.FixedPoint

Goal state before:
pp: f : Ordinal.{u} → Ordinal.{u}
hf : StrictMono f
a : Ordinal.{u}
h : a < f a
n : ℕ
⊢ f^[n] (f a) ≤ nfp f a

Tactic:
rw [← iterate_succ_apply]

Goal state after:
f : Ordinal.{u} → Ordinal.{u}
hf : StrictMono f
a : Ordinal.{u}
h : a < f a
n : ℕ
⊢ f^[n.succ] a ≤ nfp f a
Module: Mathlib.SetTheory.Cardinal.Aleph

Goal state before:
pp: ⊢ ω.IsInitial

Tactic:
rw [IsInitial, card_omega0, ord_aleph0]

Goal state after:
Module: Mathlib.SetTheory.Cardinal.Aleph

Goal state before:
pp: case isSuccPrelimit.mpr
o : Ordinal.{u_1}
ho : IsSuccPrelimit o
IH : ∀ b < o, lift.{v, u_1} (preBeth b) = preBeth (Ordinal.lift.{v, u_1} b)
i : Ordinal.{max u_1 v}
hi : i ∈ Iio (Ordinal.lift.{v, u_1} o)
⊢ (fun a ↦ preBeth ↑a) ⟨i, hi⟩ ∈ range fun i ↦ lift.{v, u_1} (preBeth ↑i)

Tactic:
obtain ⟨i, rfl⟩ := Ordinal.mem_range_lift_of_le hi.le
      rw [mem_Iio, Ordinal.lift_lt] at hi
      exact ⟨⟨i, hi⟩, IH _ hi⟩

Goal state after:
Module: Mathlib.SetTheory.Cardinal.Aleph

Goal state before:
pp: ⊢ ℶ_ 0 = ℵ₀

Tactic:
by
  simp [beth]

Goal state after:
Module: Mathlib.SetTheory.Cardinal.Arithmetic

Goal state before:
pp: a b c : Cardinal.{u_1}
h : a + b = a + c
ha : a < ℵ₀
hb : b < ℵ₀
hc : ℵ₀ ≤ c
⊢ a + b < ℵ₀

Tactic:
apply add_lt_aleph0 ha hb

Goal state after:
Module: Mathlib.SetTheory.Cardinal.Regular

Goal state before:
pp: case le_cof_ord.refine_2
c : Cardinal.{u_1}
hc : ℵ₀ ≤ c
hc₀ : ℵ₀ ≤ succ c
hc' : (succ c).ord.cof < succ c
f : ↑(Iio (succ c).ord.cof.ord) → ↑(Iio (succ c).ord)
hf : IsFundamentalSeq f
i : ↑(Iio (succ c).ord.cof.ord)
⊢ (↑(f i) + 1).card ≤ c

Tactic:
· rw [card_le_iff]
    exact (isSuccLimit_ord hc₀).add_one_lt (f i).2

Goal state after:
Module: Mathlib.SetTheory.Cardinal.Cofinality.Ordinal

Goal state before:
pp: case a.refine_1
α : Type u_1
h : (#α).IsStrongPrelimit
r : α → α → Prop
inst✝ : IsWellOrder α r
hr : (#α).ord = type r
ha✝ : #α ≠ 0
h' : (#α).IsStrongLimit
ha : ℵ₀ ≤ #α
x : α
⊢ Bounded r {x}

Tactic:
apply bounded_singleton

Goal state after:
case a.refine_1
α : Type u_1
h : (#α).IsStrongPrelimit
r : α → α → Prop
inst✝ : IsWellOrder α r
hr : (#α).ord = type r
ha✝ : #α ≠ 0
h' : (#α).IsStrongLimit
ha : ℵ₀ ≤ #α
x : α
⊢ IsSuccLimit (type r)
Module: Mathlib.SetTheory.Cardinal.Arithmetic

Goal state before:
pp: case h
α : Type u
inst✝ : Infinite α
β : Type u
s : Set α
g : ↑s ↪ β
x : α
h : x ∈ ↑⟨s, ⋯⟩
this : ∃ z, g z = g ⟨x, h⟩
⊢ (if h_1 : ∃ x_1, g x_1 = g ⟨x, h⟩ then Sum.inl ↑(Classical.choose h_1) else Sum.inr { down := 0 }) = Sum.inl x

Tactic:
dif_pos this

Goal state after:
case h
α : Type u
inst✝ : Infinite α
β : Type u
s : Set α
g : ↑s ↪ β
x : α
h : x ∈ ↑⟨s, ⋯⟩
this : ∃ z, g z = g ⟨x, h⟩
⊢ Sum.inl ↑(Classical.choose this) = Sum.inl x
Module: Mathlib.SetTheory.Cardinal.Regular

Goal state before:
pp: ⊢ ℶ_ Ordinal.univ.{u, v} = univ.{u, v}

Tactic:
by
  simpa using IsInaccessible.univ.beth_ord

Goal state after:
Module: Mathlib.Data.Finsupp.ToDFinsupp

Goal state before:
pp: ι : Type u_1
R : Type u_2
M : Type u_3
η : ι → Type u_4
N : Type u_5
inst✝¹ : Semiring R
inst✝ : Zero N
f : Π₀ (i : ι), η i →₀ N
⊢ (i : ι) × η i →₀ N

Tactic:
haveI := Classical.decEq ι
    haveI := fun i => Classical.decEq (η i →₀ N)
    refine
      onFinset (Finset.sigma f.support fun j => (f j).support) (fun ji => f ji.1 ji.2) fun g hg =>
        Finset.mem_sigma.mpr ⟨?_, mem_support_iff.mpr hg⟩
    simp only [Ne, DFinsupp.mem_support_toFun]
    intro h
    dsimp at hg
    rw [h] at hg
    simp only [coe_zero, Pi.zero_apply, not_true] at hg

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

Goal state before:
pp: ι : Type u
β : ι → Type v
inst✝² : DecidableEq ι
inst✝¹ : (i : ι) → AddCommMonoid (β i)
inst✝ : (i : ι) → (x : β i) → Decidable (x ≠ 0)
f : Π₀ (i : ι), β i
⊢ f.sum single = f

Tactic:
have := DFunLike.congr_fun (liftAddHom_singleAddHom (β := β)) f
  rw [liftAddHom_apply, sumAddHom_apply] at this
  exact this

Goal state after:
Module: Mathlib.LinearAlgebra.DFinsupp

Goal state before:
pp: ι : Type u_1
R : Type u_3
M : ι → Type u_5
inst✝³ : Semiring R
inst✝² : (i : ι) → AddCommMonoid (M i)
inst✝¹ : (i : ι) → Module R (M i)
inst✝ : DecidableEq ι
i i' : ι
h : i ≠ i'
⊢ lapply i ∘ₗ lsingle i' = 0

Tactic:
by ext; simp [h.symm]

Goal state after:
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✝¹ : R
x✝ : M
⊢ (lcompₛₗ R₅ P σ₂₃ g) (h (x✝¹ • x✝)) = σ₁₅ x✝¹ • (lcompₛₗ R₅ P σ₂₃ g) (h x✝)

Tactic:
simp [map_smulₛₗ, lcompₛₗ]

Goal state after:
Module: Mathlib.LinearAlgebra.Isomorphisms

Goal state before:
pp: R : Type u_1
M : Type u_2
M₂ : Type u_3
M₃ : Type u_4
inst✝⁶ : Ring R
inst✝⁵ : AddCommGroup M
inst✝⁴ : AddCommGroup M₂
inst✝³ : AddCommGroup M₃
inst✝² : Module R M
inst✝¹ : Module R M₂
inst✝ : Module R M₃
f : M →ₗ[R] M₂
S T : Submodule R M
h✝ h : S ≤ T
⊢ map S.mkQ T ≤ (S.mapQ T LinearMap.id h).ker

Tactic:
rintro _ ⟨x, hx, rfl⟩
      rw [LinearMap.mem_ker, mkQ_apply, mapQ_apply]
      exact (Quotient.mk_eq_zero _).mpr hx

Goal state after:
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
h : a * d ≠ b * c
h' : LinearIndependent R ![a • x + b • y, c • x + d • y]
i : Fin (Nat.succ 0).succ
⊢ ![(a * d - b * c) • x, (a * d - b * c) • y] i =
    ![d • (a • x + b • y) + -b • (c • x + d • y), -c • (a • x + b • y) + a • (c • x + d • y)] i

Tactic:
fin_cases i <;> simp <;> module

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

Goal state before:
pp: case neg
R : Type u_2
M : Type u_4
inst✝² : Ring R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
η : Type u_6
ιs : η → Type u_7
f : (j : η) → ιs j → M
hindep : ∀ (j : η), LinearIndependent R (f j)
hd : ∀ (i : η) (t : Set η), t.Finite → i ∉ t → Disjoint (span R (range (f i))) (⨆ i ∈ t, span R (range (f i)))
a✝ : Nontrivial R
x₁ : η
x₂ : ιs x₁
y₁ : η
y₂ : ιs y₁
hxy : (fun ji ↦ f ji.fst ji.snd) ⟨x₁, x₂⟩ = (fun ji ↦ f ji.fst ji.snd) ⟨y₁, y₂⟩
h_cases : ¬x₁ = y₁
⊢ ⟨x₁, x₂⟩ = ⟨y₁, y₂⟩

Tactic:
· have h0 : f x₁ x₂ = 0 := by
        apply
          disjoint_def.1 (hd x₁ {y₁} (finite_singleton y₁) fun h => h_cases (eq_of_mem_singleton h))
            (f x₁ x₂) (subset_span (mem_range_self _))
        rw [iSup_singleton]
        simp only at hxy
        rw [hxy]
        exact subset_span (mem_range_self y₂)
      exact False.elim ((hindep x₁).ne_zero _ h0)

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

Goal state before:
pp: A : Type u_1
M₀ : Type u_2
inst✝² : AddGroup A
inst✝¹ : MonoidWithZero M₀
inst✝ : Nontrivial M₀
ψ : AddChar A M₀
h : ψ 0 = 0 0
⊢ False

Tactic:
simpa only [h, Pi.zero_apply, zero_ne_one] using map_zero_eq_one ψ

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

Goal state before:
pp: R : Type u_1
S : Type u_2
M : Type u_3
inst✝² : Semiring R
inst✝¹ : Semiring S
inst✝ : MulOneClass M
f : S →+* R
g : M →* R
c : S
φ : S[M]
m✝ : M
x✝ : S
⊢ (((liftNC ↑f ⇑g).comp ((smulAddHom S S[M]) c)).comp (singleAddHom m✝)) x✝ =
    (((AddMonoidHom.mulLeft (f c)).comp (liftNC ↑f ⇑g)).comp (singleAddHom m✝)) x✝

Tactic:
simp [mul_assoc]

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

Goal state before:
pp: R : Type u_1
S : Type u_2
M : Type u_3
inst✝² : Semiring R
inst✝¹ : Semiring S
inst✝ : AddZeroClass M
f : S →+* R
g : Multiplicative M →* R
c : S
φ : S[M]
m✝ : M
x✝ : S
⊢ (((liftNC ↑f ⇑g).comp ((smulAddHom S S[M]) c)).comp (singleAddHom m✝)) x✝ =
    (((AddMonoidHom.mulLeft (f c)).comp (liftNC ↑f ⇑g)).comp (singleAddHom m✝)) x✝

Tactic:
simp [mul_assoc]

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 ⋯
a : ↑t
⊢ v ((fun a ↦ f ⋯) a) ∈ t

Tactic:
simp [hf]

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

Goal state before:
pp: β : Type u_3
γ : Type u_5
inst✝ : DecidableEq γ
f : γ → β → γ
b : β
h : ∀ (a : γ), f a b = a
s : Finset γ
⊢ image₂ f s {b} = s

Tactic:
by rw [image₂_singleton_right, funext h, image_id']

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
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
⊢ b₃ ∈ ↑(span K ↑(insert b₂ s' ∪ t))

Tactic:
by
          have : ↑(s' ∪ insert b₁ t) ⊆ insert b₁ (insert b₂ ↑(s' ∪ t) : Set V) := by
            simp only [insert_eq, union_subset_union, Subset.refl,
              subset_union_right, Finset.union_insert, Finset.coe_insert]
          have hb₃ : b₃ ∈ span K (insert b₁ (insert b₂ ↑(s' ∪ t) : Set V)) :=
            span_mono this (hss' hb₃)
          have : s ⊆ (span K (insert b₁ ↑(s' ∪ t)) : Submodule K V) := by
            simpa [insert_eq, -singleton_union, -union_singleton] using hss'
          have hb₁ : b₁ ∈ span K (insert b₂ ↑(s' ∪ t)) :=
            mem_span_insert_exchange (this hb₂s) hb₂t
          rw [span_insert_eq_span hb₁] at hb₃; simpa using hb₃

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
a : G
aA : a ∈ A
b : G
bB : b ∈ B
ab : f (a * b) = f (a0 * b0)
⊢ f a = f a0 ∧ f b = f b0

Tactic:
hf.eq_iff

Goal state after:
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
a : G
aA : a ∈ A
b : G
bB : b ∈ B
ab : a * b = a0 * b0
⊢ a = a0 ∧ b = b0
Module: Mathlib.LinearAlgebra.Finsupp.Span

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

Tactic:
exact mem_span_of_mem ⟨a, b, rfl⟩

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
inst✝² : SMulZeroClass S R
inst✝¹ : SMulZeroClass Sᵐᵒᵖ R
inst✝ : IsCentralScalar S R
⊢ ∀ (m : S) (a : R[X]), MulOpposite.op m • a = m • a

Tactic:
rintro _ ⟨⟩

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[ℕ]
⊢ MulOpposite.op m✝ • { toFinsupp := toFinsupp✝ } = m✝ • { toFinsupp := toFinsupp✝ }
Module: Mathlib.LinearAlgebra.StdBasis

Goal state before:
pp: ι : Type u_1
R : Type u_2
M : Type u_3
inst✝³ : Finite ι
inst✝² : CommSemiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
v : ι → M
⊢ Surjective ⇑((piEquiv ι R M) v) ↔ span R (Set.range v) = ⊤

Tactic:
by
  rw [← LinearMap.range_eq_top, range_piEquiv]

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

Goal state before:
pp: M : Type u_3
inst✝ : AddCommGroup M
H : AddSubgroup M
n : ℕ
x✝ : ∃ f, f.range = (toIntSubmodule H).toAddSubgroup
f : (Fin n → ℤ) →+ M
hf : f.range = (toIntSubmodule H).toAddSubgroup
⊢ f.toIntLinearMap.range.toAddSubmonoid = (toIntSubmodule H).toAddSubmonoid

Tactic:
simp [hf]

Goal state after:
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
this : x ∈ p ⊔ f.ker
⊢ ↑((p.projectionOnto f.ker ⋯) x) = ↑(f x)

Tactic:
rcases mem_sup'.1 this with ⟨x, y, rfl⟩

Goal state after:
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 : ↥p
y : ↥f.ker
this : ↑x + ↑y ∈ p ⊔ f.ker
⊢ ↑((p.projectionOnto f.ker ⋯) (↑x + ↑y)) = ↑(f (↑x + ↑y))
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 : ↥p
y : ↥f.ker
this : ↑x + ↑y ∈ p ⊔ f.ker
⊢ ↑((p.projectionOnto f.ker ⋯) (↑x + ↑y)) = ↑(f (↑x + ↑y))

Tactic:
simp [hf]

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

Goal state before:
pp: M₁ : Type u_8
M₂ : Type u_9
M₃ : Type u_10
N₁ : Type u_11
N₂ : Type u_12
N₃ : Type u_13
inst✝⁵ : CommMonoid M₁
inst✝⁴ : CommMonoid M₂
inst✝³ : CommMonoid M₃
inst✝² : CommMonoid N₁
inst✝¹ : CommMonoid N₂
inst✝ : CommMonoid N₃
f : M₁ →* M₂
g : M₂ →* M₃
f' : N₁ →* N₂
g' : N₂ →* N₃
τ₁ : M₁ →* N₁
τ₂ : M₂ →* N₂
τ₃ : M₃ →* N₃
comm₁₂ : f'.comp τ₁ = τ₂.comp f
comm₂₃ : g'.comp τ₂ = τ₃.comp g
h₁ : Surjective ⇑τ₁
h₂ : Bijective ⇑τ₂
h₃ : Injective ⇑τ₃
⊢ MulExact ⇑f ⇑g ↔ MulExact ⇑f' ⇑g'

Tactic:
replace comm₁₂ := DFunLike.congr_fun comm₁₂
  replace comm₂₃ := DFunLike.congr_fun comm₂₃
  dsimp at comm₁₂ comm₂₃
  constructor
  · intro h y₂
    obtain ⟨x₂, rfl⟩ := h₂.2 y₂
    constructor
    · intro hx₂
      obtain ⟨x₁, rfl⟩ := (h x₂).1 (h₃ (by simpa only [map_one, comm₂₃] using hx₂))
      exact ⟨τ₁ x₁, by simp only [comm₁₂]⟩
    · rintro ⟨y₁, hy₁⟩
      obtain ⟨x₁, rfl⟩ := h₁ y₁
      rw [comm₂₃, (h x₂).2 _, map_one]
      exact ⟨x₁, h₂.1 (by simpa only [comm₁₂] using hy₁)⟩
  · intro h x₂
    constructor
    · intro hx₂
      obtain ⟨y₁, hy₁⟩ := (h (τ₂ x₂)).1 (by simp only [comm₂₃, hx₂, map_one])
      obtain ⟨x₁, rfl⟩ := h₁ y₁
      exact ⟨x₁, h₂.1 (by simpa only [comm₁₂] using hy₁)⟩
    · rintro ⟨x₁, rfl⟩
      apply h₃
      simp only [← comm₁₂, ← comm₂₃, h.apply_apply_eq_one (τ₁ x₁), map_one]

Goal state after:
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
T : E →ₗ[R] E
hT : IsIdempotentElem T
⊢ T = T.range.projection T.ker ⋯

Tactic:
convert! ofIsCompl_subtype_zero_eq hT.isCompl

Goal state after:
R : Type u_1
inst✝² : Ring R
E : Type u_2
inst✝¹ : AddCommGroup E
inst✝ : Module R E
T : E →ₗ[R] E
hT : IsIdempotentElem T
⊢ T = ofIsCompl ⋯ T.range.subtype 0
Module: Mathlib.Order.RelSeries

Goal state before:
pp: case inl
α : Type u_1
r : SetRel α α
β : Type u_2
s : SetRel β β
p : RelSeries r
i : Fin p.length
a : α
prev_connect : (p.toFun i.castSucc, a) ∈ r
connect_next : (a, p.toFun i.succ) ∈ r
m : Fin (p.length + 1)
x : α := i.succ.castSucc.insertNth a p.toFun m.castSucc
y : α := i.succ.castSucc.insertNth a p.toFun m.succ
hm : ↑m < ↑i
⊢ (x, y) ∈ r

Tactic:
convert! p.step ⟨m, hm.trans i.2⟩

Goal state after:
case e'_3
α : Type u_1
r : SetRel α α
β : Type u_2
s : SetRel β β
p : RelSeries r
i : Fin p.length
a : α
prev_connect : (p.toFun i.castSucc, a) ∈ r
connect_next : (a, p.toFun i.succ) ∈ r
m : Fin (p.length + 1)
x : α := i.succ.castSucc.insertNth a p.toFun m.castSucc
y : α := i.succ.castSucc.insertNth a p.toFun m.succ
hm : ↑m < ↑i
⊢ x = p.toFun ⟨↑m, ⋯⟩.castSucc

case e'_4
α : Type u_1
r : SetRel α α
β : Type u_2
s : SetRel β β
p : RelSeries r
i : Fin p.length
a : α
prev_connect : (p.toFun i.castSucc, a) ∈ r
connect_next : (a, p.toFun i.succ) ∈ r
m : Fin (p.length + 1)
x : α := i.succ.castSucc.insertNth a p.toFun m.castSucc
y : α := i.succ.castSucc.insertNth a p.toFun m.succ
hm : ↑m < ↑i
⊢ y = p.toFun ⟨↑m, ⋯⟩.succ
Module: Mathlib.Order.RelSeries

Goal state before:
pp: case inr.inr
α : Type u_1
r : SetRel α α
β : Type u_2
s : SetRel β β
p : RelSeries r
i : Fin p.length
a : α
prev_connect : (p.toFun i.castSucc, a) ∈ r
connect_next : (a, p.toFun i.succ) ∈ r
m : Fin (p.length + 1)
x : α := i.succ.castSucc.insertNth a p.toFun m.castSucc
y : α := i.succ.castSucc.insertNth a p.toFun m.succ
hm : ↑i < ↑m
⊢ (x, y) ∈ r

Tactic:
rw [Nat.lt_iff_add_one_le, le_iff_lt_or_eq] at hm
      obtain hm | hm := hm
      · convert! p.step ⟨m.1 - 1, Nat.sub_lt_right_of_lt_add (by lia) m.2⟩
        · change Fin.insertNth _ _ _ _ = _
          rw [Fin.insertNth_apply_above (h := hm)]
          aesop
        · change Fin.insertNth _ _ _ _ = _
          rw [Fin.insertNth_apply_above]
          swap
          · exact hm.trans (lt_add_one _)
          simp only [Fin.pred_succ, eq_rec_constant, Fin.succ_mk]
          congr
          exact Fin.ext <| Eq.symm <| Nat.succ_pred_eq_of_pos (lt_trans (Nat.zero_lt_succ _) hm)
      · convert! connect_next
        · change Fin.insertNth _ _ _ _ = _
          rw [show m.castSucc = i.succ.castSucc from Fin.ext hm.symm, Fin.insertNth_apply_same]
        · change Fin.insertNth _ _ _ _ = _
          rw [Fin.insertNth_apply_above]
          swap
          · change i.1 + 1 < m.1 + 1; lia
          simp only [Fin.pred_succ, eq_rec_constant]
          congr; ext; exact hm.symm

Goal state after: