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

Goal state before:
pp: α : Type u_1
β : Type u_2
a : α
b₁ b₂ : β
inst✝⁷ : Ring α
inst✝⁶ : PartialOrder α
inst✝⁵ : IsOrderedRing α
inst✝⁴ : AddCommGroup β
inst✝³ : PartialOrder β
inst✝² : IsOrderedAddMonoid β
inst✝¹ : Module α β
inst✝ : PosSMulStrictMono α β
hb : b₁ < b₂
ha : a < 0
⊢ -a • b₁ < -a • b₂

Tactic:
exact smul_lt_smul_of_pos_left hb (neg_pos_of_neg ha)

Goal state after:
Module: Mathlib.Order.IsNormal

Goal state before:
pp: case mpr.isMin
α : Type u_1
β : Type u_2
f : α → β
inst✝⁴ : LinearOrder α
inst✝³ : WellFoundedLT α
inst✝² : SuccOrder α
inst✝¹ : LinearOrder β
inst✝ : OrderBot α
g : α → β
hf : IsNormal f
hg : IsNormal g
H₁ : f ⊥ = g ⊥
H₂ : ∀ (a : α), f a = g a → f (succ a) = g (succ a)
a : α
ha : IsMin a
⊢ f a = g a

Tactic:
| isMin a ha =>

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

Goal state before:
pp: α : Type u_1
⊢ Ordinal.univ.{u_2, u_2 + 1} ≤ (cof Ordinal.{u_2}).ord

Tactic:
← ord_univ,

Goal state after:
α : Type u_1
⊢ Cardinal.univ.{u_2, u_2 + 1}.ord ≤ (cof Ordinal.{u_2}).ord
Module: Mathlib.SetTheory.Cardinal.Cofinality.Enum

Goal state before:
pp: α : Type u_1
inst✝² : LinearOrder α
inst✝¹ : WellFoundedLT α
inst✝ : IsRegularCardinalOrder α
s : Set α
hs : IsCofinal s
a o : α
ho : o ∈ s
H : ∀ b < a, ↑((enum s hs) b) < o
⊢ a ≤ (enum s hs).symm ⟨o, ho⟩

Tactic:
apply le_of_forall_lt

Goal state after:
α : Type u_1
inst✝² : LinearOrder α
inst✝¹ : WellFoundedLT α
inst✝ : IsRegularCardinalOrder α
s : Set α
hs : IsCofinal s
a o : α
ho : o ∈ s
H : ∀ b < a, ↑((enum s hs) b) < o
⊢ ∀ c < a, c < (enum s hs).symm ⟨o, ho⟩
Module: Mathlib.SetTheory.Ordinal.Family

Goal state before:
pp: β : Type u_2
f : β → Ordinal.{u}
⊢ BddAbove ((fun x ↦ x + 1) '' range f) ↔ BddAbove (range f)

Tactic:
bddAbove_add_one_image_iff

Goal state after:
β : Type u_2
f : β → Ordinal.{u}
⊢ BddAbove (range f) ↔ BddAbove (range f)
Module: Mathlib.SetTheory.Ordinal.Family

Goal state before:
pp: case neg
s : Set Ordinal.{u_3}
hs : ¬BddAbove s
⊢ ¬BddAbove ((fun x ↦ x + 1) '' s)

Tactic:
bddAbove_add_one_image_iff

Goal state after:
case neg
s : Set Ordinal.{u_3}
hs : ¬BddAbove s
⊢ ¬BddAbove s
Module: Mathlib.SetTheory.Ordinal.Arithmetic

Goal state before:
pp: a b c : Ordinal.{u_4}
hc : c ≠ 0
⊢ a / b = c ↔ b * c ≤ a ∧ a < b * (c + 1)

Tactic:
rcases eq_or_ne b 0 with (rfl | hb)
  · simp [hc.symm]
  exact div_eq_iff hb

Goal state after:
Module: Mathlib.Data.Nat.Log

Goal state before:
pp: b n : ℕ
hb : 1 < b
hn : n ≠ 0
⊢ log b n < log b (n + 1) ↔ b ^ log b (n + 1) = n + 1

Tactic:
refine ⟨fun H ↦ ?_, fun H ↦ ?_⟩

Goal state after:
case refine_1
b n : ℕ
hb : 1 < b
hn : n ≠ 0
H : log b n < log b (n + 1)
⊢ b ^ log b (n + 1) = n + 1

case refine_2
b n : ℕ
hb : 1 < b
hn : n ≠ 0
H : b ^ log b (n + 1) = n + 1
⊢ log b n < log b (n + 1)
Module: Mathlib.Data.Nat.Log

Goal state before:
pp: b x y : ℕ
h : x ≤ b ^ y
⊢ clog b x ≤ y

Tactic:
by
  rcases Nat.lt_or_ge 1 b with hb | hb
  · rwa [clog_le_iff_le_pow hb]
  · grind [clog_of_left_le_one]

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

Goal state before:
pp: b x c : Ordinal.{u_1}
hb : 1 < b
hc : c ≠ 0
⊢ b ^ c ≤ x ↔ c ≤ log b x

Tactic:
obtain rfl | hx := eq_or_ne x 0
  · simpa [hc] using hb.ne_bot
  · exact opow_le_iff_le_log hb hx

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

Goal state before:
pp: ι : Type u_1
f : ι → Ordinal.{u} → Ordinal.{u}
inst✝ : Small.{u, u_1} ι
i : ι
H : IsNormal (f i)
a : Ordinal.{u}
⊢ f i (nfpFamily f a) = nfpFamily f a

Tactic:
rw [nfpFamily, H.map_iSup bddAbove_of_small]
  apply le_antisymm <;> refine Ordinal.iSup_le fun l => ?_
  · exact Ordinal.le_iSup _ (i::l)
  · exact H.strictMono.le_apply.trans (Ordinal.le_iSup _ _)

Goal state after:
Module: Mathlib.Data.Nat.Log

Goal state before:
pp: b n : ℕ
hb : 1 < b
⊢ clog b n < clog b (n + 1) ↔ b ^ clog b n = n

Tactic:
refine ⟨fun H ↦ ?_, fun H ↦ ?_⟩

Goal state after:
case refine_1
b n : ℕ
hb : 1 < b
H : clog b n < clog b (n + 1)
⊢ b ^ clog b n = n

case refine_2
b n : ℕ
hb : 1 < b
H : b ^ clog b n = n
⊢ clog b n < clog b (n + 1)
Module: Mathlib.SetTheory.Ordinal.Exponential

Goal state before:
pp: b : Ordinal.{u_1}
hb : 1 < b
x : Ordinal.{u_1}
⊢ x < b ^ succ (log b x)

Tactic:
obtain rfl | hx := eq_or_ne x 0
  · simpa using hb.pos
  · rw [lt_opow_iff_log_lt hb hx, lt_succ_iff]

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

Goal state before:
pp: case succ
a o : Ordinal.{u}
ho : IsPrincipal (fun x1 x2 ↦ x1 + x2) o
ha : a < o
n : ℕ
h : a * ↑n < o
⊢ a * ↑(n + 1) < o

Tactic:
| succ n h =>

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

Goal state before:
pp: c : Cardinal.{u_1}
hc : c ∈ Ici ℵ₀
⊢ preAleph (ω + (preAleph.symm c - ω)) = c

Tactic:
Ordinal.add_sub_cancel_of_le,

Goal state after:
c : Cardinal.{u_1}
hc : c ∈ Ici ℵ₀
⊢ preAleph (preAleph.symm c) = c

c : Cardinal.{u_1}
hc : c ∈ Ici ℵ₀
⊢ ω ≤ preAleph.symm c
Module: Mathlib.SetTheory.Cardinal.Cofinality.Ordinal

Goal state before:
pp: o : Ordinal.{u_1}
⊢ 1 < o.cof ↔ IsSuccLimit o

Tactic:
one_lt_cof_iff

Goal state after:
o : Ordinal.{u_1}
⊢ IsSuccLimit o ↔ IsSuccLimit o
Module: Mathlib.SetTheory.Cardinal.Cofinality.Ordinal

Goal state before:
pp: o : Ordinal.{u_1}
ho : IsSuccLimit o
ho' : o < ω_ 1
⊢ 1 < o.cof

Tactic:
one_lt_cof_iff

Goal state after:
o : Ordinal.{u_1}
ho : IsSuccLimit o
ho' : o < ω_ 1
⊢ IsSuccLimit o
Module: Mathlib.SetTheory.Cardinal.Aleph

Goal state before:
pp: a b : Ordinal.{u_1}
h : a < b
⊢ preBeth a < ⨆ a, 2 ^ preBeth ↑a

Tactic:
lt_ciSup_iff' bddAbove_of_small

Goal state after:
a b : Ordinal.{u_1}
h : a < b
⊢ ∃ i, preBeth a < 2 ^ preBeth ↑i
Module: Mathlib.SetTheory.Cardinal.Aleph

Goal state before:
pp: case a
⊢ preBeth ω ≤ ℵ₀

pp: case a
⊢ ℵ₀ ≤ preBeth ω

Tactic:
· rw [preBeth_limit isSuccLimit_omega0.isSuccPrelimit, ciSup_le_iff' bddAbove_of_small]
    rintro ⟨a, ha⟩
    obtain ⟨n, rfl⟩ := lt_omega0.1 ha
    rw [preBeth_nat]
    exact natCast_le_aleph0

Goal state after:
case a
⊢ ℵ₀ ≤ preBeth ω
Module: Mathlib.SetTheory.Cardinal.Aleph

Goal state before:
pp: o : Ordinal.{u_1}
⊢ ℶ_ (o + 1) = 2 ^ ℶ_ o

Tactic:
by
  simp [beth, ← add_assoc]

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

Goal state before:
pp: case a
a o : Ordinal.{u_1}
f : ↑(Iio a) → ↑(Iio o)
hf : IsFundamentalSeq f
⊢ ⨆ i, ↑(f i) + 1 ≤ o

Tactic:
simp_rw [Ordinal.iSup_le_iff, add_one_le_iff]

Goal state after:
case a
a o : Ordinal.{u_1}
f : ↑(Iio a) → ↑(Iio o)
hf : IsFundamentalSeq f
⊢ ∀ (i : ↑(Iio a)), ↑(f i) < o
Module: Mathlib.SetTheory.Cardinal.Cofinality.Ordinal

Goal state before:
pp: ι : Type u
f : ι → Ordinal.{max u v}
⊢ (lift.{u, max u v} (lsub f)).cof ≤ Cardinal.lift.{v, u} #ι

Tactic:
← Cardinal.lift_umax.{u, v}

Goal state after:
ι : Type u
f : ι → Ordinal.{max u v}
⊢ (lift.{u, max u v} (lsub f)).cof ≤ Cardinal.lift.{max u v, u} #ι
Module: Mathlib.SetTheory.Cardinal.Arithmetic

Goal state before:
pp: n✝ : ℕ
hn : n✝ ≠ 0
n : ℕ
hneq1 : n + 1 + 1 ≠ 0
a : Cardinal.{u_1}
⊢ ∀ ⦃b : Cardinal.{u_1}⦄, a < b → (fun a ↦ ↑(n + 1 + 1) * a) a < (fun a ↦ ↑(n + 1 + 1) * a) b

Tactic:
μ

Goal state after:
n✝ : ℕ
hn : n✝ ≠ 0
n : ℕ
hneq1 : n + 1 + 1 ≠ 0
a μ : Cardinal.{u_1}
⊢ a < μ → (fun a ↦ ↑(n + 1 + 1) * a) a < (fun a ↦ ↑(n + 1 + 1) * a) μ
Module: Mathlib.SetTheory.Cardinal.Regular

Goal state before:
pp: o : Ordinal.{u_1}
h : IsSuccLimit o
⊢ 1 < o.cof

Tactic:
one_lt_cof_iff

Goal state after:
o : Ordinal.{u_1}
h : IsSuccLimit o
⊢ IsSuccLimit o
Module: Mathlib.SetTheory.Cardinal.Cofinality.Ordinal

Goal state before:
pp: o : Ordinal.{u_1}
ho : IsSuccPrelimit o
⊢ (preOmega o).cof = o.cof

Tactic:
by_cases h : IsMin o

Goal state after:
case pos
o : Ordinal.{u_1}
ho : IsSuccPrelimit o
h : IsMin o
⊢ (preOmega o).cof = o.cof

case neg
o : Ordinal.{u_1}
ho : IsSuccPrelimit o
h : ¬IsMin o
⊢ (preOmega o).cof = o.cof
Module: Mathlib.SetTheory.Cardinal.Arithmetic

Goal state before:
pp: case a
ι : Type u
inst✝ : Infinite ι
c : ι → Cardinal.{v}
h₁ : ∀ (i : ι), 2 ≤ c i
h₂ : ∀ (i : ι), lift.{u, v} (c i) ≤ lift.{v, u} #ι
i : ι
⊢ 2 ≤ c i

Tactic:
exact h₁ i

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

Goal state before:
pp: case a
c : Cardinal.{u_1}
h : ℵ₀ ≤ c
⊢ c ≤ c ^< ℵ₀

Tactic:
convert! le_powerlt c one_lt_aleph0

Goal state after:
case e'_3
c : Cardinal.{u_1}
h : ℵ₀ ≤ c
⊢ c = c ^ 1
Module: Mathlib.SetTheory.Cardinal.Cofinality.Ordinal

Goal state before:
pp: case a.refine_1
α : Type u_1
h : (#α).IsStrongPrelimit
ha : #α ≠ 0
h' : (#α).IsStrongLimit
r : α → α → Prop
wo : IsWellOrder α r
hr : (#α).ord = type r
this : LinearOrder α := linearOrderOfSTO r
x : α
⊢ 1 < (#α).ord.cof

Tactic:
one_lt_cof_iff

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

Goal state before:
pp: case inr
α : Type u
inst✝ : Nonempty α
h✝ : Infinite α
⊢ #(List α) = max ℵ₀ #α

Tactic:
· rw [mk_list_eq_mk, eq_comm, max_eq_right]
    exact aleph0_le_mk α

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

Goal state before:
pp: ι : Type u
β : ι → Type v
inst✝¹ : DecidableEq ι
inst✝ : (i : ι) → AddZeroClass (β i)
p : (Π₀ (i : ι), β i) → Prop
h0 : p 0
ha : ∀ (i : ι) (b : β i) (f : Π₀ (i : ι), β i), f i = 0 → b ≠ 0 → p f → p (single i b + f)
i : ι
s : Multiset ι
ih : ∀ (f : (i : ι) → β i) (H : ∀ (i : ι), i ∈ s ∨ f i = 0), p { toFun := f, support' := Trunc.mk ⟨s, H⟩ }
f : (i : ι) → β i
H : ∀ (i_1 : ι), i_1 ∈ i ::ₘ s ∨ f i_1 = 0
H2 : ∀ (j : ι), j ∈ s ∨ (if j = i then 0 else f j) = 0
H3 :
  ∀ (aux : ∀ (i_1 : ι), i_1 ∈ i ::ₘ s ∨ (if i_1 = i then 0 else f i_1) = 0),
    { toFun := fun j ↦ if j = i then 0 else f j, support' := Trunc.mk ⟨i ::ₘ s, aux⟩ } =
      { toFun := fun j ↦ if j = i then 0 else f j, support' := Trunc.mk ⟨s, H2⟩ }
⊢ p { toFun := fun j ↦ if j = i then 0 else f j, support' := Trunc.mk ⟨s, H2⟩ }

Tactic:
apply ih

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

Goal state before:
pp: ι : Type u
β : ι → Type v
inst✝¹ : DecidableEq ι
inst✝ : (i : ι) → AddGroup (β i)
s : Finset ι
x y : (i : ↑↑s) → β ↑i
i : ι
⊢ (if H : i ∈ s then (x - y) ⟨i, H⟩ else 0) = (if H : i ∈ s then x ⟨i, H⟩ else 0) - if H : i ∈ s then y ⟨i, H⟩ else 0

Tactic:
split_ifs <;> [rfl; rw [sub_zero]]

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

Goal state before:
pp: ι : Type u
γ : Type w
β : ι → Type v
inst✝² : DecidableEq ι
inst✝¹ : (i : ι) → AddZeroClass (β i)
inst✝ : AddCommMonoid γ
i : ι
φ : β i →+ γ
| sumZeroHom fun i_1 ↦ ↑(Pi.single i φ i_1)

Tactic:
enter [1, i]

Goal state after:
ι : Type u
γ : Type w
β : ι → Type v
inst✝² : DecidableEq ι
inst✝¹ : (i : ι) → AddZeroClass (β i)
inst✝ : AddCommMonoid γ
i✝ : ι
φ : β i✝ →+ γ
i : ι
| ↑(Pi.single i✝ φ i)
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
this : (liftAddHom (singleAddHom β)) f = (AddMonoidHom.id (Π₀ (i : ι), β i)) f
⊢ f.sum single = f

Tactic:
rw [liftAddHom_apply, sumAddHom_apply] at this

Goal state after:
ι : Type u
β : ι → Type v
inst✝² : DecidableEq ι
inst✝¹ : (i : ι) → AddCommMonoid (β i)
inst✝ : (i : ι) → (x : β i) → Decidable (x ≠ 0)
f : Π₀ (i : ι), β i
this : (f.sum fun x ↦ ⇑(singleAddHom β x)) = (AddMonoidHom.id (Π₀ (i : ι), β i)) f
⊢ f.sum single = f
Module: Mathlib.LinearAlgebra.Dual.Defs

Goal state before:
pp: R : Type u_1
M : Type u_2
inst✝² : CommSemiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
Φ : Submodule R (Dual R M)
x : M
⊢ (Dual.eval R M) x ∈ Φ.dualAnnihilator ↔ ∀ φ ∈ Φ, φ x = 0

Tactic:
mem_dualAnnihilator,

Goal state after:
R : Type u_1
M : Type u_2
inst✝² : CommSemiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
Φ : Submodule R (Dual R M)
x : M
⊢ (∀ w ∈ Φ, ((Dual.eval R M) x) w = 0) ↔ ∀ φ ∈ Φ, φ x = 0
Module: Mathlib.LinearAlgebra.LinearIndependent.Lemmas

Goal state before:
pp: R : Type u_2
M : Type u_4
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
x y : M
⊢ LinearIndependent R ![x, y] ↔ ∀ (s t s' t' : R), s • x + t • y = s' • x + t' • y → s = s' ∧ t = t'

Tactic:
by
  simp [Fintype.linearIndependent_iffₛ, Fin.forall_fin_two, ← FinVec.forall_iff]; rfl

Goal state after:
Module: Mathlib.LinearAlgebra.DFinsupp

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

Tactic:
← erase_add_single i m,

Goal state after:
ι : Type u_1
R : Type u_3
N : Type u_6
inst✝³ : DecidableEq ι
inst✝² : Ring R
inst✝¹ : AddCommGroup N
inst✝ : Module R N
p : ι → Submodule R N
h : ∀ (i : ι) (x : ↥(p i)) (v : Π₀ (i : ι), ↥(p i)), ((lsum ℕ) fun i ↦ (p i).subtype) (erase i v) = ↑x → x = 0
m : Π₀ (i : ι), ↥(p i)
i : ι
hm : ((lsum ℕ) fun i ↦ (p i).subtype) (erase i m + single i (m i)) = 0
⊢ ((lsum ℕ) fun i ↦ (p i).subtype) (erase i m) = ↑(-m i)
Module: Mathlib.LinearAlgebra.LinearIndependent.Lemmas

Goal state before:
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) • t = (b * c) • t by
      by_contra ht; exact h (_root_.smul_left_injective S ht ‹_›)
    calc (a * d) • t
        = a • d • t := by rw [mul_smul]
      _ = -(a • b • s) := by rw [eq_neg_iff_add_eq_zero, ← smul_add, add_comm, h₂, smul_zero]
      _ = (b * c) • t := ?_
    · rw [mul_smul, neg_eq_iff_add_eq_zero, smul_comm a b, ← smul_add, h₁, smul_zero]

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

Goal state before:
pp: case right
ι : Type u'
R : Type u_2
M : Type u_4
inst✝² : Ring R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
v : ι → M
I : Set ι
hIlinind : LinearIndepOn R v I
i : ι
hi : i ∉ I
J : Set ι := ⋯
hImaximal : LinearIndepOn R v J → I = J
hJ : J = I ∪ {i}
memJ : ∀ {x : ι}, x ∈ J ↔ x = i ∨ x ∈ I
hiJ : i ∈ J
h : ¬LinearIndepOn R v J
f : ι →₀ R
supp_f : f ∈ Finsupp.supported R R J
sum_f : ∑ i ∈ f.support, f i • v i = 0
f_ne : f ≠ 0
hfi : f i ≠ 0
⊢ f i • v i ∈ span R (v '' I)

Tactic:
have hfi' : i ∈ f.support := Finsupp.mem_support_iff.mpr hfi

Goal state after:
case right
ι : Type u'
R : Type u_2
M : Type u_4
inst✝² : Ring R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
v : ι → M
I : Set ι
hIlinind : LinearIndepOn R v I
i : ι
hi : i ∉ I
J : Set ι := I ∪ {i}
hImaximal : LinearIndepOn R v J → I = J
hJ : J = I ∪ {i}
memJ : ∀ {x : ι}, x ∈ J ↔ x = i ∨ x ∈ I
hiJ : i ∈ J
h : ¬LinearIndepOn R v J
f : ι →₀ R
supp_f : f ∈ Finsupp.supported R R J
sum_f : ∑ i ∈ f.support, f i • v i = 0
f_ne : f ≠ 0
hfi : f i ≠ 0
hfi' : i ∈ f.support
⊢ f i • v i ∈ span R (v '' I)
Module: Mathlib.Algebra.Group.Pointwise.Set.ListOfFn

Goal state before:
pp: case zero
α : Type u_1
inst✝ : Monoid α
n : ℕ
a : α
s : Fin 0 → Set α
⊢ a ∈ 1 ↔ ∃ f, 1 = a

Tactic:
Fin.exists_fin_zero_pi,

Goal state after:
case zero
α : Type u_1
inst✝ : Monoid α
n : ℕ
a : α
s : Fin 0 → Set α
⊢ a ∈ 1 ↔ 1 = a
Module: Mathlib.Data.Finset.NAry

Goal state before:
pp: α : Type u_1
β : Type u_3
γ : Type u_5
inst✝¹ : DecidableEq γ
f : α → β → γ
s : Finset α
t : Finset β
b : β
inst✝ : DecidableEq β
⊢ image2 f (↑s) (insert b ↑t) = (fun a ↦ f a b) '' ↑s ∪ image2 f ↑s ↑t

Tactic:
exact image2_insert_right

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

Goal state before:
pp: R : Type u_1
M : Type u_4
inst✝ : Semiring R
m : M
⊢ single m 0 = 0

Tactic:
by simp [single]

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

Goal state before:
pp: R : Type u_1
M : Type u_4
inst✝¹ : Semiring R
x : R[M]
r : R
m m₁ : M
inst✝ : Mul M
m₂ : M
H : ∀ m' ∈ x.coeff.support, m' * m = m₁ ↔ m' = m₂
⊢ (x * single m r).coeff m₁ = x.coeff.sum fun m' r' ↦ if m' * m = m₁ then r' * r else 0

Tactic:
simp [coeff_mul]

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

Goal state before:
pp: R : Type u_1
M : Type u_4
inst✝¹ : Semiring R
x : R[M]
r : R
m m₁ : M
inst✝ : Mul M
m₂ : M
H : ∀ m' ∈ x.coeff.support, m * m' = m₁ ↔ m' = m₂
⊢ (single m r * x).coeff m₁ = x.coeff.sum fun m' r' ↦ if m * m' = m₁ then r * r' else 0

Tactic:
simp [coeff_mul]

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

Goal state before:
pp: α : Type u_2
inst✝¹ : DecidableEq α
inst✝ : DivisionMonoid α
s t : Finset α
hs : 1 ∈ s
⊢ t⁻¹ ⊆ s * t⁻¹

Tactic:
exact subset_mul_right _ hs

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

Goal state before:
pp: case refine_1
α : Type u_1
R : Type u_5
inst✝ : Semiring R
β : Type u_7
u : α → β
⊢ (lmapDomain R R u).range ≤ span R (Set.range fun x ↦ single (u x) 1)

Tactic:
rintro x ⟨x, rfl⟩
    induction x using induction_linear with
    | single i s =>
        rw [lmapDomain_apply, mapDomain_single, ← Finsupp.smul_single_one]
        exact Submodule.smul_mem _ _ (Submodule.subset_span ⟨i, rfl⟩)
    | zero => simp
    | add f g hf hg =>
        rw [map_add]
        exact Submodule.add_mem _ hf hg

Goal state after:
Module: Mathlib.Order.Sublattice

Goal state before:
pp: α : Type u_2
β : Type u_3
inst✝³ : Lattice α
inst✝² : Lattice β
L : Sublattice α
inst✝¹ : Nonempty α
inst✝ : Nonempty β
M : Sublattice β
⊢ L.prod M = ⊤ ↔ L = ⊤ ∧ M = ⊤

Tactic:
simpa only [← coe_inj] using! Set.prod_eq_univ

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

Goal state before:
pp: R : Type u
a : R
n : ℕ
inst✝ : Semiring R
h : n ≠ 0
⊢ (C a).coeff n = 0

Tactic:
coeff_C,

Goal state after:
R : Type u
a : R
n : ℕ
inst✝ : Semiring R
h : n ≠ 0
⊢ (if n = 0 then a else 0) = 0
Module: Mathlib.Algebra.Group.UniqueProds.Basic

Goal state before:
pp: case pos
G : Type u_1
inst✝¹ : Group G
inst✝ : UniqueProds G
A B : Finset G
hc : A.Nonempty ∧ B.Nonempty ∧ (1 < #A ∨ 1 < #B)
a : G
ha : a ∈ A
b : G
hb : b ∈ B
hu✝ : UniqueMul A B a b
C D : Finset G
hcard : 1 < #C ∨ 1 < #D
hC : 1 ∈ C
hD : 1 ∈ D
x✝ : Mul (Finset G) := Finset.mul
d1 : G
hd1 : d1 ∈ D
c2 : G
hc2 : c2 ∈ C
hc1 : 1 ∈ C
hd2 : 1 ∈ D
hu :
  ∀ ⦃a b : G⦄,
    (∃ y, (∃ a ∈ D, a⁻¹ = y) ∧ ∃ z ∈ C, y * z = a) →
      (∃ y ∈ D, ∃ z, (∃ a ∈ C, a⁻¹ = z) ∧ y * z = b) → a * b = d1⁻¹ * 1 * (1 * c2⁻¹) → a = d1⁻¹ * 1 ∧ b = 1 * c2⁻¹
h21 : c2 ≠ 1 ∨ d1 ≠ 1
⊢ ∃ c ∈ C, ∃ d ∈ D, (c ≠ 1 ∨ d ≠ 1) ∧ UniqueMul C D c d

Tactic:
refine ⟨c2, hc2, d1, hd1, h21, fun c4 d4 hc4 hd4 he => ?_⟩

Goal state after:
case pos
G : Type u_1
inst✝¹ : Group G
inst✝ : UniqueProds G
A B : Finset G
hc : A.Nonempty ∧ B.Nonempty ∧ (1 < #A ∨ 1 < #B)
a : G
ha : a ∈ A
b : G
hb : b ∈ B
hu✝ : UniqueMul A B a b
C D : Finset G
hcard : 1 < #C ∨ 1 < #D
hC : 1 ∈ C
hD : 1 ∈ D
x✝ : Mul (Finset G) := Finset.mul
d1 : G
hd1 : d1 ∈ D
c2 : G
hc2 : c2 ∈ C
hc1 : 1 ∈ C
hd2 : 1 ∈ D
hu :
  ∀ ⦃a b : G⦄,
    (∃ y, (∃ a ∈ D, a⁻¹ = y) ∧ ∃ z ∈ C, y * z = a) →
      (∃ y ∈ D, ∃ z, (∃ a ∈ C, a⁻¹ = z) ∧ y * z = b) → a * b = d1⁻¹ * 1 * (1 * c2⁻¹) → a = d1⁻¹ * 1 ∧ b = 1 * c2⁻¹
h21 : c2 ≠ 1 ∨ d1 ≠ 1
c4 d4 : G
hc4 : c4 ∈ C
hd4 : d4 ∈ D
he : c4 * d4 = c2 * d1
⊢ c4 = c2 ∧ d4 = d1
Module: Mathlib.Data.ENat.Lattice

Goal state before:
pp: ι : Sort u_2
f : ι → ℕ∞
a : ℕ∞
inst✝ : Nonempty ι
x : ι
⊢ a * ⨅ i, f i ≤ a * f x

Tactic:
by grw [iInf_le]

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

Goal state before:
pp: ι : Sort u_2
f : ι → ℕ∞
a : ℕ∞
h₀ : a = 0 → Nonempty ι
hι : IsEmpty ι
this : a ≠ 0
⊢ a * ⨅ i, f i = ⨅ i, a * f i

Tactic:
by simpa [iInf_of_empty, ite_eq_right_iff, mul_top']

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

Goal state before:
pp: case refine_1
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
⊢ Bijective ⇑(f ∘ₗ fst R M P + ↑l ∘ₗ snd R M P)

Tactic:
have h₂ : ∀ x, g (f x) = 0 := congr_fun h.comp_eq_zero

Goal state after:
case refine_1
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
⊢ Bijective ⇑(f ∘ₗ fst R M P + ↑l ∘ₗ snd R M P)
Module: Mathlib.Algebra.Exact.Basic

Goal state before:
pp: case refine_2
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
⊢ f = ↑(LinearEquiv.ofBijective (f ∘ₗ fst R M P + ↑l ∘ₗ snd R M P) ⋯).symm.symm ∘ₗ inl R M P ∧
    g = snd R M P ∘ₗ ↑(LinearEquiv.ofBijective (f ∘ₗ fst R M P + ↑l ∘ₗ snd R M P) ⋯).symm

Tactic:
have h₂ : ∀ x, g (f x) = 0 := congr_fun h.comp_eq_zero

Goal state after:
case refine_2
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
⊢ f = ↑(LinearEquiv.ofBijective (f ∘ₗ fst R M P + ↑l ∘ₗ snd R M P) ⋯).symm.symm ∘ₗ inl R M P ∧
    g = snd R M P ∘ₗ ↑(LinearEquiv.ofBijective (f ∘ₗ fst R M P + ↑l ∘ₗ snd R M P) ⋯).symm
Module: Mathlib.Data.Rel

Goal state before:
pp: α : Type u_1
s₁ s₂ : Set α
R : SetRel α α
inst✝ : R.IsSymm
⊢ s₁ ×ˢ s₂ ⊆ R ↔ s₂ ×ˢ s₁ ⊆ R

Tactic:
← R.inv_eq_self,

Goal state after:
α : Type u_1
s₁ s₂ : Set α
R : SetRel α α
inst✝ : R.IsSymm
⊢ s₁ ×ˢ s₂ ⊆ R.inv ↔ s₂ ×ˢ s₁ ⊆ R.inv
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 // g ∘ₗ l = LinearMap.id } ≃ { e // f = ↑e.symm ∘ₗ inl R M P ∧ g = snd R M P ∘ₗ ↑e }

Tactic:
refine
  { toFun := fun l ↦ ⟨(LinearEquiv.ofBijective (f ∘ₗ fst R M P + l.1 ∘ₗ snd R M P) ?_).symm, ?_⟩
    invFun := fun e ↦ ⟨e.1.symm ∘ₗ inr R M P, ?_⟩
    left_inv := ?_
    right_inv := ?_ }
  · have h₁ : ∀ x, g (l.1 x) = x := LinearMap.congr_fun l.2
    have h₂ : ∀ x, g (f x) = 0 := congr_fun h.comp_eq_zero
    constructor
    · intro x y e
      simp only [add_apply, coe_comp, comp_apply, fst_apply, snd_apply] at e
      suffices x.2 = y.2 from Prod.ext (hf (by rwa [this, add_left_inj] at e)) this
      simpa [h₁, h₂] using DFunLike.congr_arg g e
    · intro x
      obtain ⟨y, hy⟩ := (h (x - l.1 (g x))).mp (by simp [h₁, g.map_sub])
      exact ⟨⟨y, g x⟩, by simp [hy]⟩
  · have h₁ : ∀ x, g (l.1 x) = x := LinearMap.congr_fun l.2
    have h₂ : ∀ x, g (f x) = 0 := congr_fun h.comp_eq_zero
    constructor
    · ext; simp
    · rw [LinearEquiv.eq_comp_toLinearMap_symm]
      ext <;> simp [h₁, h₂]
  · rw [← LinearMap.comp_assoc, (LinearEquiv.eq_comp_toLinearMap_symm _ _).mp e.2.2]; rfl
  · intro; ext; simp
  · rintro ⟨e, rfl, rfl⟩
    ext1
    apply LinearEquiv.symm_bijective.injective
    ext
    apply e.injective
    ext <;> simp

Goal state after: