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

Goal state before:
pp: A : Type u_1
inst✝ : Monoid A
a : A → Finset (A × A)
ha : ∀ {n : A} {a_1 : A × A}, a_1 ∈ a n ↔ a_1.1 * a_1.2 = n
b : A → Finset (A × A)
hb : ∀ {n : A} {a : A × A}, a ∈ b n ↔ a.1 * a.2 = n
⊢ { mulAntidiagonal := a, mem_mulAntidiagonal := ha } = { mulAntidiagonal := b, mem_mulAntidiagonal := hb }

Tactic:
congr with n xy

Goal state after:
A : Type u_1
inst✝ : Monoid A
a : A → Finset (A × A)
ha : ∀ {n : A} {a_1 : A × A}, a_1 ∈ a n ↔ a_1.1 * a_1.2 = n
b : A → Finset (A × A)
hb : ∀ {n : A} {a : A × A}, a ∈ b n ↔ a.1 * a.2 = n
n : A
xy : A × A
⊢ xy ∈ a n ↔ xy ∈ b n
Module: Mathlib.Algebra.Order.Antidiag.Prod

Goal state before:
pp: A✝ : Type u_1
A : Type u_2
inst✝¹ : AddMonoid A
inst✝ : HasAntidiagonal A
a : Multiplicative A
x✝¹ x✝ : A × A
h : (fun p ↦ (ofAdd p.1, ofAdd p.2)) x✝¹ = (fun p ↦ (ofAdd p.1, ofAdd p.2)) x✝
⊢ x✝¹ = x✝

Tactic:
by aesop

Goal state after:
Module: Mathlib.Algebra.Order.Antidiag.Prod

Goal state before:
pp: A✝ : Type u_1
A : Type u_2
inst✝¹ : AddMonoid A
inst✝ : HasAntidiagonal A
a : Multiplicative A
p : Multiplicative A × Multiplicative A
⊢ p ∈ map { toFun := fun p ↦ (ofAdd p.1, ofAdd p.2), inj' := ⋯ } (antidiagonal (toAdd a)) ↔ p.1 * p.2 = a

Tactic:
by aesop

Goal state after:
Module: Mathlib.Algebra.BigOperators.Intervals

Goal state before:
pp: M : Type u_4
m n : ℕ
inst✝ : CommGroup M
hmn : m ≤ n
f : ℕ → M
⊢ ∏ i ∈ Icc m n, f (i + 1) / f i = f (n + 1) / f m

Tactic:
rw [← Finset.Ico_add_one_right_eq_Icc, prod_Ico_div]

Goal state after:
case hmn
M : Type u_4
m n : ℕ
inst✝ : CommGroup M
hmn : m ≤ n
f : ℕ → M
⊢ m ≤ n + 1
Module: Mathlib.RingTheory.Ideal.Maximal

Goal state before:
pp: α : Type u
inst✝ : Semiring α
I J : Ideal α
hI : I.IsMaximal
hJ : J ≠ ⊤
⊢ I = J → I ≤ J

Tactic:
by aesop

Goal state after:
Module: Mathlib.RingTheory.Ideal.Maximal

Goal state before:
pp: α : Type u
inst✝ : CommSemiring α
s : Set α
hs : span s = ⊤
I : Ideal α
hI : I ≠ ⊤
M : Ideal α
hM : M.IsMaximal
le : I ≤ M
this : ¬s ⊆ ↑M
⊢ ∃ r ∈ s, Disjoint ↑I ↑(Submonoid.powers r)

Tactic:
Set.not_subset

Goal state after:
α : Type u
inst✝ : CommSemiring α
s : Set α
hs : span s = ⊤
I : Ideal α
hI : I ≠ ⊤
M : Ideal α
hM : M.IsMaximal
le : I ≤ M
this : ∃ a ∈ s, a ∉ ↑M
⊢ ∃ r ∈ s, Disjoint ↑I ↑(Submonoid.powers r)
Module: Mathlib.RingTheory.Ideal.Quotient.Basic

Goal state before:
pp: R : Type u_3
inst✝² : Ring R
I : Ideal R
inst✝¹ : Finite ↥I
inst✝ : Finite (R ⧸ I)
⊢ Finite R

Tactic:
by
  rw [finite_iff_ideal_quotient]; constructor <;> assumption

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

Goal state before:
pp: R : Type u_5
inst✝¹ : CommSemiring R
inst✝ : Nontrivial R
⊢ ¬IsField R ↔ ∃ p, p ≠ ⊥ ∧ p.IsPrime

Tactic:
refine ⟨fun h ↦ ?_, fun ⟨I, h_bot, h_top⟩ ↦ not_isField_of_ne_of_ne h_bot h_top.ne_top⟩
  obtain ⟨I, hI, hIm⟩ := exists_maximal_of_not_isField h
  exact ⟨I, hI, hIm.isPrime⟩

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

Goal state before:
pp: α : Type u
p : α → Prop
f g : Filter α
⊢ (∃ᶠ (x : α) in f ⊔ g, p x) ↔ (∃ᶠ (x : α) in f, p x) ∨ ∃ᶠ (x : α) in g, p x

Tactic:
simp only [Filter.Frequently, eventually_sup, not_and_or]

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

Goal state before:
pp: case a
α : Type u_1
β : Type u_2
f : α → β
F : Filter α
G : Filter β
U : Set β
V : Set α
V_in : V ∈ F
W : Set α
h : f ⁻¹' U = V ∩ W
Z : Set β
Z_in : Z ∈ G
hZ : f ⁻¹' Z ⊆ W
⊢ f '' V ∩ Z ⊆ U

Tactic:
calc
      f '' V ∩ Z = f '' (V ∩ f ⁻¹' Z) := by rw [image_inter_preimage]
      _ ⊆ f '' (V ∩ W) := by gcongr
      _ = f '' f ⁻¹' U := by rw [h]
      _ ⊆ U := image_preimage_subset f U

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

Goal state before:
pp: case refine_1
α : Type u_1
β : Type u_2
s : Set α
m : α → β
hm : InjOn (map m) (Iic (𝓟 s))
x : α
hx : x ∈ s
y : α
hy : y ∈ s
hxy : m x = m y
⊢ x = y

pp: case refine_2
α : Type u_1
β : Type u_2
s : Set α
m : α → β
hm : InjOn m s
F : Filter α
hF : F ∈ Iic (𝓟 s)
G : Filter α
hG : G ∈ Iic (𝓟 s)
⊢ map m F = map m G → F = G

Tactic:
· rwa [← pure_injective.eq_iff, ← map_pure, ← map_pure, hm.eq_iff, pure_injective.eq_iff]
      at hxy <;> rwa [mem_Iic, pure_le_principal]

Goal state after:
case refine_2
α : Type u_1
β : Type u_2
s : Set α
m : α → β
hm : InjOn m s
F : Filter α
hF : F ∈ Iic (𝓟 s)
G : Filter α
hG : G ∈ Iic (𝓟 s)
⊢ map m F = map m G → F = G
Module: Mathlib.Algebra.Group.Shrink

Goal state before:
pp: α : Type u_2
inst✝¹ : Small.{v, u_2} α
inst✝ : Inv α
x : Shrink.{v, u_2} α
⊢ (equivShrink α).symm x⁻¹ = ((equivShrink α).symm x)⁻¹

Tactic:
simp [Equiv.inv_def]

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

Goal state before:
pp: α : Type u_2
inst✝¹ : Small.{v, u_2} α
inst✝ : Inv α
x : α
⊢ (equivShrink α) x⁻¹ = ((equivShrink α) x)⁻¹

Tactic:
simp [Equiv.inv_def]

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 : Type u_3
P : Type u_4
inst✝⁴ : Semiring S
inst✝³ : AddCommMonoid P
inst✝² : Module S P
σ : R →+* S
inst✝¹ : RingHomSurjective σ
inst✝ : Module.Finite R M
f : M →ₛₗ[σ] P
⊢ (map f ⊤).FG

Tactic:
exact Module.Finite.fg_top.map f

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
M' : Submodule R M
N : ℕ →o Submodule R M
H : iSup ⇑N = M'
S : Finset M
hS : span R ↑S = M'
s : ↥S
⊢ ↑s ∈ ⨆ k, N k

Tactic:
by simpa [H, ← hS] using subset_span s.prop

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

Goal state before:
pp: α : Type u_1
β : Type u_2
a : α
b₁ b₂ : β
inst✝⁵ : GroupWithZero α
inst✝⁴ : Preorder α
inst✝³ : Preorder β
inst✝² : MulAction α β
inst✝¹ : PosSMulMono α β
inst✝ : PosSMulReflectLE α β
ha : 0 < a
⊢ a⁻¹ • b₁ ≤ b₂ ↔ b₁ ≤ a • b₂

Tactic:
← smul_le_smul_iff_of_pos_left ha,

Goal state after:
α : Type u_1
β : Type u_2
a : α
b₁ b₂ : β
inst✝⁵ : GroupWithZero α
inst✝⁴ : Preorder α
inst✝³ : Preorder β
inst✝² : MulAction α β
inst✝¹ : PosSMulMono α β
inst✝ : PosSMulReflectLE α β
ha : 0 < a
⊢ a • a⁻¹ • b₁ ≤ a • b₂ ↔ b₁ ≤ a • b₂
Module: Mathlib.RingTheory.Finiteness.Basic

Goal state before:
pp: case a
R : Type u_1
M : Type u_2
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
M' : Submodule R M
N : ℕ →o Submodule R M
H : iSup ⇑N = M'
S : Finset M
hS : span R ↑S = M'
f : ↥S → ℕ
hf : ∀ (s : ↥S), ↑s ∈ N (f s)
⊢ N (S.attach.sup f) ≤ M'

Tactic:
← H

Goal state after:
case a
R : Type u_1
M : Type u_2
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
M' : Submodule R M
N : ℕ →o Submodule R M
H : iSup ⇑N = M'
S : Finset M
hS : span R ↑S = M'
f : ↥S → ℕ
hf : ∀ (s : ↥S), ↑s ∈ N (f s)
⊢ N (S.attach.sup f) ≤ iSup ⇑N
Module: Mathlib.Algebra.Order.Module.Defs

Goal state before:
pp: α : Type u_1
β : Type u_2
a : α
b₁ b₂ : β
inst✝⁵ : GroupWithZero α
inst✝⁴ : Preorder α
inst✝³ : Preorder β
inst✝² : MulAction α β
inst✝¹ : PosSMulMono α β
inst✝ : PosSMulReflectLE α β
ha : 0 < a
⊢ b₁ ≤ a⁻¹ • b₂ ↔ a • b₁ ≤ b₂

Tactic:
← smul_le_smul_iff_of_pos_left ha,

Goal state after:
α : Type u_1
β : Type u_2
a : α
b₁ b₂ : β
inst✝⁵ : GroupWithZero α
inst✝⁴ : Preorder α
inst✝³ : Preorder β
inst✝² : MulAction α β
inst✝¹ : PosSMulMono α β
inst✝ : PosSMulReflectLE α β
ha : 0 < a
⊢ a • b₁ ≤ a • a⁻¹ • b₂ ↔ a • b₁ ≤ b₂
Module: Mathlib.Algebra.Order.Module.Defs

Goal state before:
pp: α : Type u_1
β : Type u_2
a a₁✝ a₂✝ : α
b b₁ b₂ : β
inst✝⁶ : Preorder α
inst✝⁵ : Monoid α
inst✝⁴ : AddCommGroup β
inst✝³ : PartialOrder β
inst✝² : IsOrderedAddMonoid β
inst✝¹ : DistribMulAction α β
inst✝ : SMulPosStrictMono α β
_b : βᵒᵈ
hb : 0 < _b
a₁ a₂ : α
ha : a₁ < a₂
⊢ a₁ • _b < a₂ • _b

Tactic:
rw [← neg_lt_neg_iff, ← smul_neg, ← smul_neg]

Goal state after:
α : Type u_1
β : Type u_2
a a₁✝ a₂✝ : α
b b₁ b₂ : β
inst✝⁶ : Preorder α
inst✝⁵ : Monoid α
inst✝⁴ : AddCommGroup β
inst✝³ : PartialOrder β
inst✝² : IsOrderedAddMonoid β
inst✝¹ : DistribMulAction α β
inst✝ : SMulPosStrictMono α β
_b : βᵒᵈ
hb : 0 < _b
a₁ a₂ : α
ha : a₁ < a₂
⊢ a₂ • -_b < a₁ • -_b
Module: Mathlib.Order.DirSupClosed

Goal state before:
pp: α : Type u_1
s t : Set α
D : Set (Set α)
inst✝ : Preorder α
hDL : IsLowerSet D
hs : DirSupClosedOn D s
ht : DirSupClosedOn D t
d : Set α
⊢ d ∈ D → d ⊆ s ∪ t → d.Nonempty → DirectedOn (fun x1 x2 ↦ x1 ≤ x2) d → ∀ ⦃a : α⦄, IsLUB d a → a ∈ s ∪ t

Tactic:
hD

Goal state after:
α : Type u_1
s t : Set α
D : Set (Set α)
inst✝ : Preorder α
hDL : IsLowerSet D
hs : DirSupClosedOn D s
ht : DirSupClosedOn D t
d : Set α
hD : d ∈ D
⊢ d ⊆ s ∪ t → d.Nonempty → DirectedOn (fun x1 x2 ↦ x1 ≤ x2) d → ∀ ⦃a : α⦄, IsLUB d a → a ∈ s ∪ t
Module: Mathlib.Order.DirSupClosed

Goal state before:
pp: α : Type u_1
s : Set α
inst✝ : Preorder α
hs : DirSupClosed s
a b : α
h : AntisymmRel (fun x1 x2 ↦ x1 ≤ x2) a b
ha : a ∈ s
⊢ b ∈ s

Tactic:
apply hs (singleton_subset_iff.2 ha) ⟨a, rfl⟩ (directedOn_singleton a)
  rw [← isLUB_congr_of_antisymmRel h]
  exact isLUB_singleton

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

Goal state before:
pp: o : Ordinal.{u_1}
h0 : 0 < o
a : o.ToType
⊢ (enum fun x1 x2 ↦ x1 < x2) ⟨0, ⋯⟩ ≤ a

Tactic:
← not_lt

Goal state after:
o : Ordinal.{u_1}
h0 : 0 < o
a : o.ToType
⊢ ¬a < (enum fun x1 x2 ↦ x1 < x2) ⟨0, ⋯⟩
Module: Mathlib.SetTheory.Ordinal.Family

Goal state before:
pp: o : Ordinal.{u_3}
f : (a : Ordinal.{u_3}) → a < o → Ordinal.{max u_4 u_3}
⊢ o.bsup f = 0 ↔ ∀ (i : Ordinal.{u_3}) (hi : i < o), f i hi = 0

Tactic:
by
  refine
    ⟨fun h i hi => ?_, fun h =>
      le_antisymm (bsup_le fun i hi => nonpos_iff_eq_zero.2 (h i hi)) zero_le⟩
  rw [← nonpos_iff_eq_zero, ← h]
  exact le_bsup f i hi

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

Goal state before:
pp: ι : Type u_3
f : ι → Ordinal.{max u_4 u_3}
⊢ iSup f = lsub f ∨ succ (iSup f) = lsub f

Tactic:
rcases eq_or_lt_of_le (iSup_le_lsub f) with h | h
  · exact Or.inl h
  · exact Or.inr ((succ_le_of_lt h).antisymm (lsub_le_succ_iSup f))

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

Goal state before:
pp: o : Ordinal.{u_3}
⊢ iSup ⇑(typein fun x1 x2 ↦ x1 < x2).toRelEmbedding = o

Tactic:
rw [← csSup_Iic (a := o), iSup, PrincipalSeg.range_eq]

Goal state after:
o : Ordinal.{u_3}
⊢ sSup {b | b < (typein fun x1 x2 ↦ x1 < x2).top} = sSup (Iic o)
Module: Mathlib.SetTheory.Cardinal.Aleph

Goal state before:
pp: ⊢ IsNormal ⇑preOmega

Tactic:
rw [isNormal_iff]
  refine ⟨preOmega_strictMono, fun o ho a ha ↦
    (preOmega_le_of_forall_lt (isInitial_ord _) fun b hb ↦ ?_).trans (ord_card_le a)⟩
  rw [← (isInitial_ord _).card_lt_card, card_ord]
  apply lt_of_lt_of_le _ (card_le_card <| ha _ (ho.succ_lt hb))
  rw [(isInitial_preOmega _).card_lt_card, preOmega_lt_preOmega]
  exact lt_succ b

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

Goal state before:
pp: ⊢ IsNormal preBeth

Tactic:
rw [isNormal_iff]
  refine ⟨preBeth_strictMono, fun o ho ↦ ?_⟩
  simp [preBeth_limit ho.isSuccPrelimit, ciSup_le_iff' bddAbove_of_small]

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

Goal state before:
pp: case right.left
a b : Cardinal.{u_1}
h : a * b = a
ha : ℵ₀ ≤ a
this : a ≠ 0
⊢ b ≤ a

Tactic:
← not_lt

Goal state after:
case right.left
a b : Cardinal.{u_1}
h : a * b = a
ha : ℵ₀ ≤ a
this : a ≠ 0
⊢ ¬a < b
Module: Mathlib.SetTheory.Cardinal.Arithmetic

Goal state before:
pp: n m : ℕ
h2a : 1 ≤ n
hb : 1 ≤ m
h : n * m = n
⊢ m ≤ 1

Tactic:
← not_lt

Goal state after:
n m : ℕ
h2a : 1 ≤ n
hb : 1 ≤ m
h : n * m = n
⊢ ¬1 < m
Module: Mathlib.SetTheory.Cardinal.Arithmetic

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

Tactic:
← not_lt

Goal state after:
case a
a b c : Cardinal.{u_1}
h : a + b = c
ha : a < c
hc : ℵ₀ ≤ c
⊢ ¬b < c
Module: Mathlib.SetTheory.Cardinal.Arithmetic

Goal state before:
pp: case right
a b : Cardinal.{u_1}
h : a + b = a
ha : ℵ₀ ≤ a
⊢ b ≤ a

Tactic:
← not_lt

Goal state after:
case right
a b : Cardinal.{u_1}
h : a + b = a
ha : ℵ₀ ≤ a
⊢ ¬a < b
Module: Mathlib.SetTheory.Ordinal.Principal

Goal state before:
pp: case a
a b : Ordinal.{u}
ha : a ≠ 0
hb : IsPrincipal (fun x1 x2 ↦ x1 * x2) b
hb₂ : 2 < b
⊢ a * b ≤ b ^ succ (log b a)

pp: case a
a b : Ordinal.{u}
ha : a ≠ 0
hb : IsPrincipal (fun x1 x2 ↦ x1 * x2) b
hb₂ : 2 < b
⊢ b ^ succ (log b a) ≤ a * b

Tactic:
· have hbl := isSuccLimit_of_isPrincipal_mul hb₂ hb
    rw [(isNormal_mul_right (pos_iff_ne_zero.2 ha)).apply_of_isSuccLimit hbl,
      Ordinal.iSup_le_iff]
    intro ⟨c, hcb⟩
    have hb₁ : 1 < b := one_lt_two.trans hb₂
    have hbo₀ : b ^ log b a ≠ 0 := pos_iff_ne_zero.1 (opow_pos _ (zero_lt_one.trans hb₁))
    apply (mul_le_mul_left (le_of_lt (lt_mul_succ_div a hbo₀)) c).trans
    rw [mul_assoc, opow_succ]
    gcongr
    refine (hb (hbl.succ_lt ?_) hcb).le
    rw [← lt_mul_iff_div_lt hbo₀, ← opow_succ]
    exact lt_opow_succ_log_self hb₁ _

Goal state after:
case a
a b : Ordinal.{u}
ha : a ≠ 0
hb : IsPrincipal (fun x1 x2 ↦ x1 * x2) b
hb₂ : 2 < b
⊢ b ^ succ (log b a) ≤ a * b
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]
    exact fun i ↦ (f i).2

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

Goal state before:
pp: a o : Ordinal.{u_1}
f : ↑(Iio a) → ↑(Iio o)
hf : IsFundamentalSeq f
ha : 1 < a
⊢ ord 1 < a

Tactic:
ord_one

Goal state after:
a o : Ordinal.{u_1}
f : ↑(Iio a) → ↑(Iio o)
hf : IsFundamentalSeq f
ha : 1 < a
⊢ 1 < a
Module: Mathlib.SetTheory.Cardinal.Arithmetic

Goal state before:
pp: ι : Type u
f : ι → Cardinal.{v}
inst✝ : Nonempty ι
hf : BddAbove (range f)
c : Cardinal.{v}
⊢ (⨆ i, f i) + c = ⨆ i, f i + c

Tactic:
have (i : ι) : f i + c ≤ (⨆ i, f i) + c := by grw [le_ciSup hf i]
  refine le_antisymm ?_ (ciSup_le' this)
  have bdd : BddAbove (range (f · + c)) := ⟨_, forall_mem_range.mpr this⟩
  obtain hs | hs := lt_or_ge (⨆ i, f i) ℵ₀
  · obtain ⟨i, hi⟩ := exists_eq_ciSup_of_not_isSuccLimit hf (not_isSuccLimit_of_lt_aleph0 hs)
    exact hi ▸ le_ciSup bdd i
  rw [add_eq_max hs, max_le_iff]
  exact ⟨ciSup_mono bdd fun i ↦ self_le_add_right _ c,
    (self_le_add_left _ _).trans (le_ciSup bdd <| Classical.arbitrary ι)⟩

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

Goal state before:
pp: case refine_1
o : Ordinal.{u}
⊢ 1 ≤ ord 1

Tactic:
ord_one

Goal state after:
case refine_1
o : Ordinal.{u}
⊢ 1 ≤ 1
Module: Mathlib.SetTheory.Ordinal.FundamentalSequence

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

Tactic:
suffices h : ∃ o f, IsFundamentalSequence a o f by
    rcases h with ⟨o, f, hf⟩
    exact ⟨_, hf.ord_cof⟩
  rcases exists_lsub_cof a with ⟨ι, f, hf, hι⟩
  rcases ord_eq ι with ⟨r, wo, hr⟩
  let r' := Subrel r fun i ↦ ∀ j, r j i → f j < f i
  let hrr' : r' ↪r r := Subrel.relEmbedding _ _
  have := hrr'.isWellOrder
  refine
    ⟨_, _, hrr'.ordinal_type_le.trans ?_, @fun i j _ h _ => (enum r' ⟨j, h⟩).prop _ ?_,
      le_antisymm (blsub_le fun i hi => lsub_le_iff.1 hf.le _) ?_⟩
  · rw [← hι, hr]
  · change r (hrr'.1 _) (hrr'.1 _)
    rwa [hrr'.2, @enum_lt_enum _ r']
  · rw [← hf, lsub_le_iff]
    intro i
    suffices h : ∃ i' hi', f i ≤ bfamilyOfFamily' r' (fun i => f i) i' hi' by
      rcases h with ⟨i', hi', hfg⟩
      exact hfg.trans_lt (lt_blsub _ _ _)
    by_cases! h : ∀ j, r j i → f j < f i
    · refine ⟨typein r' ⟨i, h⟩, typein_lt_type _ _, ?_⟩
      rw [bfamilyOfFamily'_typein]
    · obtain ⟨hji, hij⟩ := wo.wf.min_mem _ h
      refine ⟨typein r' ⟨_, fun k hkj => lt_of_lt_of_le ?_ hij⟩, typein_lt_type _ _, ?_⟩
      · by_contra! H
        exact (wo.wf.not_lt_min {j | r j i ∧ f i ≤ f j} ⟨IsTrans.trans _ _ _ hkj hji, H⟩) hkj
      · rwa [bfamilyOfFamily'_typein]

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

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

Tactic:
by
  apply ((power_le_power_right <| (cantor c).le).trans _).antisymm
  · exact power_le_power_right (natCast_le_aleph0.trans h)
  · rw [← power_mul, mul_eq_self h]

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

Goal state before:
pp: case inr.a
α : Type u_1
h : (#α).IsStrongPrelimit
ha : #α ≠ 0
h' : (#α).IsStrongLimit
r : α → α → Prop
wo : IsWellOrder α r
hr : (#α).ord = type r
this : LinearOrder α := linearOrderOfSTO r
s : Set α
hs : Unbounded r s
⊢ ∀ (x : α), ∃ y ∈ s, x ≤ y

Tactic:
← not_lt

Goal state after:
case inr.a
α : Type u_1
h : (#α).IsStrongPrelimit
ha : #α ≠ 0
h' : (#α).IsStrongLimit
r : α → α → Prop
wo : IsWellOrder α r
hr : (#α).ord = type r
this : LinearOrder α := linearOrderOfSTO r
s : Set α
hs : Unbounded r s
⊢ ∀ (x : α), ∃ y ∈ s, ¬y < x
Module: Mathlib.SetTheory.Cardinal.Cofinality.Ordinal

Goal state before:
pp: case inr.a
α : Type u_1
h : (#α).IsStrongPrelimit
ha : #α ≠ 0
h' : (#α).IsStrongLimit
r : α → α → Prop
wo : IsWellOrder α r
hr : (#α).ord = type r
this : LinearOrder α := ⋯
⊢ #{ s // #↑s < (#α).ord.cof } ≤ #α

pp: case a
α : Type u_1
h : (#α).IsStrongPrelimit
ha : #α ≠ 0
h' : (#α).IsStrongLimit
r : α → α → Prop
wo : IsWellOrder α r
hr : (#α).ord = type r
this : LinearOrder α := ⋯
⊢ #α ≤ #{ s // #↑s < (#α).ord.cof }

Tactic:
· conv_rhs => rw [← mk_bounded_subset h hr]
    apply mk_subtype_le_of_subset
    intro s hs
    rw [hr] at hs
    contrapose! hs
    rw [not_bounded_iff] at hs
    apply cof_le
    simp_rw [IsCofinal, ← not_lt]
    exact hs

Goal state after:
case a
α : Type u_1
h : (#α).IsStrongPrelimit
ha : #α ≠ 0
h' : (#α).IsStrongLimit
r : α → α → Prop
wo : IsWellOrder α r
hr : (#α).ord = type r
this : LinearOrder α := ⋯
⊢ #α ≤ #{ s // #↑s < (#α).ord.cof }
Module: Mathlib.Data.DFinsupp.Sigma

Goal state before:
pp: case inl
ι : Type u
α : ι → Type u_2
δ : (i : ι) → α i → Type v
inst✝² : DecidableEq ι
inst✝¹ : (i : ι) → DecidableEq (α i)
inst✝ : (i : ι) → (j : α i) → Zero (δ i j)
i : ι
j : α i
x : δ ⟨i, j⟩.fst ⟨i, j⟩.snd
j' : α i
⊢ (single ⟨i, j⟩ x) ⟨i, j'⟩ = ((single i (single j x)) i) j'

Tactic:
rw [single_eq_same]
    obtain rfl | hj := eq_or_ne j' j
    · rw [single_eq_same, single_eq_same]
    · rw [single_eq_of_ne, single_eq_of_ne hj]
      simpa using hj

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

Goal state before:
pp: ι : Type u_1
inst✝¹ : Fintype ι
inst✝ : DecidableEq ι
α : ι → Sort u_2
S : (i : ι) → Setoid (α i)
β : Sort u_3
q : (i : ι) → Quotient (S i)
e : Quotient (Subtype.instSetoid_mathlib fun l ↦ ∀ (i : ι), i ∈ l) :=
  (Equiv.subtypeQuotientEquivQuotientSubtype (fun l ↦ ∀ (i : ι), i ∈ l) (fun s ↦ ∀ (i : ι), i ∈ s) ⋯ ⋯)
    ⟨Finset.univ.val, ⋯⟩
⊢ Quotient piSetoid

Tactic:
refine e.liftOn
    (fun l ↦ (listChoice fun i _ ↦ q i).map (fun a i ↦ a i (l.2 i)) ?_) ?_

Goal state after:
case refine_1
ι : Type u_1
inst✝¹ : Fintype ι
inst✝ : DecidableEq ι
α : ι → Sort u_2
S : (i : ι) → Setoid (α i)
β : Sort u_3
q : (i : ι) → Quotient (S i)
e : Quotient (Subtype.instSetoid_mathlib fun l ↦ ∀ (i : ι), i ∈ l) :=
  (Equiv.subtypeQuotientEquivQuotientSubtype (fun l ↦ ∀ (i : ι), i ∈ l) (fun s ↦ ∀ (i : ι), i ∈ s) ⋯ ⋯)
    ⟨Finset.univ.val, ⋯⟩
l : { l // ∀ (i : ι), i ∈ l }
⊢ ∀ ⦃a b : (i : ι) → i ∈ ↑l → α i⦄, a ≈ b → (fun i ↦ a i ⋯) ≈ fun i ↦ b i ⋯

case refine_2
ι : Type u_1
inst✝¹ : Fintype ι
inst✝ : DecidableEq ι
α : ι → Sort u_2
S : (i : ι) → Setoid (α i)
β : Sort u_3
q : (i : ι) → Quotient (S i)
e : Quotient (Subtype.instSetoid_mathlib fun l ↦ ∀ (i : ι), i ∈ l) :=
  (Equiv.subtypeQuotientEquivQuotientSubtype (fun l ↦ ∀ (i : ι), i ∈ l) (fun s ↦ ∀ (i : ι), i ∈ s) ⋯ ⋯)
    ⟨Finset.univ.val, ⋯⟩
⊢ ∀ (a b : { l // ∀ (i : ι), i ∈ l }),
    a ≈ b →
      Quotient.map (fun a_2 i ↦ a_2 i ⋯) ⋯ (listChoice fun i x ↦ q i) =
        Quotient.map (fun a i ↦ a i ⋯) ⋯ (listChoice fun i x ↦ q i)
Module: Mathlib.Data.DFinsupp.Defs

Goal state before:
pp: ι : Type u
β : ι → Type v
inst✝² : DecidableEq ι
inst✝¹ : (i : ι) → Zero (β i)
inst✝ : (i : ι) → (x : β i) → Decidable (x ≠ 0)
f : Π₀ (i : ι), β i
⊢ f = mk f.support fun i ↦ f ↑i

Tactic:
by aesop

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

Goal state before:
pp: ι : Type u
β₁ : ι → Type v₁
β₂ : ι → Type v₂
inst✝¹ : (i : ι) → Zero (β₁ i)
inst✝ : (i : ι) → Zero (β₂ i)
f : (i : ι) → β₁ i → β₂ i
hf : ∀ (i : ι), f i 0 = 0
⊢ Function.Surjective (mapRange f hf) ↔ ∀ (i : ι), Function.Surjective (f i)

Tactic:
classical
  refine ⟨fun h i u ↦ ?_, fun h x ↦ ?_⟩
  · obtain ⟨x, hx⟩ := h (single i u)
    exact ⟨x i, by simpa using congr($hx i)⟩
  · obtain ⟨x, s, hs⟩ := x
    have (i : ι) : ∃ u : β₁ i, f i u = x i ∧ (x i = 0 → u = 0) :=
      (eq_or_ne (x i) 0).elim
        (fun h ↦ ⟨0, (hf i).trans h.symm, fun _ ↦ rfl⟩)
        (fun h' ↦ by
          obtain ⟨u, hu⟩ := h i (x i)
          exact ⟨u, hu, fun h'' ↦ (h' h'').elim⟩)
    choose y hy using this
    refine ⟨⟨y, Trunc.mk ⟨s, fun i ↦ ?_⟩⟩, ext fun i ↦ ?_⟩
    · exact (hs i).imp_right (hy i).2
    · simp [(hy i).1]

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

Goal state before:
pp: ι : Type u
β : ι → Type v
inst✝³ : DecidableEq ι
inst✝² : (i : ι) → Zero (β i)
inst✝¹ : (i : ι) → (x : β i) → Decidable (x ≠ 0)
p : ι → Prop
inst✝ : DecidablePred p
f : Π₀ (i : ι), β i
⊢ subtypeDomain p f = mk (Finset.subtype p f.support) fun i ↦ f ↑↑i

Tactic:
by
  ext i; by_cases h2 : f i ≠ 0 <;> try simp at h2; simp [h2]

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

Goal state before:
pp: case pos
R : Type u_2
M : Type u_4
inst✝¹⁰ : Ring R
inst✝⁹ : AddCommGroup M
inst✝⁸ : Module R M
x y : M
S : Type u_6
inst✝⁷ : CommRing S
inst✝⁶ : IsDomain S
inst✝⁵ : Module S R
inst✝⁴ : Module S M
inst✝³ : SMulCommClass S R M
inst✝² : IsScalarTower S R M
inst✝¹ : IsTorsionFree S R
a b c d : S
inst✝ : Nontrivial R
h : a * d = b * c
hbd : b = 0 ∧ d = 0
hac : a = 0 ∧ c = 0
⊢ ∃ s t, s • a • x + t • c • x = 0 ∧ (s = 0 → t ≠ 0)

Tactic:
exact ⟨1, 0, by simp [hac.1, hac.2], by simp⟩

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

Goal state before:
pp: R : Type u_2
M : Type u_4
inst✝¹⁰ : Ring R
inst✝⁹ : AddCommGroup M
inst✝⁸ : Module R M
x y : M
S : Type u_6
inst✝⁷ : CommRing S
inst✝⁶ : IsDomain S
inst✝⁵ : Module S R
inst✝⁴ : Module S M
inst✝³ : SMulCommClass S R M
inst✝² : IsScalarTower S R M
inst✝¹ : IsTorsionFree S R
a b c d : S
inst✝ : Nontrivial R
h : a * d = b * c
hbd : b = 0 ∧ d = 0
hac : ¬(a = 0 ∧ c = 0)
⊢ c • 1 = 0 → -a • 1 ≠ 0

Tactic:
by aesop

Goal state after:
Module: Mathlib.Algebra.FreeAbelianGroup.Finsupp

Goal state before:
pp: X : Type u_1
a : FreeAbelianGroup X
⊢ a.support = ∅ ↔ a = 0

Tactic:
exact support_eq_empty

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)) = ⊤
⊢ Surjective ⇑f

Tactic:
rw [Set.range_comp, ← Submodule.map_span, hv, Submodule.map_top] at hsp

Goal state after:
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 : f.range = ⊤
⊢ Surjective ⇑f
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 : { s // LinearIndependent K s }) × ↑(↑(span K (range ↑s)))ᶜ
fst✝ : { s // LinearIndependent K s }
snd✝ : ↑(↑(span K (range ↑fst✝)))ᶜ
⊢ (fun s ↦ ⟨⟨Fin.tail ↑s, ⋯⟩, ⟨↑s 0, ⋯⟩⟩) ((fun s ↦ ⟨Fin.cons ↑s.snd ↑s.fst, ⋯⟩) ⟨fst✝, snd✝⟩) = ⟨fst✝, snd✝⟩

Tactic:
simp only [Fin.cons_zero, Subtype.coe_eta, Sigma.mk.inj_iff,
    Fin.tail_cons, heq_eq_eq, and_self]

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 : Finset β
a : α
inst✝ : DecidableEq α
⊢ ↑(image₂ f (insert a s) t) = ↑(image (fun b ↦ f a b) t ∪ image₂ f s t)

Tactic:
push_cast
    exact image2_insert_left

Goal state after: