mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.LinearAlgebra.Finsupp.Pi

Goal state before:
pp: R : Type u_1
M : Type u_2
P : Type u_4
inst✝⁴ : Semiring R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
inst✝¹ : AddCommMonoid P
inst✝ : Module R P
f : P × M →ₗ[R] M
x : ℕ →₀ P
⊢ ∑ c ∈ x.support, ((((inr R P M ∘ₗ f) ^ c) ∘ₗ inl R P M) (x c)).1 = x 0

Tactic:
Finset.sum_eq_single 0 (fun n _ hn ↦ ?_) (by simp)

Goal state after:
R : Type u_1
M : Type u_2
P : Type u_4
inst✝⁴ : Semiring R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
inst✝¹ : AddCommMonoid P
inst✝ : Module R P
f : P × M →ₗ[R] M
x : ℕ →₀ P
⊢ ((((inr R P M ∘ₗ f) ^ 0) ∘ₗ inl R P M) (x 0)).1 = x 0

R : Type u_1
M : Type u_2
P : Type u_4
inst✝⁴ : Semiring R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
inst✝¹ : AddCommMonoid P
inst✝ : Module R P
f : P × M →ₗ[R] M
x : ℕ →₀ P
n : ℕ
x✝ : n ∈ x.support
hn : n ≠ 0
⊢ ((((inr R P M ∘ₗ f) ^ n) ∘ₗ inl R P M) (x n)).1 = 0
Module: Mathlib.Order.Filter.Bases.Basic

Goal state before:
pp: case a
α : Type u_1
B : FilterBasis α
U : Set α
U_in : U ∈ B.filter
V : Set α
V_in : V ∈ B
h : V ⊆ U
⊢ U ∈ generate B.sets

Tactic:
exact GenerateSets.superset (GenerateSets.basic V_in) h

Goal state after:
Module: Mathlib.Order.Filter.Map

Goal state before:
pp: α : Type u_1
β : Type u_2
f : Filter α
m : α → β
⊢ range m ∈ map m f

Tactic:
rw [← image_univ]

Goal state after:
α : Type u_1
β : Type u_2
f : Filter α
m : α → β
⊢ m '' univ ∈ map m f
Module: Mathlib.Order.Filter.Bases.Basic

Goal state before:
pp: α : Type u_1
ι : Sort u_4
l : Filter α
s : ι → Set α
h : l.HasBasis (fun x ↦ True) s
⊢ l = ⨅ i, 𝓟 (s i)

Tactic:
simpa only [iInf_true] using h.eq_biInf

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

Goal state before:
pp: R : Type u_1
α : Type u_2
β : Type u_3
inst✝⁸ : Semiring R
A : Type u_4
inst✝⁷ : Semiring A
inst✝⁶ : Module R A
inst✝⁵ : AddCommMonoid α
inst✝⁴ : AddCommMonoid β
inst✝³ : Module A β
inst✝² : Module R α
inst✝¹ : Module R β
inst✝ : IsScalarTower R A β
e : α ≃ₗ[R] β
this : Module A α := AddEquiv.module A e.toAddEquiv
x : R
y : A
z : α
⊢ { toFun := (↑e).toFun, invFun := e.invFun, left_inv := ⋯, right_inv := ⋯ }.symm
      (x • y • { toFun := (↑e).toFun, invFun := e.invFun, left_inv := ⋯, right_inv := ⋯ } z) =
    x •
      { toFun := (↑e).toFun, invFun := e.invFun, left_inv := ⋯, right_inv := ⋯ }.symm
        (y • { toFun := (↑e).toFun, invFun := e.invFun, left_inv := ⋯, right_inv := ⋯ } z)

Tactic:
apply e.symm.map_smul

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

Goal state before:
pp: case refine_1
α : Type u
inst✝ : Preorder α
h : cof α = 1
s : Set α
hs : IsCofinal s
hs' : ∃ x, s = {x}
⊢ ∃ x, IsTop x

Tactic:
obtain ⟨t, rfl⟩ := hs'

Goal state after:
case refine_1
α : Type u
inst✝ : Preorder α
h : cof α = 1
t : α
hs : IsCofinal {t}
⊢ ∃ x, IsTop x
Module: Mathlib.Algebra.Order.Module.Defs

Goal state before:
pp: case refine_1
α : Type u_1
β : Type u_2
a₁ a₂ : α
b₁ b₂ : β
inst✝⁶ : Zero α
inst✝⁵ : Zero β
inst✝⁴ : SMulWithZero α β
inst✝³ : PartialOrder α
inst✝² : PartialOrder β
inst✝¹ : PosSMulStrictMono α β
inst✝ : SMulPosStrictMono α β
ha✝ : a₁ ≤ a₂
hb : b₁ ≤ b₂
h₂ : 0 < a₂
h₁ : 0 < b₁
h : a₁ • b₁ = a₂ • b₂
ha : a₁ < a₂
⊢ a₁ • b₁ < a₂ • b₂

pp: case refine_2
α : Type u_1
β : Type u_2
a₁ a₂ : α
b₁ b₂ : β
inst✝⁶ : Zero α
inst✝⁵ : Zero β
inst✝⁴ : SMulWithZero α β
inst✝³ : PartialOrder α
inst✝² : PartialOrder β
inst✝¹ : PosSMulStrictMono α β
inst✝ : SMulPosStrictMono α β
ha : a₁ ≤ a₂
hb✝ : b₁ ≤ b₂
h₂ : 0 < a₂
h₁ : 0 < b₁
h : a₁ • b₁ = a₂ • b₂
hb : b₁ < b₂
⊢ a₁ • b₁ < a₂ • b₂

Tactic:
· exact (smul_lt_smul_of_pos_right ha h₁).trans_le (smul_le_smul_of_nonneg_left hb h₂.le)

Goal state after:
case refine_2
α : Type u_1
β : Type u_2
a₁ a₂ : α
b₁ b₂ : β
inst✝⁶ : Zero α
inst✝⁵ : Zero β
inst✝⁴ : SMulWithZero α β
inst✝³ : PartialOrder α
inst✝² : PartialOrder β
inst✝¹ : PosSMulStrictMono α β
inst✝ : SMulPosStrictMono α β
ha : a₁ ≤ a₂
hb✝ : b₁ ≤ b₂
h₂ : 0 < a₂
h₁ : 0 < b₁
h : a₁ • b₁ = a₂ • b₂
hb : b₁ < b₂
⊢ a₁ • b₁ < a₂ • b₂
Module: Mathlib.SetTheory.Cardinal.Cofinality.Basic

Goal state before:
pp: case a
α : Type u
β : Type v
inst✝¹ : LinearOrder α
inst✝ : LinearOrder β
f : α → β
hf : StrictMono f
hf' : IsCofinal (range f)
s : Set α
hs : IsCofinal s
⊢ lift.{u, v} (cof β) ≤ lift.{v, u} #↑s

Tactic:
· exact (lift_le.2 <| cof_le (hs.image hf.monotone hf')).trans mk_image_le_lift

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

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

Tactic:
rw [← sub_nonneg, ← sub_smul]; exact smul_nonneg (sub_nonneg.2 ha) hb

Goal state after:
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 α β
inst✝ : PosSMulReflectLT α β
ha : a < 0
⊢ -a • b₂ < -a • b₁ ↔ b₂ < b₁

Tactic:
exact smul_lt_smul_iff_of_pos_left (neg_pos_of_neg ha)

Goal state after:
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✝¹ : Zero γ
inst✝ : SMulPosReflectLE α γ
hf : ∀ {b₁ b₂ : β}, f b₁ ≤ f b₂ ↔ b₁ ≤ b₂
smul : ∀ (a : α) (b : β), f (a • b) = a • f b
zero : f 0 = 0
b : β
hb : 0 < b
a₁ a₂ : α
h : a₁ • b ≤ a₂ • b
⊢ a₁ ≤ a₂

Tactic:
simp only [← hf, ← lt_iff_lt_of_le_iff_le' hf hf, zero, smul] at *
    exact le_of_smul_le_smul_right h hb

Goal state after:
Module: Mathlib.Order.IsNormal

Goal state before:
pp: α : Type u_1
inst✝¹ : LinearOrder α
inst✝ : WellFoundedLT α
f : α → α
hf : IsNormal f
⊢ DirSupClosed (range f)

Tactic:
by
  intro s hs hs₀ _ a ha
  have hf' : (f ⁻¹' s).Nonempty := by
    obtain ⟨b, hb⟩ := hs₀
    obtain ⟨c, rfl⟩ := hs hb
    exact ⟨c, hb⟩
  have : Nonempty α := ⟨a⟩
  let := WellFoundedLT.toOrderBot α
  let := WellFoundedLT.conditionallyCompleteLinearOrderBot α
  have hfl : IsLUB (f ⁻¹' s) (sSup (f ⁻¹' s)) :=
    isLUB_csSup hf' ⟨a, fun b hb ↦ hf.strictMono.le_apply.trans (ha.1 hb)⟩
  have ha' := hf.map_isLUB hfl hf'
  rw [image_preimage_eq_of_subset hs] at ha'
  obtain rfl := ha.unique ha'
  exact mem_range_self _

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

Goal state before:
pp: case inr
α : Type u_1
inst✝² : LinearOrder α
inst✝¹ : WellFoundedLT α
inst✝ : Subsingleton α
h✝ : Nonempty α
⊢ typeLT α ≤ (cof α).ord

Tactic:
cases nonempty_unique α
      have := BoundedOrder.ofUnique α
      simp

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

Goal state before:
pp: case mpr
s : Set Ordinal.{u}
hs : ¬BddAbove s
a : Ordinal.{u}
t : Set Ordinal.{u} := ⋯
⊢ a ∈ s → a ∈ range (enumOrd s)

Tactic:
intro ha
    refine ⟨sInf t, (enumOrd_le_of_forall_lt ha ?_).antisymm ?_⟩
    · intro b hb
      by_contra! hb'
      exact hb.not_ge (csInf_le' hb')
    · exact csInf_mem (s := t) ⟨a, (enumOrd_strictMono hs).id_le a⟩

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

Goal state before:
pp: case mp.refine_1
α : Type u
inst✝¹ : LinearOrder α
inst✝ : WellFoundedLT α
a : Ordinal.{u}
ha : succ a = typeLT α
⊢ a ∈ Iio (typeLT α)

pp: case mp.refine_2
α : Type u
inst✝¹ : LinearOrder α
inst✝ : WellFoundedLT α
a : Ordinal.{u}
ha : succ a = typeLT α
b : α
⊢ b ≤ (enum fun x1 x2 ↦ x1 < x2) ⟨a, ?mp.refine_1⟩

Tactic:
· rw [mem_Iio, ← ha, lt_succ_iff]

Goal state after:
case mp.refine_2
α : Type u
inst✝¹ : LinearOrder α
inst✝ : WellFoundedLT α
a : Ordinal.{u}
ha : succ a = typeLT α
b : α
⊢ b ≤ (enum fun x1 x2 ↦ x1 < x2) ⟨a, ⋯⟩
Module: Mathlib.SetTheory.Ordinal.Basic

Goal state before:
pp: case mp.refine_2
α : Type u
inst✝¹ : LinearOrder α
inst✝ : WellFoundedLT α
a : Ordinal.{u}
ha : succ a = typeLT α
b : α
⊢ (typein fun x1 x2 ↦ x1 < x2).toRelEmbedding b ≤ a

Tactic:
← lt_succ_iff,

Goal state after:
case mp.refine_2
α : Type u
inst✝¹ : LinearOrder α
inst✝ : WellFoundedLT α
a : Ordinal.{u}
ha : succ a = typeLT α
b : α
⊢ (typein fun x1 x2 ↦ x1 < x2).toRelEmbedding b < succ a
Module: Mathlib.SetTheory.Ordinal.Arithmetic

Goal state before:
pp: a b c : Ordinal.{u_4}
b0 : b ≠ 0
⊢ a / b ≤ c ↔ a < b * succ c

Tactic:
← lt_succ_iff,

Goal state after:
a b c : Ordinal.{u_4}
b0 : b ≠ 0
⊢ a / b < succ c ↔ a < b * succ c
Module: Mathlib.SetTheory.Ordinal.Basic

Goal state before:
pp: o : Ordinal.{u_1}
⊢ ℵ₀ ≤ o.card ↔ ω ≤ o

Tactic:
by
  rw [← ord_le, ord_aleph0]

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

Goal state before:
pp: b n : ℕ
⊢ log b n = 0 ↔ n < b ∨ b ≤ 1

Tactic:
by
  rcases Nat.lt_or_ge 1 b with hb | hb
  · rcases eq_or_ne n 0 with rfl | hn
    · grind [log_of_lt]
    · rw [← Nat.lt_one_iff, log_lt_iff_lt_pow hb hn, Nat.pow_one, or_iff_left (Nat.not_le_of_lt hb)]
  · simp [hb, log_of_left_le_one]

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

Goal state before:
pp: a b : Ordinal.{u_4}
h : a ≤ b
c : Ordinal.{u_4}
⊢ a / c ≤ b / c

Tactic:
obtain rfl | hc := eq_or_ne c 0
  · rw [div_zero, div_zero]
  · rw [← mul_le_iff_le_div hc]
    exact (mul_div_le a c).trans h

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

Goal state before:
pp: case inr.a
a c : Ordinal.{u_4}
hc : c < a
b d : Ordinal.{u_4}
hd : d ≠ 0
H : a * d ≠ 0
⊢ (a * b + c) / (a * d) ≤ b / d

Tactic:
← lt_succ_iff,

Goal state after:
case inr.a
a c : Ordinal.{u_4}
hc : c < a
b d : Ordinal.{u_4}
hd : d ≠ 0
H : a * d ≠ 0
⊢ (a * b + c) / (a * d) < succ (b / d)
Module: Mathlib.SetTheory.Ordinal.Arithmetic

Goal state before:
pp: a b : Ordinal.{u_4}
⊢ a / b = 1 ↔ b ≤ a ∧ a < b * 2

Tactic:
rw [div_eq_iff' one_ne_zero, mul_one, one_add_one_eq_two]

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

Goal state before:
pp: case refine_1
a b : Ordinal.{u_1}
⊢ (a = 0 ∨ a = 1) ∨ b = 0 → a ^ b ≤ 1

Tactic:
rintro ((rfl | rfl) | rfl)

Goal state after:
case refine_1.inl.inl
b : Ordinal.{u_1}
⊢ 0 ^ b ≤ 1

case refine_1.inl.inr
b : Ordinal.{u_1}
⊢ 1 ^ b ≤ 1

case refine_1.inr
a : Ordinal.{u_1}
⊢ a ^ 0 ≤ 1
Module: Mathlib.SetTheory.Ordinal.Exponential

Goal state before:
pp: b u v w : Ordinal.{u_1}
hb : 1 < b
hv : v ≠ 0
hw : w < b ^ u
⊢ log b (b ^ u * v + w) = u + log b v

Tactic:
by
  rw [log_eq_iff hb]
  · constructor
    · grw [opow_add, opow_log_le_self b hv, ← le_self_add]
    · grw [hw, ← mul_add_one, add_assoc, opow_add]
      gcongr
      rw [add_one_le_iff]
      exact lt_opow_succ_log_self hb _
  · exact fun h ↦ mul_ne_zero (opow_ne_zero u (bot_lt_of_lt hb).ne') hv <|
      left_eq_zero_of_add_eq_zero h

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

Goal state before:
pp: case inr.inr
m n : ℕ
hm : 1 < m
hn : ¬n = 0
⊢ m ^ Nat.log m n ≤ n ∧ n < m ^ (Nat.log m n + 1)

Tactic:
← Nat.log_eq_iff (.inr ⟨hm, hn⟩)

Goal state after:
case inr.inr
m n : ℕ
hm : 1 < m
hn : ¬n = 0
⊢ Nat.log m n = Nat.log m n
Module: Mathlib.SetTheory.Cardinal.Aleph

Goal state before:
pp: a b : Ordinal.{u_1}
ha : a.IsInitial
h : a.card ≤ b.card
⊢ a ≤ b

Tactic:
rw [← ha.le_ord_iff_card_le] at h

Goal state after:
a b : Ordinal.{u_1}
ha : a.IsInitial
h : a ≤ b.card.ord
⊢ a ≤ b
Module: Mathlib.SetTheory.Cardinal.Aleph

Goal state before:
pp: n : ℕ
⊢ preAleph.symm ↑n = ↑n

Tactic:
simp [OrderIso.symm_apply_eq]

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

Goal state before:
pp: ⊢ preAleph.symm ℵ₀ = ω

Tactic:
simp [OrderIso.symm_apply_eq]

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

Goal state before:
pp: case a
o : Ordinal.{u}
h : IsPrincipal (fun x1 x2 ↦ x1 * x2) o
a : Ordinal.{u}
ha₀ : 0 < a
hao : a < o
ho : o ≤ 2
⊢ a < 2

Tactic:
exact hao.trans_le ho

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

Goal state before:
pp: case type
α : Type u
inst✝¹ : LinearOrder α
inst✝ : WellFoundedLT α
⊢ Cardinal.lift.{v, u} (Order.cof α) = Order.cof (ULift.{v, u} α)

Tactic:
← Cardinal.lift_id'.{u, v} (Order.cof (ULift _)),

Goal state after:
case type
α : Type u
inst✝¹ : LinearOrder α
inst✝ : WellFoundedLT α
⊢ Cardinal.lift.{v, u} (Order.cof α) = Cardinal.lift.{u, max u v} (Order.cof (ULift.{v, u} α))
Module: Mathlib.SetTheory.Cardinal.Arithmetic

Goal state before:
pp: case inr.inr.inr.inr
a b : Cardinal.{u_1}
ha0 : a ≠ 0
hb0 : b ≠ 0
ha : a < ℵ₀
hb : b < ℵ₀
⊢ a * b ≤ max (max a b) ℵ₀

Tactic:
exact le_max_of_le_right (mul_lt_aleph0 ha hb).le

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

Goal state before:
pp: case inl
a : Ordinal.{u}
a0 : 0 < a
h : a < ω ^ ω ^ 0
⊢ a * ω ^ ω ^ 0 = ω ^ ω ^ 0

pp: case inr
a b : Ordinal.{u}
a0 : 0 < a
h : a < ω ^ ω ^ b
b0 : b ≠ 0
⊢ a * ω ^ ω ^ b = ω ^ ω ^ b

Tactic:
· rw [opow_zero, opow_one] at h ⊢
    exact mul_omega0 a0 h

Goal state after:
case inr
a b : Ordinal.{u}
a0 : 0 < a
h : a < ω ^ ω ^ b
b0 : b ≠ 0
⊢ a * ω ^ ω ^ b = ω ^ ω ^ b
Module: Mathlib.SetTheory.Ordinal.Principal

Goal state before:
pp: a b : Ordinal.{u}
a0 : 0 < a
h : a < ω ^ ω ^ b
b0 : b ≠ 0
| ω ^ ω ^ b

Tactic:
rw [← one_mul (ω ^ _)]

Goal state after:
a b : Ordinal.{u}
a0 : 0 < a
h : a < ω ^ ω ^ b
b0 : b ≠ 0
| 1 * ω ^ ω ^ b
Module: Mathlib.SetTheory.Cardinal.Arithmetic

Goal state before:
pp: c : Cardinal.{u_1}
h : ℵ₀ ≤ c
⊢ c + c ≤ c

Tactic:
simpa [two_mul, mul_eq_self h] using mul_le_mul_left (natCast_le_aleph0 (n := 2).trans h) c

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

Goal state before:
pp: α✝ : Type u_1
inst✝ : Infinite α✝
α : LinearOrder α✝
w✝ : WellFoundedLT α✝
hα : (#α✝).ord = typeLT α✝
x : α✝
⊢ #{ y // ¬x < y } < #α✝

Tactic:
simpa using! mk_Iic_lt _ hα (aleph0_le_mk _)

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

Goal state before:
pp: o : Ordinal.{u}
c : Cardinal.{v}
f : ↑(Iio o) → Ordinal.{v}
hι : Cardinal.lift.{v, u} o.card ≤ Cardinal.lift.{u, v} c
hf : ∀ (i : ↑(Iio o)), (f i).card ≤ c
⊢ Cardinal.lift.{v, u + 1} #↑(Iio o) ≤ Cardinal.lift.{u + 1, max u v} (Cardinal.lift.{u, v} c)

Tactic:
rwa [Cardinal.mk_Iio_ordinal, Cardinal.lift_lift, ← Cardinal.lift_lift.{v, u + 1},
    Cardinal.lift_le]

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

Goal state before:
pp: f : (b : Ordinal.{u_1}) → b < 0 → Ordinal.{u_1}
⊢ 0 ≤ (cof 0).ord

Tactic:
rw [cof_zero, ord_zero]

Goal state after:
Module: Mathlib.LinearAlgebra.Basis.Cardinality

Goal state before:
pp: R : Type u
M : Type v
inst✝³ : Semiring R
inst✝² : AddCommMonoid M
inst✝¹ : Nontrivial R
inst✝ : Module R M
ι : Type w
b : Basis ι R M
κ : Type w'
v : κ → M
ind : LinearIndependent R v
m : ind.Maximal
i : ι
w : ∀ (x : κ), (b.repr (v x)) i = 0
l : κ →₀ R
⊢ (b.repr ((linearCombination R v) l)) i = 0

Tactic:
simp [linearCombination_apply, Finsupp.sum, w]

Goal state after:
Module: Mathlib.LinearAlgebra.Basis.Cardinality

Goal state before:
pp: R : Type u
M : Type v
inst✝³ : Semiring R
inst✝² : AddCommMonoid M
inst✝¹ : Nontrivial R
inst✝ : Module R M
ι : Type w
b : Basis ι R M
κ : Type w'
v : κ → M
ind : LinearIndependent R v
m : ind.Maximal
i : ι
w : ∀ (x : κ), (b.repr (v x)) i = 0
repr_eq_zero : ∀ (l : κ →₀ R), (b.repr ((linearCombination R v) l)) i = 0
v' : Option κ → M := fun o ↦ o.elim (b i) v
r : range v ⊆ range v'
r' : b i ∉ range v
r'' : range v ≠ range v'
l : Option κ →₀ R
⊢ ∀ (l₂ : Option κ →₀ R), (linearCombination R v') l = (linearCombination R v') l₂ → l = l₂

Tactic:
l'

Goal state after:
R : Type u
M : Type v
inst✝³ : Semiring R
inst✝² : AddCommMonoid M
inst✝¹ : Nontrivial R
inst✝ : Module R M
ι : Type w
b : Basis ι R M
κ : Type w'
v : κ → M
ind : LinearIndependent R v
m : ind.Maximal
i : ι
w : ∀ (x : κ), (b.repr (v x)) i = 0
repr_eq_zero : ∀ (l : κ →₀ R), (b.repr ((linearCombination R v) l)) i = 0
v' : Option κ → M := fun o ↦ o.elim (b i) v
r : range v ⊆ range v'
r' : b i ∉ range v
r'' : range v ≠ range v'
l l' : Option κ →₀ R
⊢ (linearCombination R v') l = (linearCombination R v') l' → l = l'
Module: Mathlib.SetTheory.Cardinal.Regular

Goal state before:
pp: ⊢ preAleph.symm univ.{u, v} = Ordinal.univ.{u, v}

Tactic:
simp [OrderIso.symm_apply_eq]

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

Goal state before:
pp: ι : Type u
β : ι → Type v
inst✝¹ : (i : ι) → Zero (β i)
inst✝ : DecidableEq ι
x : Π₀ (i : ι), β i
i j : ι
⊢ ((single i (x i)).piecewise (erase i x) {i}) j = x j

Tactic:
piecewise_apply

Goal state after:
ι : Type u
β : ι → Type v
inst✝¹ : (i : ι) → Zero (β i)
inst✝ : DecidableEq ι
x : Π₀ (i : ι), β i
i j : ι
⊢ (if j ∈ {i} then (single i (x i)) j else (erase i x) j) = x j
Module: Mathlib.Data.Fintype.Quotient

Goal state before:
pp: ι : Type u_1
inst✝ : DecidableEq ι
α : ι → Sort u_2
S : (i : ι) → Setoid (α i)
l✝ : List ι
i : ι
l : List ι
C : ((i_1 : ι) → i_1 ∈ i :: l → Quotient (S i_1)) → Prop
f : ∀ (a : (i_1 : ι) → i_1 ∈ i :: l → α i_1), C fun x1 x2 ↦ ⟦a x1 x2⟧
q : (i_1 : ι) → i_1 ∈ i :: l → Quotient (S i_1)
⊢ C q

Tactic:
rw [← List.Pi.cons_eta q]
    induction List.Pi.head q using Quotient.ind with | _ a
    refine @list_ind _ (fun q ↦ C (List.Pi.cons _ _ ⟦a⟧ q)) ?_ (List.Pi.tail q)
    intro as
    rw [List.Pi.cons_map a as (fun i ↦ Quotient.mk (S i))]
    exact f _

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

Goal state before:
pp: ι : Type u
γ : Type w
β : ι → Type v
β₁ : ι → Type v₁
β₂ : ι → Type v₂
inst✝² : DecidableEq ι
inst✝¹ : (i : ι) → AddZeroClass (β i)
inst✝ : AddCommMonoid γ
φ : (i : ι) → β i →+ γ
⊢ ∀ (x y : Π₀ (i : ι), β i),
    (sumZeroHom fun i ↦ ↑(φ i)).toFun (x + y) =
      (sumZeroHom fun i ↦ ↑(φ i)).toFun x + (sumZeroHom fun i ↦ ↑(φ i)).toFun y

Tactic:
rintro ⟨f, sf, hf⟩ ⟨g, sg, hg⟩
    change (∑ i ∈ _, _) = (∑ i ∈ _, _) + ∑ i ∈ _, _
    simp only [AddMonoidHom.toZeroHom_coe, coe_add, coe_mk', Pi.add_apply, map_add,
      Finset.sum_add_distrib]
    congr 1
    · refine (Finset.sum_subset ?_ ?_).symm
      · intro i
        simp only [Multiset.mem_toFinset, Multiset.mem_add]
        exact Or.inl
      · intro i _ H2
        simp only [Multiset.mem_toFinset] at H2
        rw [(hf i).resolve_left H2, map_zero]
    · refine (Finset.sum_subset ?_ ?_).symm
      · intro i
        simp only [Multiset.mem_toFinset, Multiset.mem_add]
        exact Or.inr
      · intro i _ H2
        simp only [Multiset.mem_toFinset] at H2
        rw [(hg i).resolve_left H2, map_zero]

Goal state after:
Module: Mathlib.LinearAlgebra.DFinsupp

Goal state before:
pp: case pos
ι : Type u_1
β₁ : ι → Type u_8
β₂ : ι → Type u_9
inst✝¹ : (i : ι) → AddCommMonoid (β₁ i)
inst✝ : (i : ι) → AddCommMonoid (β₂ i)
f : (i : ι) → β₁ i →+ β₂ i
x : Π₀ (i : ι), β₂ i
h : ⇑x ∈ AddSubmonoid.pi Set.univ fun i ↦ AddMonoidHom.mrange (f i)
g : (i : ι) → β₁ i
hg : ∀ (i : ι), (f i) (g i) = x i
i : ι
mem : i ∈ x.support
⊢ (f i) ((mk x.support fun x_1 ↦ g ↑x_1) i) = x i

Tactic:
rw [mk_of_mem mem, hg]

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
S' : Type u_15
inst✝¹² : Semiring R'
inst✝¹¹ : Semiring S'
inst✝¹⁰ : Module R' M
inst✝⁹ : Module S' N
inst✝⁸ : Module R' Pₗ
inst✝⁷ : Module S' Pₗ
inst✝⁶ : SMulCommClass S' R' Pₗ
inst✝⁵ : SMul S' S
inst✝⁴ : IsScalarTower S' S N
inst✝³ : IsScalarTower S' S Pₗ
inst✝² : SMul R' R
inst✝¹ : IsScalarTower R' R M
inst✝ : IsScalarTower R' R Pₗ
B : M →ₗ[R] N →ₗ[S] Pₗ
r' : R'
m : M
x✝ : N
⊢ (B ((r' • 1) • m)) x✝ = r' • (B m) x✝

Tactic:
map_smul₂,

Goal state after:
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
S' : Type u_15
inst✝¹² : Semiring R'
inst✝¹¹ : Semiring S'
inst✝¹⁰ : Module R' M
inst✝⁹ : Module S' N
inst✝⁸ : Module R' Pₗ
inst✝⁷ : Module S' Pₗ
inst✝⁶ : SMulCommClass S' R' Pₗ
inst✝⁵ : SMul S' S
inst✝⁴ : IsScalarTower S' S N
inst✝³ : IsScalarTower S' S Pₗ
inst✝² : SMul R' R
inst✝¹ : IsScalarTower R' R M
inst✝ : IsScalarTower R' R Pₗ
B : M →ₗ[R] N →ₗ[S] Pₗ
r' : R'
m : M
x✝ : N
⊢ (r' • 1) • (B m) x✝ = r' • (B m) x✝
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
this : ∀ (x y : M), LinearIndependent R ![x, x + y] → LinearIndependent R ![x, y]
h : LinearIndependent R ![x, y]
⊢ LinearIndependent R ![x, x + y]

Tactic:
simpa using this (-x) (x + y) (by simpa)

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
N : Type u_6
inst✝¹ : AddCommGroup N
inst✝ : Module R N
f : M →ₗ[R] N
ι : Type u_7
v : ι → M
hv : span R (Set.range v) = ⊤
hli : LinearIndependent R (⇑f ∘ v)
hsp : span R (Set.range (⇑f ∘ v)) = ⊤
⊢ Bijective ⇑f

Tactic:
refine ⟨LinearMap.injective_of_linearIndependent hv hli, ?_⟩
  rw [Set.range_comp, ← Submodule.map_span, hv, Submodule.map_top] at hsp
  rwa [← range_eq_top]

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

Goal state before:
pp: α : Type u_1
β : Type u_3
γ : Type u_5
inst✝¹ : DecidableEq γ
f : α → β → γ
s : Finset α
t t' : Finset β
inst✝ : DecidableEq β
⊢ ↑(image₂ f s (t ∩ t')) ⊆ ↑(image₂ f s t ∩ image₂ f s t')

Tactic:
push_cast
    exact image2_inter_subset_right

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

Goal state before:
pp: α : Type u_5
inst✝ : Group α
s : Finset α
⊢ (∃ a, s = {a} ∧ IsUnit a) ↔ ∃ a, s = {a}

Tactic:
by
  simp only [Group.isUnit, and_true]

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

Goal state before:
pp: α : Type u_2
inst✝¹ : DecidableEq α
inst✝ : CancelMonoid α
s : Finset α
n : ℕ
hn : n ≠ 0
⊢ #s ≤ #(s ^ n)

Tactic:
simpa using card_pow_mono (s := s) one_ne_zero (Nat.one_le_iff_ne_zero.2 hn)

Goal state after: