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

Goal state before:
pp: case refine_1
α : Type u_1
β : Type u_2
g : α → β
f : Filter α
s : Set α
hs : s ∈ f
⊢ g '' s ∈ (pure g).seq f

pp: case refine_2
α : Type u_1
β : Type u_2
g : α → β
f : Filter α
s : Set (α → β)
hs : s ∈ pure g
t : Set α
ht : t ∈ f
⊢ s.seq t ∈ map g f

Tactic:
· rw [← singleton_seq]
    apply seq_mem_seq _ hs
    exact singleton_mem_pure

Goal state after:
case refine_2
α : Type u_1
β : Type u_2
g : α → β
f : Filter α
s : Set (α → β)
hs : s ∈ pure g
t : Set α
ht : t ∈ f
⊢ s.seq t ∈ map g f
Module: Mathlib.Order.Filter.Map

Goal state before:
pp: case refine_2
α : Type u_1
β : Type u_2
g : α → β
f : Filter α
s : Set (α → β)
hs : s ∈ pure g
t : Set α
ht : t ∈ f
⊢ g '' t ⊆ s.seq t

Tactic:
rintro b ⟨a, ha, rfl⟩

Goal state after:
case refine_2
α : Type u_1
β : Type u_2
g : α → β
f : Filter α
s : Set (α → β)
hs : s ∈ pure g
t : Set α
ht : t ∈ f
a : α
ha : a ∈ t
⊢ g a ∈ s.seq t
Module: Mathlib.Order.Filter.AtTopBot.Basic

Goal state before:
pp: case refine_2
α : Type u_3
β : Type u_4
inst✝³ : Preorder α
inst✝² : IsDirectedOrder α
inst✝¹ : Preorder β
inst✝ : IsDirectedOrder β
f : α → β
hf : Monotone f
b : β
this : Nonempty α
g : β → α
hfg : ∀ (c : β), b ≤ c → f (g c) = c
hgle : ∀ (c : β), b ≤ c → ∀ (a : α), f a ≤ c ↔ a ≤ g c
⊢ atTop ≤ map f atTop

Tactic:
have : Nonempty α := ⟨g b⟩
    rw [(atTop_basis.map f).ge_iff]
    intro a _
    filter_upwards [eventually_ge_atTop (f a), eventually_ge_atTop b] with c hac hbc
    exact ⟨g c, (hgle _ hbc _).1 hac, hfg _ hbc⟩

Goal state after:
Module: Mathlib.Data.Set.Finite.Lemmas

Goal state before:
pp: α : Type u
inst✝ : Finite α
C : Set α → Prop
S0 : Set α
H0 : C S0
H1 : ∀ (S : Set α), S ≠ univ → C S → ∃ a ∉ S, C (insert a S)
⊢ ∀ s ⊂ univ, C s → ∃ a ∈ univ \ s, C (insert a s)

Tactic:
simpa [ssubset_univ_iff]

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

Goal state before:
pp: A : Type u
inst✝² : Semiring A
M : Type v
inst✝¹ : AddCommMonoid M
inst✝ : Module A M
N : Submodule A M
⊢ N.FG ↔ ∃ G, ∃ (_ : Finite G), ∃ g, span A (range g) = N

Tactic:
by
  constructor
  · intro hN
    obtain ⟨n, f, h⟩ := fg_iff_exists_fin_generating_family.mp hN
    refine ⟨ULift (Fin n), inferInstance, f ∘ ULift.down, ?_⟩
    convert! h
    ext
    simp
  · rintro ⟨G, _, g, hg⟩
    have := Fintype.ofFinite (range g)
    exact ⟨(range g).toFinset, by simpa⟩

Goal state after:
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
α : Type (max 0 u_2) := { N // N.FG }
H : WellFoundedGT { N // N.FG }
N N₀ : Submodule R M
h₁ : N₀.FG
e : N₀ ≤ N
h₂ : ∀ x ∈ {N' | ↑N' ≤ N}, ¬⟨N₀, h₁⟩ < x
⊢ N = N₀

Tactic:
refine (e.antisymm ?_).symm

Goal state after:
R : Type u_1
M : Type u_2
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
α : Type (max 0 u_2) := { N // N.FG }
H : WellFoundedGT { N // N.FG }
N N₀ : Submodule R M
h₁ : N₀.FG
e : N₀ ≤ N
h₂ : ∀ x ∈ {N' | ↑N' ≤ N}, ¬⟨N₀, h₁⟩ < x
⊢ N ≤ N₀
Module: Mathlib.Order.Cofinal

Goal state before:
pp: α : Type u_1
inst✝ : LinearOrder α
s : Set α
h : ¬BddAbove s
⊢ IsCofinal s

Tactic:
contrapose h

Goal state after:
α : Type u_1
inst✝ : LinearOrder α
s : Set α
h : ¬IsCofinal s
⊢ BddAbove s
Module: Mathlib.SetTheory.Cardinal.Cofinality.Basic

Goal state before:
pp: α : Type u
inst✝ : Preorder α
c : Cardinal.{u}
⊢ c ≤ cof α ↔ ∀ (s : Set α), IsCofinal s → c ≤ #↑s

Tactic:
by
  simpa using @le_lift_cof_iff.{u, u} α _ c

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

Goal state before:
pp: R : Type u_1
M : Type u_2
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
s : Submodule R M
sp : M → Submodule R M := fun a ↦ R ∙ a
supr_rw : ∀ (t : Finset M), ⨆ x ∈ t, sp x = ⨆ x ∈ ↑t, sp x
h : ∀ (s_1 : Set (Submodule R M)), s ≤ sSup s_1 → ∃ t, ↑t ⊆ s_1 ∧ s ≤ t.sup id
sSup' : s = sSup (sp '' ↑s)
u : Finset (Submodule R M)
huspan : ↑u ⊆ sp '' ↑s
husup : s ≤ u.sup id
⊢ s = u.sup id

Tactic:
suffices u.sup id ≤ s from le_antisymm husup this

Goal state after:
R : Type u_1
M : Type u_2
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
s : Submodule R M
sp : M → Submodule R M := fun a ↦ R ∙ a
supr_rw : ∀ (t : Finset M), ⨆ x ∈ t, sp x = ⨆ x ∈ ↑t, sp x
h : ∀ (s_1 : Set (Submodule R M)), s ≤ sSup s_1 → ∃ t, ↑t ⊆ s_1 ∧ s ≤ t.sup id
sSup' : s = sSup (sp '' ↑s)
u : Finset (Submodule R M)
huspan : ↑u ⊆ sp '' ↑s
husup : s ≤ u.sup id
⊢ u.sup id ≤ s
Module: Mathlib.RingTheory.Finiteness.Basic

Goal state before:
pp: R : Type u_1
A : Type u_2
B : Type u_3
M : Type u_4
N : Type u_5
inst✝⁵ : Semiring R
inst✝⁴ : AddCommMonoid M
inst✝³ : Module R M
inst✝² : AddCommMonoid N
inst✝¹ : Module R N
inst✝ : Finite M
⊢ Module.Finite R M

Tactic:
cases nonempty_fintype M
  exact ⟨⟨Finset.univ, by rw [Finset.coe_univ, span_univ]⟩⟩

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

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝⁷ : Ring α
inst✝⁶ : LinearOrder α
inst✝⁵ : IsStrictOrderedRing α
inst✝⁴ : AddCommGroup β
inst✝³ : LinearOrder β
inst✝² : IsOrderedAddMonoid β
inst✝¹ : Module α β
inst✝ : PosSMulStrictMono α β
a : α
b : β
hab : 0 ≤ a • b
⊢ 0 ≤ a ∧ 0 ≤ b ∨ a ≤ 0 ∧ b ≤ 0

Tactic:
simp only [Decidable.or_iff_not_not_and_not, not_and, not_le]
  refine fun ab nab ↦ hab.not_gt ?_
  obtain ha | rfl | ha := lt_trichotomy 0 a
  exacts [smul_neg_of_pos_of_neg ha (ab ha.le), ((ab le_rfl).asymm (nab le_rfl)).elim,
    smul_neg_of_neg_of_pos ha (nab ha.le)]

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✝ : SMulPosStrictMono α γ
hf : ∀ {b₁ b₂ : β}, f b₁ ≤ f b₂ ↔ b₁ ≤ b₂
b : β
a₁ a₂ : α
ha : a₁ < a₂
smul : ∀ (a : α) (b : β), True
zero : True
hb : 0 < f b
⊢ a₁ • f b < a₂ • f b

Tactic:
exact smul_lt_smul_of_pos_right ha hb

Goal state after:
Module: Mathlib.Order.IsNormal

Goal state before:
pp: case a
α : Type u_1
inst✝¹ : ConditionallyCompleteLinearOrder α
inst✝ : WellFoundedLT α
f : α → α
a : α
hf : IsNormal f
hf' : BddAbove (range fun n ↦ f^[n] a)
n : ℕ
⊢ f^[n] a ≤ ⨆ i, f (f^[i] a)

Tactic:
apply hf.strictMono.le_apply.trans
    apply (le_ciSup (hf'.mono _) n)
    simp_rw [← f.iterate_succ_apply']
    grind

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

Goal state before:
pp: case refine_1
α : Type u
β : Type v
γ : Type w
r✝ : α → α → Prop
s : β → β → Prop
t : γ → γ → Prop
r : α → α → Prop
inst✝ : IsWellOrder α r
a b : α
ha : r a b
⊢ ∀ (a_1 : { x // r x a }), (PrincipalSeg.ofElement r a).toRelEmbedding a_1 ∈ fun x ↦ r x b

Tactic:
rintro ⟨c, hc⟩
    exact trans hc ha

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

Goal state before:
pp: a b : Ordinal.{v}
α : Type v
r : α → α → Prop
x✝¹ : IsWellOrder α r
β : Type v
s : β → β → Prop
x✝ : IsWellOrder β s
⊢ lift.{u, v} (type r) ≤ lift.{u, v} (type s) ↔ type r ≤ type s

Tactic:
rw [← lift_umax]
    exact lift_type_le.{_, _, u}

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

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

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

Tactic:
· have hs' := bddAbove_add_one_image_iff.2 hs
    rw [csSup_le_iff' hs]
    exact fun x hx ↦ (lt_add_one _).le.trans (le_csSup hs' (mem_image_of_mem _ hx))

Goal state after:
case neg
s : Set Ordinal.{u_3}
hs : ¬BddAbove s
⊢ sSup s ≤ sSup ((fun x ↦ x + 1) '' s)
Module: Mathlib.SetTheory.Ordinal.Family

Goal state before:
pp: β : Type u_2
f : β → Ordinal.{u_3}
⊢ ⨆ i, f i ≤ ⨆ i, f i + 1

Tactic:
by
  rw [iSup, iSup, range_comp' (· + 1)]
  exact sSup_le_sSup_add_one _

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

Goal state before:
pp: a : Ordinal.{u}
f : ↑(Iio a) → Ordinal.{u}
hf : StrictMono f
ha : IsSuccPrelimit a
⊢ ⨆ i, f i + 1 = ⨆ i, f i

Tactic:
have := ha.noMaxOrder_Iio
  exact iSup_add_one hf

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

Goal state before:
pp: case refine_2
a : Ordinal.{u_4}
h : 0 < a
a✝ : Ordinal.{u_4}
hb : IsSuccLimit a✝
⊢ IsLUB ((fun x ↦ a * x) '' Iio a✝) (a * a✝)

Tactic:
simpa [IsLUB, IsLeast, upperBounds, lowerBounds, mul_le_iff_of_isSuccLimit hb] using
      fun c hc ↦ mul_le_mul_right hc.le a

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

Goal state before:
pp: case succ.inr
n : ℕ
hn : n ≠ 0
fuel : ℕ
ih :
  ∀ {b : ℕ},
    1 < b →
      n < b ^ fuel →
        (go n b fuel).fst = n / b ^ (go n b fuel).snd ∧ b ^ (go n b fuel).snd ≤ n ∧ n < b ^ ((go n b fuel).snd + 1)
b : ℕ
hb : 1 < b
hfuel : n < b ^ (fuel + 1)
hnb : n ≥ b
⊢ (go n b (fuel + 1)).fst = n / b ^ (go n b (fuel + 1)).snd ∧
    b ^ (go n b (fuel + 1)).snd ≤ n ∧ n < b ^ ((go n b (fuel + 1)).snd + 1)

Tactic:
| inr hnb =>

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

Goal state before:
pp: a b : Ordinal.{u_4}
h : a < b
⊢ a % b = a

Tactic:
by
  simp [mod_def, div_eq_zero_of_lt h]

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

Goal state before:
pp: b n : ℕ
hb : 1 < b
hn : 2 ≤ n
⊢ (n + b - 1).succ ≤ n * b

Tactic:
← pred_eq_sub_one,

Goal state after:
b n : ℕ
hb : 1 < b
hn : 2 ≤ n
⊢ (n + b).pred.succ ≤ n * b
Module: Mathlib.SetTheory.Ordinal.Exponential

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

Tactic:
by
  obtain rfl | ha := eq_zero_or_pos a
  · obtain rfl | hc := eq_zero_or_pos c; · simp
    have : b + c ≠ 0 := (hc.trans_le le_add_self).ne'
    rw [zero_opow hc.ne', zero_opow, mul_zero]
    exact (hc.trans_le le_add_self).ne'
  obtain rfl | ha' := (one_le_iff_ne_zero.2 ha.ne').eq_or_lt; · simp
  induction c using limitRecOn with
  | zero => simp
  | add_one c IH => rw [← add_assoc, opow_add_one, IH, opow_add_one, mul_assoc]
  | limit c l IH =>
    refine eq_of_forall_ge_iff fun d ↦
      (((isNormal_opow ha').comp (isNormal_add_right b)).le_iff_forall_le l).trans ?_
    simpa +contextual [IH] using
      (((isNormal_mul_right <| opow_pos b (pos_iff_ne_zero.2 ha.ne')).comp
        (isNormal_opow ha')).le_iff_forall_le l).symm

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

Goal state before:
pp: case inr
b c : Ordinal.{u_1}
ha : IsPrincipal (fun x1 x2 ↦ x1 + x2) ((fun x ↦ ω ^ x) c)
⊢ IsPrincipal (fun x1 x2 ↦ x1 + x2) (ω ^ (c * b))

Tactic:
exact isPrincipal_add_omega0_opow _

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

Goal state before:
pp: case a
a c b : Ordinal.{u_1}
ha : 0 < a
hc : 0 < c
hca : c ≤ a ^ ω
d : Ordinal.{u_1}
hd : nfp (fun x ↦ a * x) (a ^ ω * b + c) = a ^ ω * d
this✝ : a ^ ω * b + c ≤ a ^ ω * d
this : a ^ ω * b < a ^ ω * d
⊢ succ b ≤ d

Tactic:
mul_lt_mul_iff_right₀ (opow_pos ω ha)

Goal state after:
case a
a c b : Ordinal.{u_1}
ha : 0 < a
hc : 0 < c
hca : c ≤ a ^ ω
d : Ordinal.{u_1}
hd : nfp (fun x ↦ a * x) (a ^ ω * b + c) = a ^ ω * d
this✝ : a ^ ω * b + c ≤ a ^ ω * d
this : b < d
⊢ succ b ≤ d
Module: Mathlib.SetTheory.Ordinal.Principal

Goal state before:
pp: o : Ordinal.{u}
ho : o ≤ 2
⊢ IsPrincipal (fun x1 x2 ↦ x1 * x2) o

Tactic:
obtain rfl | rfl | rfl := le_two_iff.1 ho
  exacts [isPrincipal_zero, isPrincipal_mul_one, isPrincipal_mul_two]

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

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

Tactic:
rw [aleph_eq_preAleph, Ordinal.add_sub_cancel_of_le, preAleph.apply_symm_apply]

Goal state after:
c : Cardinal.{u_1}
hc : c ∈ Ici ℵ₀
⊢ ω ≤ preAleph.symm c
Module: Mathlib.SetTheory.Cardinal.Aleph

Goal state before:
pp: c : Cardinal.{u}
n : ℕ
⊢ lift.{v, u} c ≤ ℵ_ ↑n ↔ c ≤ ℵ_ ↑n

Tactic:
by
  simpa using lift_le (b := ℵ_ n)

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

Goal state before:
pp: α : Type u
f : α → Ordinal.{u}
a : Ordinal.{u}
ha : #α < a.cof
hf : ∀ (i : α), f i < a
⊢ ⨆ i, f i < a

Tactic:
rw [← Cardinal.lift_lt.{_, u}, lift_cof] at ha
  simpa using lift_iSup_lt_of_lt_cof ha hf

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

Goal state before:
pp: case refine_2
o i j : Ordinal.{u}
hi✝ : i < 1
hi : i = 0
hj✝ : j < 1
hj : j = 0
h : 0 < j
⊢ (fun x x_1 ↦ o) i hi✝ < (fun x x_1 ↦ o) j hj✝

Tactic:
hj

Goal state after:
case refine_2
o i j : Ordinal.{u}
hi✝ : i < 1
hi : i = 0
hj✝ : j < 1
hj : j = 0
h : 0 < 0
⊢ (fun x x_1 ↦ o) i hi✝ < (fun x x_1 ↦ o) j hj✝
Module: Mathlib.SetTheory.Cardinal.Arithmetic

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

Tactic:
by
  rw [← lift_id'.{u, v} (iSup _)]
  apply sum_eq_lift_iSup_of_lift_mk_le_lift_iSup hι
  rwa [lift_umax, lift_id'.{u, v}]

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

Goal state before:
pp: a : Ordinal.{u}
⊢ ∃ o f, a.IsFundamentalSequence o f

Tactic:
rcases exists_lsub_cof a with ⟨ι, f, hf, hι⟩

Goal state after:
a : Ordinal.{u}
ι : Type u
f : ι → Ordinal.{u}
hf : lsub f = a
hι : #ι = a.cof
⊢ ∃ o f, a.IsFundamentalSequence o f
Module: Mathlib.SetTheory.Cardinal.Arithmetic

Goal state before:
pp: α β γ : Cardinal.{u_1}
γ₀ : γ < ℵ₀
h : α + γ ≤ β + γ
⊢ α ≤ β

Tactic:
contrapose h

Goal state after:
α β γ : Cardinal.{u_1}
γ₀ : γ < ℵ₀
h : ¬α ≤ β
⊢ ¬α + γ ≤ β + γ
Module: Mathlib.SetTheory.Cardinal.Arithmetic

Goal state before:
pp: case inl
κ₁ κ₂ μ₁ μ₂ : Cardinal.{u_1}
hκ : κ₁ < κ₂
hμ : μ₁ < μ₂
hinf : ℵ₀ ≤ κ₂ + μ₂
⊢ κ₁ + μ₁ < κ₂ + μ₂

Tactic:
refine add_lt_of_lt hinf ?_ ?_

Goal state after:
case inl.refine_1
κ₁ κ₂ μ₁ μ₂ : Cardinal.{u_1}
hκ : κ₁ < κ₂
hμ : μ₁ < μ₂
hinf : ℵ₀ ≤ κ₂ + μ₂
⊢ κ₁ < κ₂ + μ₂

case inl.refine_2
κ₁ κ₂ μ₁ μ₂ : Cardinal.{u_1}
hκ : κ₁ < κ₂
hμ : μ₁ < μ₂
hinf : ℵ₀ ≤ κ₂ + μ₂
⊢ μ₁ < κ₂ + μ₂
Module: Mathlib.SetTheory.Ordinal.FundamentalSequence

Goal state before:
pp: case neg
a : Ordinal.{u}
ι : Type u
f : ι → Ordinal.{u}
hf : lsub f = a
hι : #ι = a.cof
r : ι → ι → Prop
wo : IsWellOrder ι r
hr : (#ι).ord = type r
r' : { i // ∀ (j : ι), r j i → f j < f i } → { i // ∀ (j : ι), r j i → f j < f i } → Prop :=
  Subrel r fun i ↦ ∀ (j : ι), r j i → f j < f i
hrr' : r' ↪r r := Subrel.relEmbedding r fun i ↦ ∀ (j : ι), r j i → f j < f i
this : IsWellOrder { i // ∀ (j : ι), r j i → f j < f i } r'
i : ι
h : ∃ j, r j i ∧ f i ≤ f j
hji : r (⋯.min (fun x ↦ r x i ∧ f i ≤ f x) h) i
hij : f i ≤ f (⋯.min (fun x ↦ r x i ∧ f i ≤ f x) h)
⊢ ∃ i', ∃ (hi' : i' < type r'), f i ≤ bfamilyOfFamily' r' (fun i ↦ f ↑i) i' hi'

Tactic:
refine ⟨typein r' ⟨_, fun k hkj => lt_of_lt_of_le ?_ hij⟩, typein_lt_type _ _, ?_⟩

Goal state after:
case neg.refine_1
a : Ordinal.{u}
ι : Type u
f : ι → Ordinal.{u}
hf : lsub f = a
hι : #ι = a.cof
r : ι → ι → Prop
wo : IsWellOrder ι r
hr : (#ι).ord = type r
r' : { i // ∀ (j : ι), r j i → f j < f i } → { i // ∀ (j : ι), r j i → f j < f i } → Prop :=
  Subrel r fun i ↦ ∀ (j : ι), r j i → f j < f i
hrr' : r' ↪r r := Subrel.relEmbedding r fun i ↦ ∀ (j : ι), r j i → f j < f i
this : IsWellOrder { i // ∀ (j : ι), r j i → f j < f i } r'
i : ι
h : ∃ j, r j i ∧ f i ≤ f j
hji : r (⋯.min (fun x ↦ r x i ∧ f i ≤ f x) h) i
hij : f i ≤ f (⋯.min (fun x ↦ r x i ∧ f i ≤ f x) h)
k : ι
hkj : r k (⋯.min (fun x ↦ r x i ∧ f i ≤ f x) h)
⊢ f k < f i

case neg.refine_2
a : Ordinal.{u}
ι : Type u
f : ι → Ordinal.{u}
hf : lsub f = a
hι : #ι = a.cof
r : ι → ι → Prop
wo : IsWellOrder ι r
hr : (#ι).ord = type r
r' : { i // ∀ (j : ι), r j i → f j < f i } → { i // ∀ (j : ι), r j i → f j < f i } → Prop :=
  Subrel r fun i ↦ ∀ (j : ι), r j i → f j < f i
hrr' : r' ↪r r := Subrel.relEmbedding r fun i ↦ ∀ (j : ι), r j i → f j < f i
this : IsWellOrder { i // ∀ (j : ι), r j i → f j < f i } r'
i : ι
h : ∃ j, r j i ∧ f i ≤ f j
hji : r (⋯.min (fun x ↦ r x i ∧ f i ≤ f x) h) i
hij : f i ≤ f (⋯.min (fun x ↦ r x i ∧ f i ≤ f x) h)
⊢ f i ≤ bfamilyOfFamily' r' (fun i ↦ f ↑i) ((typein r').toRelEmbedding ⟨⋯.min (fun x ↦ r x i ∧ f i ≤ f x) h, ⋯⟩) ⋯
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) < #β
b : β
⊢ ∃ a, b ∈ f a

Tactic:
simpa using (w.ge :) (Set.mem_univ b)

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

Goal state before:
pp: x : Cardinal.{u_1}
h : x ≠ 0
⊢ (sum fun n ↦ x ^ n) = max ℵ₀ x

Tactic:
by
  have := nonempty_out h
  conv_lhs => rw [← x.mk_out, ← mk_list_eq_sum_pow, mk_list_eq_max, mk_out]

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

Goal state before:
pp: c : Cardinal.{u_1}
hc : c.IsSingular
⊢ IsSuccLimit c

Tactic:
Cardinal.isSuccLimit_iff,

Goal state after:
c : Cardinal.{u_1}
hc : c.IsSingular
⊢ c ≠ 0 ∧ IsSuccPrelimit c
Module: Mathlib.SetTheory.Cardinal.Arithmetic

Goal state before:
pp: α : Type u_1
β : Type u_2
s : Set α
f : ↑s ↪ β
h : Nonempty (↑sᶜ ≃ ↑(range ⇑f)ᶜ)
⊢ ∃ g, ∀ (x : ↑s), g ↑x = f x

Tactic:
by
  classical
  have := h; obtain ⟨g⟩ := this
  let h : α ≃ β :=
    (Set.sumCompl (s : Set α)).symm.trans
      ((sumCongr (Equiv.ofInjective f f.2) g).trans (Set.sumCompl (range f)))
  refine ⟨h, ?_⟩; rintro ⟨x, hx⟩; simp [h, Set.sumCompl_symm_apply_of_mem, hx]

Goal state after:
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 ι
a : (i_1 : ι) → i_1 ∈ i :: l → α i_1
⊢ (List.Pi.head fun x1 x2 ↦ ⟦a x1 x2⟧).liftOn₂ (listChoice fun j hj ↦ (fun x1 x2 ↦ ⟦a x1 x2⟧) j ⋯)
      (fun x1 x2 ↦ ⟦List.Pi.cons i l x1 x2⟧) ⋯ =
    ⟦a⟧

Tactic:
listChoice_mk

Goal state after:
ι : Type u_1
inst✝ : DecidableEq ι
α : ι → Sort u_2
S : (i : ι) → Setoid (α i)
l✝ : List ι
i : ι
l : List ι
a : (i_1 : ι) → i_1 ∈ i :: l → α i_1
⊢ (List.Pi.head fun x1 x2 ↦ ⟦a x1 x2⟧).liftOn₂ ⟦fun j hj ↦ a j ⋯⟧ (fun x1 x2 ↦ ⟦List.Pi.cons i l x1 x2⟧) ⋯ = ⟦a⟧
Module: Mathlib.Data.DFinsupp.BigOperators

Goal state before:
pp: ι : Type u
γ : Type w
β : ι → Type v
inst✝³ : DecidableEq ι
inst✝² : (i : ι) → Zero (β i)
inst✝¹ : (i : ι) → (x : β i) → Decidable (x ≠ 0)
inst✝ : CommMonoid γ
f : Π₀ (i : ι), β i
g : (i : ι) → β i → γ
s : Finset ι
hs : f.support ⊆ s
map_zero : ∀ i ∈ s, g i 0 = 1
i : ι
hi : i ∈ s
hi' : i ∉ f.support
⊢ g i (f i) = 1

Tactic:
simp only [DFinsupp.mem_support_toFun, ne_eq, not_not] at hi'

Goal state after:
ι : Type u
γ : Type w
β : ι → Type v
inst✝³ : DecidableEq ι
inst✝² : (i : ι) → Zero (β i)
inst✝¹ : (i : ι) → (x : β i) → Decidable (x ≠ 0)
inst✝ : CommMonoid γ
f : Π₀ (i : ι), β i
g : (i : ι) → β i → γ
s : Finset ι
hs : f.support ⊆ s
map_zero : ∀ i ∈ s, g i 0 = 1
i : ι
hi : i ∈ s
hi' : f i = 0
⊢ g i (f i) = 1
Module: Mathlib.Data.Fintype.Quotient

Goal state before:
pp: ι : Type u_1
inst✝¹ : Fintype ι
inst✝ : DecidableEq ι
α : ι → Sort u_2
S : (i : ι) → Setoid (α i)
a : (i : ι) → α i
l : List ι
hl : ⟦l⟧ = Finset.univ.val
⊢ ({
            toFun := fun a ↦
              Quotient.hrecOn (motive := fun x ↦
                (∀ (i : ι), i ∈ x) → Quotient (Subtype.instSetoid_mathlib fun l ↦ ∀ (i : ι), i ∈ l)) (↑a)
                (fun a h ↦ ⟦⟨a, ⋯⟩⟧) ⋯ ⋯,
            invFun := fun a ↦ a.liftOn (fun a ↦ ⟨⟦↑a⟧, ⋯⟩) ⋯, left_inv := ⋯, right_inv := ⋯ }
          ⟨⟦l⟧, ⋯⟩).liftOn
      (fun l ↦ Quotient.map (fun a i ↦ a i ⋯) ⋯ (listChoice fun i x ↦ ⟦a i⟧)) ⋯ =
    ⟦a⟧

Tactic:
listChoice_mk

Goal state after:
ι : Type u_1
inst✝¹ : Fintype ι
inst✝ : DecidableEq ι
α : ι → Sort u_2
S : (i : ι) → Setoid (α i)
a : (i : ι) → α i
l : List ι
hl : ⟦l⟧ = Finset.univ.val
⊢ ({
            toFun := fun a ↦
              Quotient.hrecOn (motive := fun x ↦
                (∀ (i : ι), i ∈ x) → Quotient (Subtype.instSetoid_mathlib fun l ↦ ∀ (i : ι), i ∈ l)) (↑a)
                (fun a h ↦ ⟦⟨a, ⋯⟩⟧) ⋯ ⋯,
            invFun := fun a ↦ a.liftOn (fun a ↦ ⟨⟦↑a⟧, ⋯⟩) ⋯, left_inv := ⋯, right_inv := ⋯ }
          ⟨⟦l⟧, ⋯⟩).liftOn
      (fun l ↦ Quotient.map (fun a i ↦ a i ⋯) ⋯ ⟦fun x1 x2 ↦ a x1⟧) ⋯ =
    ⟦a⟧
Module: Mathlib.Data.Finsupp.ToDFinsupp

Goal state before:
pp: case neg
ι : Type u_1
η : ι → Type u_4
N : Type u_5
inst✝¹ : DecidableEq ι
inst✝ : Zero N
n : N
i : ι
a : η i
j : ι
b : η j
h : ¬i = j
H : ⟨i, a⟩ ≠ ⟨j, b⟩
⊢ (if ⟨i, a⟩ = ⟨j, b⟩ then n else 0) = 0

Tactic:
if_neg H

Goal state after:
case neg
ι : Type u_1
η : ι → Type u_4
N : Type u_5
inst✝¹ : DecidableEq ι
inst✝ : Zero N
n : N
i : ι
a : η i
j : ι
b : η j
h : ¬i = j
H : ⟨i, a⟩ ≠ ⟨j, b⟩
⊢ 0 = 0
Module: Mathlib.Data.DFinsupp.Defs

Goal state before:
pp: case some
ι : Type u
α : Option ι → Type v
inst✝¹ : DecidableEq ι
inst✝ : (i : Option ι) → Zero (α i)
i : ι
x : α (some i)
j : ι
⊢ (single i x) j = (single (some i) x) (some j)

Tactic:
obtain rfl | hij := Decidable.eq_or_ne j i

Goal state after:
case some.inl
ι : Type u
α : Option ι → Type v
inst✝¹ : DecidableEq ι
inst✝ : (i : Option ι) → Zero (α i)
j : ι
x : α (some j)
⊢ (single j x) j = (single (some j) x) (some j)

case some.inr
ι : Type u
α : Option ι → Type v
inst✝¹ : DecidableEq ι
inst✝ : (i : Option ι) → Zero (α i)
i : ι
x : α (some i)
j : ι
hij : j ≠ i
⊢ (single i x) j = (single (some i) x) (some j)
Module: Mathlib.LinearAlgebra.LinearIndependent.Lemmas

Goal state before:
pp: ι : Type u'
ι' : Type u_1
R : Type u_2
M : Type u_4
M' : Type u_5
inst✝⁴ : Semiring R
inst✝³ : AddCommMonoid M
inst✝² : AddCommMonoid M'
inst✝¹ : Module R M
inst✝ : Module R M'
v : ι → M
v' : ι' → M'
hv : LinearIndependent R v
hv' : LinearIndependent R v'
⊢ LinearIndependent R (Sum.elim (⇑(inl R M M') ∘ v) (⇑(inr R M M') ∘ v'))

Tactic:
by
  have : linearCombination R (Sum.elim (inl R M M' ∘ v) (inr R M M' ∘ v')) =
      .prodMap (linearCombination R v) (linearCombination R v') ∘ₗ
      (sumFinsuppLEquivProdFinsupp R).toLinearMap := by ext (_ | _) <;> simp
  rw [LinearIndependent, this]
  simpa [LinearMap.coe_prodMap] using ⟨hv, hv'⟩

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
⊢ LinearIndepOn R ![x, y] (insert 0 ↑{1}) ↔ ∀ (s t : R), s • x + t • y = 0 → s = 0 ∧ t = 0

Tactic:
Finset.coe_singleton,

Goal state after:
R : Type u_2
M : Type u_4
inst✝² : Ring R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
x y : M
⊢ LinearIndepOn R ![x, y] {0, 1} ↔ ∀ (s t : R), s • x + t • y = 0 → s = 0 ∧ t = 0
Module: Mathlib.Algebra.Group.AddChar

Goal state before:
pp: A : Type u_1
M : Type u_2
inst✝¹ : AddCommGroup A
inst✝ : CommMonoid M
ψ : AddChar A M
⊢ ψ.compAddMonoidHom negAddMonoidHom * ψ = 1

Tactic:
ext1 x

Goal state after:
A : Type u_1
M : Type u_2
inst✝¹ : AddCommGroup A
inst✝ : CommMonoid M
ψ : AddChar A M
x : A
⊢ (ψ.compAddMonoidHom negAddMonoidHom * ψ) x = 1 x
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
x y : V
hx : x ≠ 0
⊢ LinearIndepOn K ![x, y] (insert 0 ↑{1}) ↔ ∀ (a : K), a • x ≠ y

Tactic:
Finset.coe_singleton,

Goal state after:
K : Type u_3
V : Type u
inst✝² : DivisionRing K
inst✝¹ : AddCommGroup V
inst✝ : Module K V
x y : V
hx : x ≠ 0
⊢ LinearIndepOn K ![x, y] {0, 1} ↔ ∀ (a : K), a • x ≠ y
Module: Mathlib.Algebra.Group.Pointwise.Set.ListOfFn

Goal state before:
pp: α : Type u_1
inst✝ : Monoid α
n : ℕ
a : α
s : Fin n → Set α
⊢ a ∈ (List.ofFn s).prod ↔ ∃ f, (List.ofFn fun i ↦ ↑(f i)).prod = a

Tactic:
induction n generalizing a with

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

Goal state before:
pp: ι : Type u'
ι' : Type u_1
R : Type u_2
K : Type u_3
s✝ : Set ι
M : Type u_4
M' : Type u_5
V : Type u
inst✝² : DivisionRing K
inst✝¹ : AddCommGroup V
inst✝ : Module K V
v : ι → V
s t : Set V
x y : V
n : ℕ
x✝ : { s // LinearIndependent K s }
⊢ (fun s ↦ ⟨Fin.cons ↑s.snd ↑s.fst, ⋯⟩) ((fun s ↦ ⟨⟨Fin.tail ↑s, ⋯⟩, ⟨↑s 0, ⋯⟩⟩) x✝) = x✝

Tactic:
simp only [Fin.cons_self_tail, Subtype.coe_eta]

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
f : Fin 2 → V
⊢ LinearIndependent K (Fin.tail f) ∧ f 0 ∉ span K (range (Fin.tail f)) ↔ f 1 ≠ 0 ∧ ∀ (a : K), a • f 1 ≠ f 0

Tactic:
linearIndependent_unique_iff,

Goal state after:
K : Type u_3
V : Type u
inst✝² : DivisionRing K
inst✝¹ : AddCommGroup V
inst✝ : Module K V
f : Fin 2 → V
⊢ Fin.tail f default ≠ 0 ∧ f 0 ∉ span K (range (Fin.tail f)) ↔ f 1 ≠ 0 ∧ ∀ (a : K), a • f 1 ≠ f 0