mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Order.Filter.Map

Goal state before:
pp: case refine_1
α : Type u_1
β : Type u_2
F : Filter α
G : Filter β
m : α → β
hm : SurjOn (map m) (Iic F) (Iic G)
⊢ G ≤ map m F

Tactic:
rcases hm self_mem_Iic with ⟨H, (hHF : H ≤ F), rfl⟩

Goal state after:
case refine_1
α : Type u_1
β : Type u_2
F : Filter α
m : α → β
H : Filter α
hHF : H ≤ F
hm : SurjOn (map m) (Iic F) (Iic (map m H))
⊢ map m H ≤ map m F
Module: Mathlib.RingTheory.Noetherian.Defs

Goal state before:
pp: R : Type u_1
M : Type u_2
inst✝³ : Semiring R
inst✝² : AddCommMonoid M
inst✝¹ : Module R M
inst✝ : IsNoetherian R M
f : End R M
n : ℕ
hn : ∀ (m : ℕ), n ≤ m → LinearMap.ker (f ^ n) = LinearMap.ker (f ^ m)
m : ℕ
hm : n ≤ m
⊢ LinearMap.ker (f ^ n) ⊓ (f ^ m).range = ⊥

Tactic:
Submodule.eq_bot_iff

Goal state after:
R : Type u_1
M : Type u_2
inst✝³ : Semiring R
inst✝² : AddCommMonoid M
inst✝¹ : Module R M
inst✝ : IsNoetherian R M
f : End R M
n : ℕ
hn : ∀ (m : ℕ), n ≤ m → LinearMap.ker (f ^ n) = LinearMap.ker (f ^ m)
m : ℕ
hm : n ≤ m
⊢ ∀ x ∈ LinearMap.ker (f ^ n) ⊓ (f ^ m).range, x = 0
Module: Mathlib.Algebra.Order.Module.Defs

Goal state before:
pp: α : 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₂
⊢ a₁ = a₂ ∧ b₁ = b₂ → a₁ • b₁ = a₂ • b₂

Tactic:
rintro ⟨rfl, rfl⟩

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

Goal state before:
pp: α : 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₁
⊢ a₁ = a₂ ∧ b₁ = b₂ → a₁ • b₁ = a₂ • b₂

Tactic:
rintro ⟨rfl, rfl⟩

Goal state after:
α : Type u_1
β : Type u_2
a₁ : α
b₁ : β
inst✝⁶ : Zero α
inst✝⁵ : Zero β
inst✝⁴ : SMulWithZero α β
inst✝³ : PartialOrder α
inst✝² : PartialOrder β
inst✝¹ : PosSMulStrictMono α β
inst✝ : SMulPosStrictMono α β
h₁ : 0 < b₁
ha : a₁ ≤ a₁
h₂ : 0 < a₁
hb : b₁ ≤ b₁
⊢ a₁ • b₁ = 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✝¹ : Zero γ
inst✝ : SMulPosReflectLT α γ
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 lt_of_smul_lt_smul_right h hb

Goal state after:
Module: Mathlib.Order.IsNormal

Goal state before:
pp: case refine_1
α : Type u_1
β : Type u_2
inst✝⁶ : LinearOrder α
inst✝⁵ : WellFoundedLT α
inst✝⁴ : SuccOrder α
inst✝³ : LinearOrder β
inst✝² : NoMaxOrder α
inst✝¹ : OrderBot α
inst✝ : WellFoundedLT β
f : α → β
x : β
hf : IsNormal f
hf' : ∃ y, x ≤ f y
hx : f ⊥ ≤ x
this✝² : Nonempty β
this✝¹ : OrderBot β := WellFoundedLT.toOrderBot β
this✝ : ConditionallyCompleteLinearOrderBot α := WellFoundedLT.conditionallyCompleteLinearOrderBot α
this : ConditionallyCompleteLinearOrderBot β := WellFoundedLT.conditionallyCompleteLinearOrderBot β
H : BddAbove (f ⁻¹' Iic x)
⊢ f (sSup (f ⁻¹' Iic x)) ≤ x

pp: case refine_2
α : Type u_1
β : Type u_2
inst✝⁶ : LinearOrder α
inst✝⁵ : WellFoundedLT α
inst✝⁴ : SuccOrder α
inst✝³ : LinearOrder β
inst✝² : NoMaxOrder α
inst✝¹ : OrderBot α
inst✝ : WellFoundedLT β
f : α → β
x : β
hf : IsNormal f
hf' : ∃ y, x ≤ f y
hx : f ⊥ ≤ x
this✝² : Nonempty β
this✝¹ : OrderBot β := WellFoundedLT.toOrderBot β
this✝ : ConditionallyCompleteLinearOrderBot α := WellFoundedLT.conditionallyCompleteLinearOrderBot α
this : ConditionallyCompleteLinearOrderBot β := WellFoundedLT.conditionallyCompleteLinearOrderBot β
H : BddAbove (f ⁻¹' Iic x)
⊢ x < f (succ (sSup (f ⁻¹' Iic x)))

Tactic:
· rw [hf.le_iff_le_sSup ⟨⊥, hx⟩ H]

Goal state after:
case refine_2
α : Type u_1
β : Type u_2
inst✝⁶ : LinearOrder α
inst✝⁵ : WellFoundedLT α
inst✝⁴ : SuccOrder α
inst✝³ : LinearOrder β
inst✝² : NoMaxOrder α
inst✝¹ : OrderBot α
inst✝ : WellFoundedLT β
f : α → β
x : β
hf : IsNormal f
hf' : ∃ y, x ≤ f y
hx : f ⊥ ≤ x
this✝² : Nonempty β
this✝¹ : OrderBot β := WellFoundedLT.toOrderBot β
this✝ : ConditionallyCompleteLinearOrderBot α := WellFoundedLT.conditionallyCompleteLinearOrderBot α
this : ConditionallyCompleteLinearOrderBot β := WellFoundedLT.conditionallyCompleteLinearOrderBot β
H : BddAbove (f ⁻¹' Iic x)
⊢ x < f (succ (sSup (f ⁻¹' Iic x)))
Module: Mathlib.SetTheory.Ordinal.Arithmetic

Goal state before:
pp: a b : Ordinal.{u_4}
α : Type u_4
r : α → α → Prop
x✝¹ : IsWellOrder α r
β : Type u_4
s : β → β → Prop
x✝ : IsWellOrder β s
⊢ type r + type s = 0 ↔ type r = 0 ∧ type s = 0

Tactic:
by
    simp_rw [← type_sum_lex, type_eq_zero_iff_isEmpty]
    exact isEmpty_sum

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

Goal state before:
pp: case inr
o : Ordinal.{u_4}
ho : IsSuccPrelimit o
⊢ o.pred = o ↔ IsSuccPrelimit o

Tactic:
simp_rw [ho.ordinalPred_eq, ho]

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

Goal state before:
pp: a b : Ordinal.{u_4}
h : b ≤ a
⊢ b + (a - b) = a

Tactic:
by
  change b + dite _ _ _ = a
  rw [dif_pos h]
  exact (Classical.choose_spec (exists_add_of_le h)).symm

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

Goal state before:
pp: α : Type u_1
inst✝² : LinearOrder α
inst✝¹ : WellFoundedLT α
inst✝ : IsRegularCardinalOrder α
s : Set α
hs : IsCofinal s
H : StrictMono (Subtype.val ∘ ⇑(enum s hs)) := ⋯
hs' : ∀ ⦃d : Set α⦄, d ⊆ s → d.Nonempty → ∀ ⦃a : α⦄, IsLUB d a → a ∈ s
a : α
ha : IsSuccLimit a
b : α
hb : ∀ b_1 < a, (Subtype.val ∘ ⇑(enum s hs)) b_1 ≤ b
bdd : BddAbove (Subtype.val ∘ ⇑(enum s hs) '' Iio a)
this✝¹ : Nonempty α
this✝ : OrderBot α := ⋯
this : ConditionallyCompleteLinearOrderBot α := ⋯
⊢ sSup (Subtype.val ∘ ⇑(enum s hs) '' Iio a) ≤ b

Tactic:
apply csSup_le'
    simpa [upperBounds]

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

Goal state before:
pp: f : Ordinal.{max u_3 u_4} → Ordinal.{max u_4 u_5}
H : IsNormal f
o : Ordinal.{u_4}
α : Type u_4
r : α → α → Prop
x✝ : IsWellOrder α r
g : (a : Ordinal.{u_4}) → a < type r → Ordinal.{max u_4 u_3}
h : type r ≠ 0
this : Nonempty α
⊢ f ((type r).bsup g) = (type r).bsup fun a h ↦ f (g a h)

Tactic:
← iSup'_eq_bsup r,

Goal state after:
f : Ordinal.{max u_3 u_4} → Ordinal.{max u_4 u_5}
H : IsNormal f
o : Ordinal.{u_4}
α : Type u_4
r : α → α → Prop
x✝ : IsWellOrder α r
g : (a : Ordinal.{u_4}) → a < type r → Ordinal.{max u_4 u_3}
h : type r ≠ 0
this : Nonempty α
⊢ f (iSup (familyOfBFamily' r ?ho g)) = (type r).bsup fun a h ↦ f (g a h)

case ho
f : Ordinal.{max u_3 u_4} → Ordinal.{max u_4 u_5}
H : IsNormal f
o : Ordinal.{u_4}
α : Type u_4
r : α → α → Prop
x✝ : IsWellOrder α r
g : (a : Ordinal.{u_4}) → a < type r → Ordinal.{max u_4 u_3}
h : type r ≠ 0
this : Nonempty α
⊢ type r = type r
Module: Mathlib.SetTheory.Ordinal.Arithmetic

Goal state before:
pp: a b : Ordinal.{u_4}
l : IsSuccLimit a
b0 : 0 < b
⊢ IsSuccLimit (a * b)

Tactic:
rcases zero_or_succ_or_isSuccLimit b with (rfl | ⟨b, rfl⟩ | lb)
  · exact b0.false.elim
  · rw [mul_succ]
    exact isSuccLimit_add _ l
  · exact isSuccLimit_mul_right l.bot_lt lb

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

Goal state before:
pp: n : ℕ
⊢ (↑n).ord = ↑n

Tactic:
apply (ord_le.2 (card_nat n).ge).antisymm
  induction n with
  | zero => exact zero_le
  | succ n IH => exact (IH.trans_lt <| by simp).succ_le

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

Goal state before:
pp: case inr
a b : Ordinal.{u_4}
h : a ≤ b
c : Ordinal.{u_4}
hc : c ≠ 0
⊢ a / c ≤ b / c

Tactic:
rw [← mul_le_iff_le_div hc]

Goal state after:
case inr
a b : Ordinal.{u_4}
h : a ≤ b
c : Ordinal.{u_4}
hc : c ≠ 0
⊢ c * (a / c) ≤ b
Module: Mathlib.SetTheory.Ordinal.Family

Goal state before:
pp: o : Ordinal.{u}
o' : Ordinal.{v}
f : (a : Ordinal.{u}) → a < o → Ordinal.{max (max u v) w}
g : (a : Ordinal.{v}) → a < o' → Ordinal.{max (max u v) w}
h : o.brange f ⊆ o'.brange g
a : Ordinal.{max (max u v) w}
x✝ : a ∈ o.brange fun a ha ↦ succ (f a ha)
b : Ordinal.{u}
hb : b < o
hb' : (fun a ha ↦ succ (f a ha)) b hb = a
c : Ordinal.{v}
hc : c < o'
hc' : g c hc = f b hb
⊢ a ∈ o'.brange fun a ha ↦ succ (g a ha)

Tactic:
simp_rw [← hc'] at hb'

Goal state after:
o : Ordinal.{u}
o' : Ordinal.{v}
f : (a : Ordinal.{u}) → a < o → Ordinal.{max (max u v) w}
g : (a : Ordinal.{v}) → a < o' → Ordinal.{max (max u v) w}
h : o.brange f ⊆ o'.brange g
a : Ordinal.{max (max u v) w}
x✝ : a ∈ o.brange fun a ha ↦ succ (f a ha)
b : Ordinal.{u}
hb : b < o
c : Ordinal.{v}
hc : c < o'
hc' : g c hc = f b hb
hb' : succ (g c hc) = a
⊢ a ∈ o'.brange fun a ha ↦ succ (g a ha)
Module: Mathlib.SetTheory.Ordinal.Arithmetic

Goal state before:
pp: a c b : Ordinal.{u_4}
x✝ : a ∣ c
d : Ordinal.{u_4}
e : c = a * d
⊢ a ∣ a * b + c

Tactic:
by
      rw [e, ← mul_add]
      apply dvd_mul_right

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

Goal state before:
pp: case inr.inr.inr.hb
b k n : ℕ
hn : n ≠ 0
hk : k > 0
hb : 1 ≥ b
⊢ b ^ k ≤ 1

Tactic:
Nat.pow_le_one_iff (Nat.ne_of_gt hk)

Goal state after:
case inr.inr.inr.hb
b k n : ℕ
hn : n ≠ 0
hk : k > 0
hb : 1 ≥ b
⊢ b ≤ 1
Module: Mathlib.SetTheory.Ordinal.Exponential

Goal state before:
pp: b u v x : Ordinal.{u_1}
hv : v < b
hu : u < x
⊢ b ^ u * v < b ^ x

Tactic:
by
  simpa using opow_mul_add_lt_opow hv (opow_pos _ hv.pos) hu

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

Goal state before:
pp: a b : Ordinal.{u_1}
hb : 0 < b
hba : b ≤ a ^ ω
⊢ nfp (fun x ↦ a * x) b = a ^ ω

Tactic:
rcases eq_zero_or_pos a with rfl | ha
  · rw [zero_opow omega0_ne_zero] at hba
    cases hba.not_gt hb
  apply le_antisymm
  · apply nfp_le_fp (isNormal_mul_right ha).monotone hba
    rw [← opow_one_add, one_add_omega0]
  rw [← nfp_mul_one ha]
  exact nfp_monotone (isNormal_mul_right ha).monotone (one_le_iff_pos.2 hb)

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

Goal state before:
pp: case inr
o : Ordinal.{u_1}
ha' : o ≠ 0
a : Ordinal.{u_1}
ha : a < ω ^ o
⊢ a + a < ω ^ o

Tactic:
obtain ⟨c, hc, m, hm⟩ := (lt_omega0_opow ha').1 ha

Goal state after:
case inr
o : Ordinal.{u_1}
ha' : o ≠ 0
a : Ordinal.{u_1}
ha : a < ω ^ o
c : Ordinal.{u_1}
hc : c < o
m : ℕ
hm : a < ω ^ c * ↑m
⊢ a + a < ω ^ o
Module: Mathlib.SetTheory.Cardinal.Arithmetic

Goal state before:
pp: a b : Cardinal.{u_1}
h' : a ≠ 0
h : ℵ₀ ≤ b
⊢ a * b = max a b

Tactic:
rw [mul_comm, max_comm]

Goal state after:
a b : Cardinal.{u_1}
h' : a ≠ 0
h : ℵ₀ ≤ b
⊢ b * a = max b a
Module: Mathlib.SetTheory.Cardinal.Aleph

Goal state before:
pp: ⊢ range ⇑ℵ_ = Ici ℵ₀

Tactic:
ext c

Goal state after:
c : Cardinal.{u_1}
⊢ c ∈ range ⇑ℵ_ ↔ c ∈ Ici ℵ₀
Module: Mathlib.SetTheory.Cardinal.Arithmetic

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

Tactic:
· rcases le_or_gt ℵ₀ b with hb | hb
    · rw [mul_comm, mul_eq_max_of_aleph0_le_left hb ha0, max_comm]
      exact le_max_left _ _
    · exact le_max_of_le_right (mul_lt_aleph0 ha hb).le

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

Goal state before:
pp: ⊢ preBeth ω = ℵ₀

Tactic:
apply le_antisymm
  · 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
  · simpa using preAleph_le_preBeth ω

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

Goal state before:
pp: case refine_1.inl
a b : Cardinal.{u_1}
h : a * b = a
ha : ℵ₀ ≤ a
⊢ (ℵ₀ ≤ a ∧ b ≤ a) ∧ b ≠ 0 ∨ b = 1 ∨ a = 0

pp: case refine_1.inr
a b : Cardinal.{u_1}
h : a * b = a
ha : a < ℵ₀
⊢ (ℵ₀ ≤ a ∧ b ≤ a) ∧ b ≠ 0 ∨ b = 1 ∨ a = 0

Tactic:
· have : a ≠ 0 := by
        rintro rfl
        exact ha.not_gt aleph0_pos
      left
      rw [and_assoc]
      use ha
      constructor
      · rw [← not_lt]
        exact fun hb => ne_of_gt (hb.trans_le (le_mul_left this)) h
      · rintro rfl
        apply this
        rw [mul_zero] at h
        exact h.symm

Goal state after:
case refine_1.inr
a b : Cardinal.{u_1}
h : a * b = a
ha : a < ℵ₀
⊢ (ℵ₀ ≤ a ∧ b ≤ a) ∧ b ≠ 0 ∨ b = 1 ∨ a = 0
Module: Mathlib.SetTheory.Cardinal.Cofinality.Ordinal

Goal state before:
pp: β : Type v
inst✝² : LinearOrder β
inst✝¹ : Small.{u, v} β
inst✝ : NoMaxOrder β
f : β → Ordinal.{u}
hf : StrictMono f
⊢ Cardinal.lift.{v, u} (⨆ i, f i).cof = Cardinal.lift.{u, v} (Order.cof β)

Tactic:
← iSup_add_one hf,

Goal state after:
β : Type v
inst✝² : LinearOrder β
inst✝¹ : Small.{u, v} β
inst✝ : NoMaxOrder β
f : β → Ordinal.{u}
hf : StrictMono f
⊢ Cardinal.lift.{v, u} (⨆ i, f i + 1).cof = Cardinal.lift.{u, v} (Order.cof β)
Module: Mathlib.SetTheory.Ordinal.FundamentalSequence

Goal state before:
pp: case inl
a o : Ordinal.{u}
f : (b : Ordinal.{u}) → b < o → Ordinal.{u}
hf : a.IsFundamentalSequence o f
i j : Ordinal.{u}
hi : i < o
hj : j < o
hij✝ : i ≤ j
hij : i < j
⊢ f i hi ≤ f j hj

Tactic:
exact (hf.2.1 hi hj hij).le

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

Goal state before:
pp: ι : Type u
inst✝ : Small.{v, u} ι
f : ι → Cardinal.{v}
hι : ℵ₀ ≤ #ι
h : lift.{v, u} #ι ≤ lift.{u, v} (⨆ i, f i)
⊢ sum f = lift.{u, v} (⨆ i, f i)

Tactic:
rw [lift_iSup bddAbove_of_small] at h
  apply (lift_iSup_le_sum f).antisymm'
  convert! sum_le_lift_mk_mul_iSup_lift f
  rw [mul_eq_max (aleph0_le_lift.mpr hι) ((aleph0_le_lift.mpr hι).trans h), max_eq_right h,
    lift_iSup bddAbove_of_small]

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

Goal state before:
pp: case mp
a b c : Cardinal.{u_1}
hc : c < ℵ₀
⊢ b ≤ a → b + c ≤ a + c

Tactic:
simp [add_le_add_iff_of_lt_aleph0 hc]

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

Goal state before:
pp: case mpr
a b c : Cardinal.{u_1}
hc : c < ℵ₀
⊢ b + c ≤ a + c → b ≤ a

Tactic:
simp [add_le_add_iff_of_lt_aleph0 hc]

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

Goal state before:
pp: ⊢ (ℵ_ 1).IsRegular

Tactic:
rw [← succ_aleph0]
  exact isRegular_succ le_rfl

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

Goal state before:
pp: ⊢ (ℵ_ 1).IsRegular

Tactic:
by
  rw [← succ_aleph0]
  exact isRegular_succ le_rfl

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

Goal state before:
pp: ⊢ (ω_ 1).cof = ℵ_ 1

Tactic:
simpa using isRegular_aleph_one.cof_omega_eq

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

Goal state before:
pp: ⊢ Cardinal.univ.{u, max (u + 1) v} = Cardinal.univ.{u, v}

Tactic:
Cardinal.univ_umax.{u, v}

Goal state after:
⊢ Cardinal.univ.{u, v} = Cardinal.univ.{u, v}
Module: Mathlib.SetTheory.Cardinal.Pigeonhole

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝ : Infinite β
f : α → Finset β
w : ⋃ a, ↑(f a) = Set.univ
h : #↑(range f) < #β
u : ∀ (b : β), ∃ a, b ∈ f a :=
  fun b ↦
    Eq.mp (Eq.trans mem_iUnion._simp_1 (congrArg Exists (funext fun i ↦ SetLike.mem_coe._simp_1)))
      (Eq.ge w (mem_univ b))
u' : β → ↑(range f) := fun b ↦ ⟨f ⋯.choose, ⋯⟩
a : α
p : β
m✝ : p ∈ u' ⁻¹' {⟨f a, ⋯⟩}
m : f ⋯.choose = f a
⊢ p ∈ ↑(f ⋯.choose)

Tactic:
apply fun b => (u b).choose_spec

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

Goal state before:
pp: case refine_2
α : Type u
inst✝ : Infinite α
f g : α → Bool
h :
  (fun f ↦ Involutive.toPerm (fun x ↦ (x.1, f x.1 ^^ x.2)) ⋯) f =
    (fun f ↦ Involutive.toPerm (fun x ↦ (x.1, f x.1 ^^ x.2)) ⋯) g
a : α
⊢ f a = g a

Tactic:
rw [← (f a).xor_false, ← (g a).xor_false]

Goal state after:
case refine_2
α : Type u
inst✝ : Infinite α
f g : α → Bool
h :
  (fun f ↦ Involutive.toPerm (fun x ↦ (x.1, f x.1 ^^ x.2)) ⋯) f =
    (fun f ↦ Involutive.toPerm (fun x ↦ (x.1, f x.1 ^^ x.2)) ⋯) g
a : α
⊢ (f a ^^ false) = (g a ^^ false)
Module: Mathlib.Data.DFinsupp.Defs

Goal state before:
pp: ι : Type u
β : ι → Type v
inst✝¹ : (i : ι) → Zero (β i)
inst✝ : DecidableEq ι
i j : ι
xi : β i
xj : β j
⊢ single i xi = single j xj ↔ i = j ∧ xi ≍ xj ∨ xi = 0 ∧ xj = 0

Tactic:
by
  constructor
  · intro h
    by_cases hij : i = j
    · subst hij
      exact Or.inl ⟨rfl, heq_of_eq (DFinsupp.single_injective h)⟩
    · have h_coe : ⇑(DFinsupp.single i xi) = DFinsupp.single j xj := congr_arg (⇑) h
      have hci := congr_fun h_coe i
      have hcj := congr_fun h_coe j
      rw [DFinsupp.single_eq_same] at hci hcj
      rw [DFinsupp.single_eq_of_ne hij] at hci
      rw [DFinsupp.single_eq_of_ne (Ne.symm hij)] at hcj
      exact Or.inr ⟨hci, hcj.symm⟩
  · rintro (⟨rfl, hxi⟩ | ⟨hi, hj⟩)
    · rw [eq_of_heq hxi]
    · rw [hi, hj, DFinsupp.single_zero, DFinsupp.single_zero]

Goal state after:
Module: Mathlib.Data.Fintype.Quotient

Goal state before:
pp: case a
ι : Type u_1
inst✝¹ : Fintype ι
inst✝ : DecidableEq ι
α : ι → Sort u_2
S : (i : ι) → Setoid (α i)
β : Sort u_3
e : IsEmpty ι
q : (i : ι) → Quotient (S i)
f : ((i : ι) → α i) → β
h : ∀ (a b : (i : ι) → α i), (∀ (i : ι), a i ≈ b i) → f a = f b
a✝ : (i : ι) → α i
⊢ ⟦a✝⟧.liftOn f h = f fun a ↦ e.elim a

Tactic:
exact h _ _ e.elim

Goal state after:
Module: Mathlib.LinearAlgebra.Dual.Defs

Goal state before:
pp: R : Type u_1
M : Type u_2
M' : Type u_3
inst✝⁴ : CommSemiring R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
inst✝¹ : AddCommMonoid M'
inst✝ : Module R M'
B : M →ₗ[R] M' →ₗ[R] R
x : M'
⊢ x ∈ B.range.dualCoannihilator ↔ x ∈ B.flip.ker

Tactic:
simp [LinearMap.ext_iff (f := B.flip x)]

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

Goal state before:
pp: ι : Type u'
R : Type u_2
M : Type u_4
v : ι → M
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
η : Type u_6
s : Set η
t : η → Set ι
hs : DirectedOn (t ⁻¹'o fun x1 x2 ↦ x1 ⊆ x2) s
h : ∀ a ∈ s, LinearIndepOn R v (t a)
⊢ LinearIndepOn R v (⋃ a ∈ s, t a)

Tactic:
by
  rw [biUnion_eq_iUnion]
  exact linearIndepOn_iUnion_of_directed (directed_comp.2 <| hs.directed_val) (by simpa using h)

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

Goal state before:
pp: ι : Type u'
R : Type u_2
M : Type u_4
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
i : ι
m : M
hm : (Finsupp.lsingle i) m ∈ ↑(⨆ j, ⨆ (_ : j ≠ i), (fun i ↦ (Finsupp.lsingle i).range) j)
this : ⨆ j, ⨆ (_ : j ≠ i), (Finsupp.lsingle j).range ≤ Finsupp.supported M R {i}ᶜ
⊢ (Finsupp.lsingle i) m ∈ ⊥

Tactic:
have := (Finsupp.mem_supported ..).mp (this hm); simp_all

Goal state after:
Module: Mathlib.LinearAlgebra.DFinsupp

Goal state before:
pp: case refine_2
ι : Type u_1
R : Type u_3
N : Type u_6
inst✝² : Semiring R
inst✝¹ : AddCommMonoid N
inst✝ : Module R N
p : ι → Submodule R N
f : ι →₀ N
hf : ∀ (i : ι), f i ∈ p i
i : ι
hi : i ∈ f.support
⊢ (fun x xi ↦ ↑xi) i ((DFinsupp.mk f.support fun i ↦ ⟨f ↑i, ⋯⟩) i) = (fun _i xi ↦ xi) i (f i)

Tactic:
simp [Finsupp.mem_support_iff.mp hi]

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

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

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

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

Goal state before:
pp: k : Type u₁
G : Type u₂
R : Type u_2
inst✝⁴ : Semiring k
inst✝³ : Mul G
inst✝² : Semiring R
g_hom : Type u_6
inst✝¹ : FunLike g_hom G R
inst✝ : MulHomClass g_hom G R
f : k →+* R
g : g_hom
a b : k[G]
h_comm : ∀ {x y : G}, y ∈ a.coeff.support → Commute (f (b.coeff x)) (g y)
y : G
hy : y ∈ a.coeff.support
x : G
_hx : x ∈ b.coeff.support
⊢ (fun a_1 b ↦ ↑f (a.coeff y * b) * g (y * a_1)) x (b.coeff x) =
    (fun a_1 c ↦ ↑f (a.coeff y) * g y * (↑f c * g a_1)) x (b.coeff x)

Tactic:
simp [mul_assoc, (h_comm hy).left_comm]

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

Goal state before:
pp: k : Type u₁
G : Type u₂
R : Type u_2
inst✝⁴ : Semiring k
inst✝³ : Add G
inst✝² : Semiring R
g_hom : Type u_6
inst✝¹ : FunLike g_hom (Multiplicative G) R
inst✝ : MulHomClass g_hom (Multiplicative G) R
f : k →+* R
g : g_hom
a b : k[G]
h_comm : ∀ {x y : G}, y ∈ a.coeff.support → Commute (f (b.coeff x)) (g (Multiplicative.ofAdd y))
y : G
hy : y ∈ a.coeff.support
x : G
_hx : x ∈ b.coeff.support
⊢ (fun a_1 b ↦ ↑f (a.coeff y * b) * g (Multiplicative.ofAdd (y + a_1))) x (b.coeff x) =
    (fun a_1 c ↦ ↑f (a.coeff y) * g (Multiplicative.ofAdd y) * (↑f c * g (Multiplicative.ofAdd a_1))) x (b.coeff x)

Tactic:
simp [mul_assoc, (h_comm hy).left_comm]

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))
u : Finset V
hust : ↑u ⊆ s ∪ ↑t
hsu : s ⊆ ↑u
Eq : u.card = (s' ∪ t).card
hb₁u : b₁ ∉ u
⊢ (insert b₁ u).card = (s' ∪ insert b₁ t).card

Tactic:
simp [Eq, hb₁t, hb₁s', hb₁u]

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

Goal state before:
pp: R : Type u_3
S : Type u_4
M : Type u_6
inst✝² : Semiring R
inst✝¹ : Semiring S
inst✝ : Mul M
f : R →+* S
x y : R[M]
⊢ map (↑f) (x * y) = map (↑f) x * map (↑f) y

Tactic:
by
  classical
  ext
  simp [mul_def, sum_mapRange_index, map_finsuppSum, single_apply, apply_ite]

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
f : G →ₙ* H
hf : Function.Injective ⇑f
a0 b0 : G
A B : Finset H
u : UniqueMul A B (f a0) (f b0)
⊢ UniqueMul (A.preimage ⇑f ⋯) (B.preimage ⇑f ⋯) a0 b0

Tactic:
by
  intro a b ha hb ab
  simp only [← hf.eq_iff, map_mul] at ab ⊢
  exact u (Finset.mem_preimage.mp ha) (Finset.mem_preimage.mp hb) ab

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

Goal state before:
pp: case refine_2
α : Type u_1
R : Type u_5
inst✝ : Semiring R
β : Type u_7
u : α → β
i : α
⊢ single (u i) 1 ∈ ↑(lmapDomain R R u).range

Tactic:
exact ⟨Finsupp.single i 1, by simp⟩

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
f g : End R M
p : Submodule R M
hp : p ∈ {p | p ≤ Submodule.comap f p}
q : Submodule R M
hq : q ∈ {p | p ≤ Submodule.comap f p}
⊢ p ⊓ q ∈ {p | p ≤ Submodule.comap f p}

Tactic:
by
    simp only [Set.mem_ofPred_eq, Submodule.comap_inf, le_inf_iff]
    exact ⟨inf_le_of_left_le hp, inf_le_of_right_le hq⟩

Goal state after: