mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.RingTheory.Ideal.Quotient.Basic

Goal state before:
pp: case left
R : Type u_5
inst✝ : CommRing R
I : Ideal R
hqf : IsField (R ⧸ I)
h : 1 ∈ I
⊢ False

Tactic:
rcases hqf.exists_pair_ne with ⟨⟨x⟩, ⟨y⟩, hxy⟩

Goal state after:
case left.mk.mk
R : Type u_5
inst✝ : CommRing R
I : Ideal R
hqf : IsField (R ⧸ I)
h : 1 ∈ I
w✝¹ : R ⧸ I
x : R
w✝ : R ⧸ I
y : R
hxy : Quot.mk (⇑(Submodule.quotientRel I)) x ≠ Quot.mk (⇑(Submodule.quotientRel I)) y
⊢ False
Module: Mathlib.RingTheory.Ideal.Basic

Goal state before:
pp: case succ
α : Type u_2
inst✝ : CommSemiring α
s : Set α
n : ℕ
f : ↑s →₀ α
hf : ∑ a ∈ f.support, f a * ↑a = 1
this : 1 ∈ span ((fun i ↦ (f i * ↑i) ^ (n + 1)) '' ↑f.support)
⊢ (fun i ↦ (f i * ↑i) ^ (n + 1)) '' ↑f.support ⊆ ↑(span ((fun x ↦ x ^ (n + 1)) '' s))

Tactic:
rintro _ hx

Goal state after:
case succ
α : Type u_2
inst✝ : CommSemiring α
s : Set α
n : ℕ
f : ↑s →₀ α
hf : ∑ a ∈ f.support, f a * ↑a = 1
this : 1 ∈ span ((fun i ↦ (f i * ↑i) ^ (n + 1)) '' ↑f.support)
a✝ : α
hx : a✝ ∈ (fun i ↦ (f i * ↑i) ^ (n + 1)) '' ↑f.support
⊢ a✝ ∈ ↑(span ((fun x ↦ x ^ (n + 1)) '' s))
Module: Mathlib.RingTheory.Ideal.Quotient.Basic

Goal state before:
pp: case intro
ι : Type u_1
ι' : Type u_2
R : Type u_3
inst✝² : Ring R
I : Ideal R
inst✝¹ : I.IsTwoSided
inst✝ : Finite ι
x : ι → R
hi : ∀ (i : ι), x i ∈ I
f : (ι → R) →ₗ[R] ι' → R
i : ι'
val✝ : Fintype ι
⊢ ∑ x_1, x x_1 * f (fun j ↦ if x_1 = j then 1 else 0) i ∈ I

Tactic:
exact I.sum_mem fun j _ => I.mul_mem_right _ (hi j)

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

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
ι : Sort u_4
ι' : Sort u_5
⊢ ∀ {x y : Set ℕ}, x ∈ range Ici → y ∈ range Ici → ∃ z ∈ range Ici, z ⊆ x ∩ y

Tactic:
rintro _ _ ⟨n, rfl⟩ ⟨m, rfl⟩
        exact ⟨Ici (max n m), mem_range_self _, Ici_inter_Ici.symm.subset⟩

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

Goal state before:
pp: M : Type u_5
inst✝³ : AddCommMonoid M
X : Type u_6
Y : Type u_7
inst✝² : Fintype X
inst✝¹ : Finite Y
inst✝ : DecidableEq Y
f : X → Y
y : Y
s : X →₀ M
⊢ equivFunOnFinite (mapDomain f s) y = ∑ x with f x = y, equivFunOnFinite s x

Tactic:
nth_rw 1 [← Finsupp.univ_sum_single s]

Goal state after:
M : Type u_5
inst✝³ : AddCommMonoid M
X : Type u_6
Y : Type u_7
inst✝² : Fintype X
inst✝¹ : Finite Y
inst✝ : DecidableEq Y
f : X → Y
y : Y
s : X →₀ M
⊢ equivFunOnFinite (mapDomain f (∑ a, Finsupp.single a (s a))) y = ∑ x with f x = y, equivFunOnFinite s x
Module: Mathlib.Order.Filter.Bases.Basic

Goal state before:
pp: α : Type u_1
ι : Sort u_4
ι' : Sort u_5
l l' : Filter α
p : ι → Prop
s : ι → Set α
p' : ι' → Prop
s' : ι' → Set α
hl : l.HasBasis p s
hl' : l'.HasBasis p' s'
⊢ (∀ {i : ι ×' ι'}, p i.fst ∧ p' i.snd → (s i.fst ∩ s' i.snd).Nonempty) ↔
    ∀ ⦃i : ι⦄, p i → ∀ ⦃i' : ι'⦄, p' i' → (s i ∩ s' i').Nonempty

Tactic:
by simp [@forall_comm _ ι']

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

Goal state before:
pp: α : Type u_1
f : Filter α
s : Set α
⊢ s ∈ f ↔ f ⊓ 𝓟 sᶜ = ⊥

Tactic:
by
  refine not_iff_not.1 ((inf_principal_neBot_iff.trans ?_).symm.trans neBot_iff)
  exact
    ⟨fun h hs => by simpa [Set.not_nonempty_empty] using h s hs, fun hs t ht =>
      inter_compl_nonempty_iff.2 fun hts => hs <| mem_of_superset ht hts⟩

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

Goal state before:
pp: α : Type u_1
f : Filter α
s : Set α
⊢ Disjoint f (𝓟 s) ↔ f ⊓ 𝓟 s = ⊥

Tactic:
disjoint_iff

Goal state after:
α : Type u_1
f : Filter α
s : Set α
⊢ f ⊓ 𝓟 s = ⊥ ↔ f ⊓ 𝓟 s = ⊥
Module: Mathlib.Order.Filter.Basic

Goal state before:
pp: α : Type u
f : Filter α
inst✝ : f.NeBot
p : Prop
⊢ (∃ᶠ (x : α) in f, p) ↔ p

Tactic:
by_cases p

Goal state after:
case pos
α : Type u
f : Filter α
inst✝ : f.NeBot
p : Prop
h✝ : p
⊢ (∃ᶠ (x : α) in f, p) ↔ p

case neg
α : Type u
f : Filter α
inst✝ : f.NeBot
p : Prop
h✝ : ¬p
⊢ (∃ᶠ (x : α) in f, p) ↔ p
Module: Mathlib.Algebra.Group.TransferInstance

Goal state before:
pp: M : Type u_1
α : Type u_2
β : Type u_3
e : α ≃ β
inst✝ : CommGroup β
one : One α := e.one
mul : Mul α := e.mul
inv : Inv α := e.Inv
div : Div α := e.div
npow : Pow α ℕ := Equiv.pow ℕ e
zpow : Pow α ℤ := Equiv.pow ℤ e
⊢ CommGroup α

Tactic:
apply e.injective.commGroup _ <;> intros <;> exact e.apply_symm_apply _

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 σ
f : M →ₛₗ[σ] P
hf : Function.Injective ⇑f
N : Submodule R M
hfn : (map f N).FG
t : Finset P
ht : span S ↑t = map f N
⊢ ↑t ⊆ ↑f.range

Tactic:
← span_le,

Goal state after:
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 σ
f : M →ₛₗ[σ] P
hf : Function.Injective ⇑f
N : Submodule R M
hfn : (map f N).FG
t : Finset P
ht : span S ↑t = map f N
⊢ span S ↑t ≤ f.range
Module: Mathlib.SetTheory.Ordinal.Univ

Goal state before:
pp: case mpr.type.refine_3
b✝ : Ordinal.{max (u + 1) v}
β : Type (max (u + 1) v)
s : β → β → Prop
inst✝¹ : IsWellOrder β s
h : lift.{max (u + 1) v, max (u + 1) v} (type s) < lift.{max (u + 1) v, u + 1} (typeLT Ordinal.{u})
f : s ↪r fun x1 x2 ↦ x1 < x2
α : Type u
r : α → α → Prop
inst✝ : IsWellOrder α r
hf : ∀ (b : Ordinal.{u}), b ∈ Set.range ⇑f ↔ b < type r
a' : α
b : β
e : f b = (typein r).toRelEmbedding a'
⊢ ∃ a, (RelEmbedding.ofMonotone (fun b ↦ (enum r) ⟨f b, ⋯⟩) ⋯) a = a'

Tactic:
exists b

Goal state after:
case mpr.type.refine_3
b✝ : Ordinal.{max (u + 1) v}
β : Type (max (u + 1) v)
s : β → β → Prop
inst✝¹ : IsWellOrder β s
h : lift.{max (u + 1) v, max (u + 1) v} (type s) < lift.{max (u + 1) v, u + 1} (typeLT Ordinal.{u})
f : s ↪r fun x1 x2 ↦ x1 < x2
α : Type u
r : α → α → Prop
inst✝ : IsWellOrder α r
hf : ∀ (b : Ordinal.{u}), b ∈ Set.range ⇑f ↔ b < type r
a' : α
b : β
e : f b = (typein r).toRelEmbedding a'
⊢ (RelEmbedding.ofMonotone (fun b ↦ (enum r) ⟨f b, ⋯⟩) ⋯) b = a'
Module: Mathlib.SetTheory.Cardinal.Cofinality.Enum

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

Tactic:
rw [← Subtype.coe_mk o ho, Subtype.coe_le_coe, ← OrderIso.le_symm_apply]

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

Goal state before:
pp: α : Type u_1
inst✝² : LinearOrder α
inst✝¹ : WellFoundedLT α
inst✝ : IsRegularCardinalOrder α
s : Set α
hs : IsCofinal s
f : α → α
⊢ Subtype.val ∘ ⇑(enum s hs) = f ↔ StrictMono f ∧ range f = s

Tactic:
have H := (Subtype.strictMono_coe _).comp (enum s hs).strictMono
  constructor
  · rintro rfl
    use (Subtype.strictMono_coe _).comp (enum s hs).strictMono
    simp
  · rintro ⟨hf, rfl⟩
    rw [← StrictMono.range_inj H hf]
    simp
    rfl

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

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

Tactic:
exact mk_range_le_lift

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

Goal state before:
pp: case refine_2
ι : Type u_3
f : ι → Ordinal.{max u_4 u_3}
hf : ∀ a < lsub f, succ a < lsub f
i : ι
hle : iSup f ≤ f i
⊢ False

Tactic:
have heq := (succ_iSup_eq_lsub_iff f).2 ⟨i, le_antisymm (Ordinal.le_iSup _ _) hle⟩

Goal state after:
case refine_2
ι : Type u_3
f : ι → Ordinal.{max u_4 u_3}
hf : ∀ a < lsub f, succ a < lsub f
i : ι
hle : iSup f ≤ f i
heq : succ (iSup f) = lsub f
⊢ False
Module: Mathlib.SetTheory.Ordinal.Arithmetic

Goal state before:
pp: case inl
b : Ordinal.{u_4}
hb : IsSuccLimit b
⊢ IsSuccPrelimit 0

Tactic:
exact isSuccPrelimit_zero

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

Goal state before:
pp: case inl
a : Ordinal.{u_4}
ha : IsSuccLimit a
⊢ IsSuccPrelimit 0

Tactic:
exact isSuccPrelimit_zero

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

Goal state before:
pp: ⊢ ord 1 = 1

Tactic:
simpa using ord_natCast 1

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

Goal state before:
pp: case refine_2
o : Ordinal.{u}
f : (a : Ordinal.{u}) → a < o → Ordinal.{max u v}
w✝¹ : Ordinal.{u}
w✝ : w✝¹ < o
hf : f w✝¹ w✝ = o.bsup f
⊢ f w✝¹ w✝ < o.blsub f

Tactic:
exact lt_blsub _ _ _

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

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

Tactic:
apply log_eq_of_pow_le_of_lt_pow

Goal state after:
case h₁
b n : ℕ
hb : 1 < b
hn : n ≠ 0
⊢ b ^ (log b n + 1) ≤ n * b

case h₂
b n : ℕ
hb : 1 < b
hn : n ≠ 0
⊢ n * b < b ^ (log b n + 1 + 1)
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:
rw [e, ← mul_add]

Goal state after:
a c b : Ordinal.{u_4}
x✝ : a ∣ c
d : Ordinal.{u_4}
e : c = a * d
⊢ a ∣ a * (b + d)
Module: Mathlib.SetTheory.Ordinal.Family

Goal state before:
pp: case mp
f : Ordinal.{u} → Ordinal.{max u v}
h : ∀ (a : Ordinal.{u}), f a < f (succ a)
⊢ (∀ (o : Ordinal.{u}), IsSuccLimit o → (o.bsup fun x x_1 ↦ f x) = f o) →
    ∀ (o : Ordinal.{u}), IsSuccLimit o → (o.blsub fun x x_1 ↦ f x) = f o

Tactic:
intro H o ho

Goal state after:
case mp
f : Ordinal.{u} → Ordinal.{max u v}
h : ∀ (a : Ordinal.{u}), f a < f (succ a)
H : ∀ (o : Ordinal.{u}), IsSuccLimit o → (o.bsup fun x x_1 ↦ f x) = f o
o : Ordinal.{u}
ho : IsSuccLimit o
⊢ (o.blsub fun x x_1 ↦ f x) = f o
Module: Mathlib.SetTheory.Ordinal.Arithmetic

Goal state before:
pp: a b : Ordinal.{u_4}
b0 : b ≠ 0
h : a ∣ b
⊢ a ≤ b

Tactic:
rcases h with ⟨b, rfl⟩
  simpa using mul_le_mul_right (one_le_iff_ne_zero.mpr fun h ↦ by simp [h] at b0) a

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

Goal state before:
pp: case mpr
f : Ordinal.{u} → Ordinal.{max u v}
h : ∀ (a : Ordinal.{u}), f a < f (succ a)
⊢ (∀ (o : Ordinal.{u}), IsSuccLimit o → (o.blsub fun x x_1 ↦ f x) = f o) →
    ∀ (o : Ordinal.{u}), IsSuccLimit o → (o.bsup fun x x_1 ↦ f x) = f o

Tactic:
intro H o ho

Goal state after:
case mpr
f : Ordinal.{u} → Ordinal.{max u v}
h : ∀ (a : Ordinal.{u}), f a < f (succ a)
H : ∀ (o : Ordinal.{u}), IsSuccLimit o → (o.blsub fun x x_1 ↦ f x) = f o
o : Ordinal.{u}
ho : IsSuccLimit o
⊢ (o.bsup fun x x_1 ↦ f x) = f o
Module: Mathlib.SetTheory.Ordinal.Arithmetic

Goal state before:
pp: case inr
m n : ℕ
hn : n ≠ 0
⊢ ↑(m / n) = ↑m / ↑n

Tactic:
· have hn' : (n : Ordinal) ≠ 0 := Nat.cast_ne_zero.2 hn
    apply le_antisymm
    · rw [← mul_le_iff_le_div hn', ← natCast_mul, Nat.cast_le, mul_comm]
      apply Nat.div_mul_le_self
    · rw [div_le hn', succ_eq_add_one, ← Nat.cast_succ, ← natCast_mul, Nat.cast_lt, mul_comm,
        ← Nat.div_lt_iff_lt_mul (Nat.pos_of_ne_zero hn)]
      apply Nat.lt_succ_self

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

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

Tactic:
· exact opow_le_iff_le_log hb hx

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

Goal state before:
pp: case inr.inr
b o : Ordinal.{u_1}
hbo : o < b
ho : o ≠ 0
hb : 1 < b
⊢ log b o = 0

Tactic:
rwa [← nonpos_iff_eq_zero, ← lt_add_one_iff, zero_add, ← lt_opow_iff_log_lt hb ho, opow_one]

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

Goal state before:
pp: b o : Ordinal.{u_1}
hbo : o < b
⊢ log b o = 0

Tactic:
rcases eq_or_ne o 0 with (rfl | ho)
  · exact log_zero_right b
  rcases le_or_gt b 1 with hb | hb
  · rcases le_one_iff.1 hb with (rfl | rfl)
    · exact log_zero_left o
    · exact log_one_left o
  · rwa [← nonpos_iff_eq_zero, ← lt_add_one_iff, zero_add, ← lt_opow_iff_log_lt hb ho, opow_one]

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

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

Tactic:
opow_add

Goal state after:
case right
b u v w : Ordinal.{u_1}
hb : 1 < b
hv : v ≠ 0
hw : w < b ^ u
⊢ b ^ u * (v + 1) ≤ b ^ u * b ^ (log b v + 1)
Module: Mathlib.SetTheory.Ordinal.Exponential

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

Tactic:
grw [hw, ← mul_add_one, add_assoc, opow_add]
      gcongr
      rw [add_one_le_iff]
      exact lt_opow_succ_log_self hb _

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

Goal state before:
pp: case inl
x y b : Ordinal.{u_1}
hx : x ≠ 0
hy : y ≠ 0
hb : 1 < b
⊢ b ^ (log b x + log b y) ≤ x * y

Tactic:
opow_add

Goal state after:
case inl
x y b : Ordinal.{u_1}
hx : x ≠ 0
hy : y ≠ 0
hb : 1 < b
⊢ b ^ log b x * b ^ log b y ≤ x * y
Module: Mathlib.SetTheory.Ordinal.FixedPoint

Goal state before:
pp: case right.refine_2
ι : Type u_1
f : ι → Ordinal.{u} → Ordinal.{u}
inst✝ : Small.{u, u_1} ι
H : ∀ (i : ι), IsNormal (f i)
a : Ordinal.{u}
ha : a ∈ ⋂ i, fixedPoints (f i)
⊢ ∃ a_1, derivFamily f a_1 = a

Tactic:
Set.mem_iInter

Goal state after:
case right.refine_2
ι : Type u_1
f : ι → Ordinal.{u} → Ordinal.{u}
inst✝ : Small.{u, u_1} ι
H : ∀ (i : ι), IsNormal (f i)
a : Ordinal.{u}
ha : ∀ (i : ι), a ∈ fixedPoints (f i)
⊢ ∃ a_1, derivFamily f a_1 = a
Module: Mathlib.SetTheory.Ordinal.FixedPoint

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

Tactic:
← nfp_mul_one ha

Goal state after:
case a
a b : Ordinal.{u_1}
hb : 0 < b
hba : b ≤ a ^ ω
ha : 0 < a
⊢ nfp (fun x ↦ a * x) 1 ≤ nfp (fun x ↦ a * x) b
Module: Mathlib.SetTheory.Ordinal.FixedPoint

Goal state before:
pp: case inr
a b : Ordinal.{u_1}
hab : a * b = b
ha : 0 < a
hb : ¬b = 0
⊢ a ^ ω ≤ b

Tactic:
← nfp_mul_one ha

Goal state after:
case inr
a b : Ordinal.{u_1}
hab : a * b = b
ha : 0 < a
hb : ¬b = 0
⊢ nfp (fun x ↦ a * x) 1 ≤ b
Module: Mathlib.SetTheory.Cardinal.Aleph

Goal state before:
pp: n : ℕ
IH : preOmega ↑n = ↑n
⊢ n < n + 1

Tactic:
exact lt_succ n

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

Goal state before:
pp: a b c : Ordinal.{u}
hb : IsPrincipal (fun x1 x2 ↦ x1 + x2) b
hab : a < b
hbc : b ≤ c
⊢ a + b + (c - b) = b + (c - b)

Tactic:
hb.add_eq_right hab,

Goal state after:
a b c : Ordinal.{u}
hb : IsPrincipal (fun x1 x2 ↦ x1 + x2) b
hab : a < b
hbc : b ≤ c
⊢ b + (c - b) = b + (c - b)
Module: Mathlib.SetTheory.Ordinal.Principal

Goal state before:
pp: case inr
a b : Ordinal.{u}
hb₁ : b ≠ 1
hb : IsPrincipal (fun x1 x2 ↦ x1 + x2) b
h✝ : 0 < a
⊢ IsPrincipal (fun x1 x2 ↦ x1 + x2) (a * b)

Tactic:
· rcases eq_zero_or_pos b with (rfl | hb₁')
    · rw [mul_zero]
      exact isPrincipal_zero
    · rw [← one_le_iff_pos] at hb₁'
      intro c d hc hd
      rw [lt_mul_iff_of_isSuccLimit
        (isSuccLimit_of_isPrincipal_add (lt_of_le_of_ne hb₁' hb₁.symm) hb)] at *
      rcases hc with ⟨x, hx, hx'⟩
      rcases hd with ⟨y, hy, hy'⟩
      use x + y, hb hx hy
      rw [mul_add]
      exact Left.add_lt_add hx' hy'

Goal state after:
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
hb : b < c
⊢ False

Tactic:
have : a + b < c := add_lt_of_lt hc ha hb

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

Goal state before:
pp: o : Ordinal.{u}
⊢ ω_ 1 ≤ lift.{v, u} o ↔ ω_ 1 ≤ o

Tactic:
by
  simpa using lift_le (a := ω₁)

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

Goal state before:
pp: o : Ordinal.{u}
n : ℕ
⊢ lift.{v, u} o < ω_ ↑n ↔ o < ω_ ↑n

Tactic:
simpa using lift_lt (b := ω_ n)

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

Goal state before:
pp: case refine_2
ι : Type u
f : ι → Ordinal.{max u v} → Ordinal.{max u v}
c : Ordinal.{max u v}
hc : ℵ₀ < c.cof
hc' : Cardinal.lift.{v, u} #ι < c.cof
hf : ∀ (i : ι), ∀ b < c, f i b < c
a : Ordinal.{max u v}
ha : a < c
l : List ι
⊢ List.foldr f a l < c

Tactic:
· induction l with
    | nil => exact ha
    | cons i l H => exact hf _ _ H

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

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

Tactic:
rw [powerlt_le]

Goal state after:
case a
c : Cardinal.{u_1}
h : ℵ₀ ≤ c
⊢ ∀ x < ℵ₀, c ^ x ≤ c
Module: Mathlib.SetTheory.Cardinal.Arithmetic

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

Tactic:
rw [powerlt_le]

Goal state after:
case inr
c : Cardinal.{u_1}
h : c < ℵ₀
⊢ ∀ x < ℵ₀, c ^ x ≤ max c ℵ₀
Module: Mathlib.SetTheory.Cardinal.Regular

Goal state before:
pp: ι : Type u
f : ι → Cardinal.{max u v}
c : Cardinal.{max u v}
hc : c.IsRegular
hι : lift.{v, u} #ι < c
hf : ∀ (i : ι), f i < c
⊢ iSup f < c

Tactic:
by
  apply lift_iSup_lt_of_lt_cof_ord _ hf
  rwa [lift_umax, c.lift_id', hc.cof_ord]

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

Goal state before:
pp: α β : Type u
⊢ #(α ≃ β) = 0 ↔ #α ≠ #β

Tactic:
by
  rw [mk_equiv_eq_zero_iff_lift_ne, lift_id, lift_id]

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

Goal state before:
pp: c : Cardinal.{u}
α β : Type u
s : Set α
t : (a : α) → a ∈ s → Set β
hc : c.IsRegular
hs : #↑s < c
⊢ #↑(⋃ a, ⋃ (h : a ∈ s), t a h) < c ↔ ∀ (a : α) (ha : a ∈ s), #↑(t a ha) < c

Tactic:
by
  rw [biUnion_eq_iUnion, card_iUnion_lt_iff_forall_of_isRegular hc hs, SetCoe.forall']

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

Goal state before:
pp: c : Cardinal.{u_1}
⊢ c < ℵ₀ ∨ c.IsRegular ∨ c.IsSingular

Tactic:
by
  have := isRegular_or_isSingular (c := c)
  rw [← not_le]
  tauto

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

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

Tactic:
H3

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

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

Tactic:
rw [H3]

Goal state after:
ι : Type u
β : ι → Type v
inst✝¹ : DecidableEq ι
inst✝ : (i : ι) → AddZeroClass (β i)
p : (Π₀ (i : ι), β i) → Prop
h0 : p 0
ha : ∀ (i : ι) (b : β i) (f : Π₀ (i : ι), β i), f i = 0 → b ≠ 0 → p f → p (single i b + f)
i : ι
s : Multiset ι
ih : ∀ (f : (i : ι) → β i) (H : ∀ (i : ι), i ∈ s ∨ f i = 0), p { toFun := f, support' := Trunc.mk ⟨s, H⟩ }
f : (i : ι) → β i
H : ∀ (i_1 : ι), i_1 ∈ i ::ₘ s ∨ f i_1 = 0
H2 : ∀ (j : ι), j ∈ s ∨ (if j = i then 0 else f j) = 0
H3 :
  ∀ (aux : ∀ (i_1 : ι), i_1 ∈ i ::ₘ s ∨ (if i_1 = i then 0 else f i_1) = 0),
    { toFun := fun j ↦ if j = i then 0 else f j, support' := Trunc.mk ⟨i ::ₘ s, aux⟩ } =
      { toFun := fun j ↦ if j = i then 0 else f j, support' := Trunc.mk ⟨s, H2⟩ }
⊢ p { toFun := fun j ↦ if j = i then 0 else f j, support' := Trunc.mk ⟨s, H2⟩ }
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 (List.Pi.cons i l (List.Pi.head q) (List.Pi.tail q))

Tactic:
induction List.Pi.head q using Quotient.ind with | _ a

Goal state after:
case a
ι : 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)
a : α i
⊢ C (List.Pi.cons i l ⟦a⟧ (List.Pi.tail q))
Module: Mathlib.Data.DFinsupp.Sigma

Goal state before:
pp: case inr
ι : Type u
γ : Type w
β : ι → Type v
β₁ : ι → Type v₁
β₂ : ι → Type v₂
κ : Type u_1
α : ι → Type u_2
δ : (i : ι) → α i → Type v
inst✝¹ : DecidableEq ι
inst✝ : (i : ι) → (j : α i) → Zero (δ i j)
f : Π₀ (i : ι) (j : α i), δ i j
s : { s // ∀ (i : ι), i ∈ s ∨ f.toFun i = 0 }
fs : (i : ↥(↑s).toFinset) → { s_1 // ∀ (i_1 : α ↑i), i_1 ∈ s_1 ∨ (f ↑i).toFun i_1 = 0 }
i : ι
a : α i
hi : f.toFun i = 0
⊢ (f ⟨i, a⟩.fst) ⟨i, a⟩.snd = 0

Tactic:
simp [toFun_eq_coe f ▸ hi]

Goal state after:
Module: Mathlib.Data.Finsupp.ToDFinsupp

Goal state before:
pp: ι : Type u_1
η : ι → Type u_4
N : Type u_5
inst✝¹ : DecidableEq ι
inst✝ : Zero N
a : (i : ι) × η i
n : N
⊢ sigmaFinsuppEquivDFinsupp (single a n) = DFinsupp.single a.fst (single a.snd n)

Tactic:
obtain ⟨i, a⟩ := a
  ext j b
  by_cases h : i = j
  · subst h
    classical simp [split_apply, Finsupp.single_apply]
  suffices Finsupp.single (⟨i, a⟩ : Σ i, η i) n ⟨j, b⟩ = 0 by simp [split_apply, dif_neg h, this]
  have H : (⟨i, a⟩ : Σ i, η i) ≠ ⟨j, b⟩ := by simp [h]
  classical rw [Finsupp.single_apply, if_neg H]

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

Goal state before:
pp: R : Type u_3
M : Type u_4
inst✝⁵ : CommSemiring R
inst✝⁴ : AddCommMonoid M
inst✝³ : Module R M
inst✝² : IsReflexive R M
M' : Type u_6
inst✝¹ : AddCommMonoid M'
inst✝ : Module R M'
f g : M →ₗ[R] M'
h : Injective ⇑(Dual.eval R M')
hfg : f ∘ₗ ↑(evalEquiv R M).symm = g ∘ₗ ↑(evalEquiv R M).symm
⊢ f = g

Tactic:
LinearEquiv.eq_comp_toLinearMap_iff

Goal state after:
R : Type u_3
M : Type u_4
inst✝⁵ : CommSemiring R
inst✝⁴ : AddCommMonoid M
inst✝³ : Module R M
inst✝² : IsReflexive R M
M' : Type u_6
inst✝¹ : AddCommMonoid M'
inst✝ : Module R M'
f g : M →ₗ[R] M'
h : Injective ⇑(Dual.eval R M')
hfg : f = g
⊢ f = g