mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Data.Multiset.NatAntidiagonal

Goal state before:
pp: n : ℕ
⊢ (antidiagonal n).card = n + 1

Tactic:
rw [antidiagonal, coe_card, List.Nat.length_antidiagonal]

Goal state after:
Module: Mathlib.Order.Disjointed

Goal state before:
pp: α : Type u_1
s : ℕ → Set α
H : ∀ (x : α), ∃ n, x ∈ s n
inst✝ : (x : α) → (n : ℕ) → Decidable (x ∈ s n)
n : ℕ
x : α
⊢ x ∈ (fun x ↦ Nat.find ⋯) ⁻¹' {n} ↔ x ∈ disjointed s n

Tactic:
simp [Nat.find_eq_iff, disjointed_eq_inter_compl]

Goal state after:
Module: Mathlib.Algebra.Ring.Idempotent

Goal state before:
pp: R : Type u_1
inst✝¹ : NonUnitalRing R
inst✝ : IsAddTorsionFree R
p q : R
hp : IsIdempotentElem p
hq : IsIdempotentElem q
hqp : IsIdempotentElem (q - p)
h : p * (q - p) + (q - p) * p = 0
hpq : Commute p q
⊢ q * p = p

Tactic:
← nsmul_right_inj (by simp : 2 ≠ 0),

Goal state after:
R : Type u_1
inst✝¹ : NonUnitalRing R
inst✝ : IsAddTorsionFree R
p q : R
hp : IsIdempotentElem p
hq : IsIdempotentElem q
hqp : IsIdempotentElem (q - p)
h : p * (q - p) + (q - p) * p = 0
hpq : Commute p q
⊢ 2 • (q * p) = 2 • p
Module: Mathlib.RingTheory.Ideal.Span

Goal state before:
pp: α : Type u
inst✝ : CommSemiring α
x y : α
⊢ span {x, y} = span {x} ↔ x ∣ y

Tactic:
Ideal.span_insert,

Goal state after:
α : Type u
inst✝ : CommSemiring α
x y : α
⊢ span {x} ⊔ span {y} = span {x} ↔ x ∣ y
Module: Mathlib.RingTheory.Ideal.Span

Goal state before:
pp: α : Type u
inst✝ : CommSemiring α
x y : α
⊢ span {x, y} = span {y} ↔ y ∣ x

Tactic:
Ideal.span_insert,

Goal state after:
α : Type u
inst✝ : CommSemiring α
x y : α
⊢ span {x} ⊔ span {y} = span {y} ↔ y ∣ x
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
⊢ ∃ r ∈ s, Disjoint ↑I ↑(Submonoid.powers r)

Tactic:
have := hM.1.1

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 : M ≠ ⊤
⊢ ∃ r ∈ s, Disjoint ↑I ↑(Submonoid.powers r)
Module: Mathlib.RingTheory.Ideal.Basic

Goal state before:
pp: ι : Type u_1
R : ι → Type u_5
inst✝ : (i : ι) → Semiring (R i)
r x✝ : (i : ι) → R i
⊢ (∀ (i : ι), x✝ i ∈ span {r i}) ↔ x✝ ∈ span {r}

Tactic:
mem_span_singleton',

Goal state after:
ι : Type u_1
R : ι → Type u_5
inst✝ : (i : ι) → Semiring (R i)
r x✝ : (i : ι) → R i
⊢ (∀ (i : ι), ∃ a, a * r i = x✝ i) ↔ ∃ a, a * r = x✝
Module: Mathlib.RingTheory.Ideal.Quotient.Defs

Goal state before:
pp: R : Type u
inst✝¹ : Ring R
I : Ideal R
inst✝ : I.IsTwoSided
x : R
⊢ (mk I) x = 1 ↔ x - 1 ∈ I

Tactic:
← mk_eq_mk_iff_sub_mem,

Goal state after:
R : Type u
inst✝¹ : Ring R
I : Ideal R
inst✝ : I.IsTwoSided
x : R
⊢ (mk I) x = 1 ↔ (mk I) x = (mk I) 1
Module: Mathlib.Data.Nat.Choose.Sum

Goal state before:
pp: M : Type u_2
inst✝ : CommMonoid M
f : ℕ → ℕ → M
n : ℕ
⊢ ∏ i ∈ range (n + 2), f i (n + 1 - i) ^ (n + 1).choose i =
    (∏ i ∈ range (n + 1), f i (n + 1 - i) ^ n.choose i) * ∏ i ∈ range (n + 1), f (i + 1) (n - i) ^ n.choose i

Tactic:
have A : (∏ i ∈ range (n + 1), f (i + 1) (n - i) ^ (n.choose (i + 1))) * f 0 (n + 1) =
      ∏ i ∈ range (n + 1), f i (n + 1 - i) ^ (n.choose i) := by
    rw [prod_range_succ, prod_range_succ']; simp

Goal state after:
M : Type u_2
inst✝ : CommMonoid M
f : ℕ → ℕ → M
n : ℕ
A :
  (∏ i ∈ range (n + 1), f (i + 1) (n - i) ^ n.choose (i + 1)) * f 0 (n + 1) =
    ∏ i ∈ range (n + 1), f i (n + 1 - i) ^ n.choose i
⊢ ∏ i ∈ range (n + 2), f i (n + 1 - i) ^ (n + 1).choose i =
    (∏ i ∈ range (n + 1), f i (n + 1 - i) ^ n.choose i) * ∏ i ∈ range (n + 1), f (i + 1) (n - i) ^ n.choose i
Module: Mathlib.Algebra.Module.Submodule.IterateMapComap

Goal state before:
pp: case succ
R : Type u_1
N : Type u_2
M : Type u_3
inst✝⁴ : Semiring R
inst✝³ : AddCommMonoid N
inst✝² : Module R N
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
f i : N →ₗ[R] M
K : Submodule R N
h : map f K ≤ map i K
n : ℕ
ih : map f (f.iterateMapComap i n K) ≤ map i (f.iterateMapComap i n K)
⊢ map f (comap f (map i ((fun K ↦ comap f (map i K))^[n] K))) ≤
    map i (comap f (map i ((fun K ↦ comap f (map i K))^[n] K)))

Tactic:
calc
      _ ≤ (f.iterateMapComap i n K).map i := map_comap_le _ _
      _ ≤ (((f.iterateMapComap i n K).map f).comap f).map i := by grw [← le_comap_map]
      _ ≤ _ := by gcongr; exact ih

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

Goal state before:
pp: R : Type u_5
inst✝¹ : CommSemiring R
inst✝ : Nontrivial R
⊢ ¬IsField R ↔ ∃ I, ⊥ < I ∧ I < ⊤

Tactic:
by
  refine ⟨fun h ↦ ?_, fun ⟨I, h_bot, h_top⟩ ↦ not_isField_of_ne_of_ne h_bot.ne' h_top.ne⟩
  obtain ⟨I, hI, hIm⟩ := exists_maximal_of_not_isField h
  exact ⟨I, bot_lt_iff_ne_bot.mpr hI, lt_top_iff_ne_top.mpr hIm.ne_top⟩

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

Goal state before:
pp: α : Type u_1
β : Type u_2
f : α → β
g : β → α
hfg : LeftInverse g f
F : Filter α
⊢ comap f (comap g F) = F

Tactic:
comap_comap,

Goal state after:
α : Type u_1
β : Type u_2
f : α → β
g : β → α
hfg : LeftInverse g f
F : Filter α
⊢ comap (g ∘ f) F = F
Module: Mathlib.Order.Filter.Map

Goal state before:
pp: α : Type u_1
β : Type u_2
f : Filter β
m : α → β
inj : Injective m
large : range m ∈ f
S : Set α
⊢ S ∈ comap m f ↔ m '' S ∈ f

Tactic:
rw [← image_mem_map_iff inj, map_comap_of_mem large]

Goal state after:
Module: Mathlib.Order.Filter.AtTopBot.Disjoint

Goal state before:
pp: case pos
α : Type u_3
inst✝¹ : PartialOrder α
inst✝ : Nontrivial α
x y : α
hne : x ≠ y
hle : x ≤ y
⊢ Disjoint atBot atTop

pp: case neg
α : Type u_3
inst✝¹ : PartialOrder α
inst✝ : Nontrivial α
x y : α
hne : x ≠ y
hle : ¬x ≤ y
⊢ Disjoint atBot atTop

Tactic:
· refine disjoint_of_disjoint_of_mem ?_ (Iic_mem_atBot x) (Ici_mem_atTop y)
    exact Iic_disjoint_Ici.2 (hle.lt_of_ne hne).not_ge

Goal state after:
case neg
α : Type u_3
inst✝¹ : PartialOrder α
inst✝ : Nontrivial α
x y : α
hne : x ≠ y
hle : ¬x ≤ y
⊢ Disjoint atBot atTop
Module: Mathlib.Order.Filter.Tendsto

Goal state before:
pp: α : Type u_1
β : Type u_2
f : α → β
l₁ : Filter α
l₂ : Filter β
⊢ ¬Tendsto f l₁ l₂ ↔ ∃ s ∈ l₂, ∃ᶠ (x : α) in l₁, f x ∉ s

Tactic:
simp only [tendsto_iff_forall_eventually_mem, not_forall, exists_prop, not_eventually]

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

Goal state before:
pp: α : Type u_1
β : Type u_2
f : Filter α
g : Filter β
φ : α → β
ψ : β → α
eq : ψ ∘ φ = id
hφ : Tendsto φ f g
hψ : Tendsto ψ g f
⊢ comap φ (comap ψ f) ≤ f

Tactic:
comap_comap,

Goal state after:
α : Type u_1
β : Type u_2
f : Filter α
g : Filter β
φ : α → β
ψ : β → α
eq : ψ ∘ φ = id
hφ : Tendsto φ f g
hψ : Tendsto ψ g f
⊢ comap (ψ ∘ φ) f ≤ f
Module: Mathlib.Order.Filter.Basic

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

Tactic:
by
  by_cases h : p <;> simp [h, t.ne]

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

Goal state before:
pp: case refine_2
α : Type u_1
β : Type u_2
γ : Type u_3
x : Filter α
g : Filter (α → β)
h : Filter (β → γ)
s : Set (β → γ)
hs : s ∈ h
t : Set β
ht : t ∈ g.seq x
⊢ s.seq t ∈ ((map (fun x1 x2 ↦ x1 ∘ x2) h).seq g).seq x

Tactic:
rcases mem_seq_iff.1 ht with ⟨u, hu, v, hv, ht⟩
    grw [← ht]
    rw [Set.seq_seq]
    exact seq_mem_seq (seq_mem_seq (image_mem_map hs) hu) hv

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

Goal state before:
pp: α : Type u_3
β : Type u_4
inst✝² : Preorder α
inst✝¹ : IsDirectedOrder α
u : α → β
inst✝ : Preorder β
h : Tendsto u atTop atTop
a : α
b : β
this : Nonempty α
⊢ ∃ a', a ≤ a' ∧ b ≤ u a'

Tactic:
have : ∀ᶠ x in atTop, a ≤ x ∧ b ≤ u x :=
    (eventually_ge_atTop a).and (h.eventually <| eventually_ge_atTop b)

Goal state after:
α : Type u_3
β : Type u_4
inst✝² : Preorder α
inst✝¹ : IsDirectedOrder α
u : α → β
inst✝ : Preorder β
h : Tendsto u atTop atTop
a : α
b : β
this✝ : Nonempty α
this : ∀ᶠ (x : α) in atTop, a ≤ x ∧ b ≤ u x
⊢ ∃ a', a ≤ a' ∧ b ≤ u a'
Module: Mathlib.RingTheory.Finiteness.Defs

Goal state before:
pp: M : Type u_2
inst✝ : AddCommMonoid M
P : Submodule ℕ M
x✝ : P.FG
S : Finset M
hS : span ℕ ↑S = P
⊢ AddSubmonoid.closure ↑S = P.toAddSubmonoid

Tactic:
by simpa [← span_nat_eq_addSubmonoidClosure]

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

Goal state before:
pp: R : Type u_4
M : Type u_5
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
motive : (N : Submodule R M) → N.FG → Prop
bot : motive ⊥ ⋯
sup : ∀ (N : Submodule R M) (x : M) (hN : N.FG), motive N hN → motive (N ⊔ R ∙ x) ⋯
s : Finset M
⊢ motive (span R ↑s) ⋯

Tactic:
induction s using Finset.induction with
  | empty => simp [bot]
  | insert x s hxs ih => simpa [span_insert, sup_comm] using sup (span R s) x (by use s) ih

Goal state after:
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:
← type_sum_lex,

Goal state after:
a b : Ordinal.{u_4}
α : Type u_4
r : α → α → Prop
x✝¹ : IsWellOrder α r
β : Type u_4
s : β → β → Prop
x✝ : IsWellOrder β s
⊢ type (Sum.Lex r s) = 0 ↔ type r = 0 ∧ type s = 0
Module: Mathlib.SetTheory.Ordinal.Basic

Goal state before:
pp: α✝ : Type u
β✝ : Type v
γ : Type w
r : α✝ → α✝ → Prop
s : β✝ → β✝ → Prop
t : γ → γ → Prop
α β : Ordinal.{?u.29}
h : α ≤ β
⊢ α.ToType ≤i β.ToType

Tactic:
by
  apply Classical.choice (type_le_iff.mp _)
  rwa [type_toType, type_toType]

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

Goal state before:
pp: s : Set Ordinal.{u}
hf : BddAbove s
f : Ordinal.{u} → Ordinal.{max u v}
⊢ BddAbove (f '' s)

Tactic:
rw [bddAbove_iff_small] at hf ⊢

Goal state after:
s : Set Ordinal.{u}
hf : Small.{u, u + 1} ↑s
f : Ordinal.{u} → Ordinal.{max u v}
⊢ Small.{max u v, (max u v) + 1} ↑(f '' s)
Module: Mathlib.SetTheory.Ordinal.Basic

Goal state before:
pp: α : Type u
β : Type v
γ : Type w
r : α → α → Prop
s : β → β → Prop
t : γ → γ → Prop
c a b : Ordinal.{u}
⊢ (fun x1 x2 ↦ x1 ≤ x2) a b → (fun x1 x2 ↦ x1 ≤ x2) ((fun x1 x2 ↦ x1 + x2) c a) ((fun x1 x2 ↦ x1 + x2) c b)

Tactic:
refine inductionOn₃ a b c fun α r _ β s _ γ t _ ⟨f⟩ ↦
      (RelEmbedding.ofMonotone (Sum.recOn · Sum.inl (Sum.inr ∘ f)) ?_).ordinal_type_le
    simp [f.map_rel_iff]

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)

Tactic:
have hs' := bddAbove_add_one_image_iff.2 hs

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

Goal state before:
pp: a b : Ordinal.{u_4}
ha : IsSuccLimit a
⊢ IsSuccPrelimit (a * b)

Tactic:
obtain rfl | hb := eq_zero_or_pos b

Goal state after:
case inl
a : Ordinal.{u_4}
ha : IsSuccLimit a
⊢ IsSuccPrelimit (a * 0)

case inr
a b : Ordinal.{u_4}
ha : IsSuccLimit a
hb : 0 < b
⊢ IsSuccPrelimit (a * b)
Module: Mathlib.Data.Nat.Log

Goal state before:
pp: case succ
b n : ℕ
h : 1 < b
hn : b ≤ n
c : ℕ
⊢ log b n < c + 1 ↔ log b (n / b) + 1 < c + 1

Tactic:
have : n / b ≠ 0 := by simp [*, Nat.ne_zero_of_lt h]

Goal state after:
case succ
b n : ℕ
h : 1 < b
hn : b ≤ n
c : ℕ
this : n / b ≠ 0
⊢ log b n < c + 1 ↔ log b (n / b) + 1 < c + 1
Module: Mathlib.Data.Nat.Log

Goal state before:
pp: case inr.inl
b m n : ℕ
h : m ≠ 0 ∨ 1 < b ∧ n ≠ 0
hm : m ≠ 0
hb : b ≤ 1
⊢ log b n = m ↔ b ^ m ≤ n ∧ n < b ^ (m + 1)

Tactic:
obtain rfl | rfl := le_one_iff_eq_zero_or_eq_one.1 hb <;>
      simp only [log_zero_left, log_one_left]

Goal state after:
case inr.inl.inl
m n : ℕ
hm : m ≠ 0
h : m ≠ 0 ∨ 1 < 0 ∧ n ≠ 0
hb : 0 ≤ 1
⊢ 0 = m ↔ 0 ^ m ≤ n ∧ n < 0 ^ (m + 1)

case inr.inl.inr
m n : ℕ
hm : m ≠ 0
h : m ≠ 0 ∨ 1 < 1 ∧ n ≠ 0
hb : 1 ≤ 1
⊢ 0 = m ↔ 1 ^ m ≤ n ∧ n < 1 ^ (m + 1)
Module: Mathlib.SetTheory.Ordinal.Exponential

Goal state before:
pp: a : Ordinal.{u_1}
h : 1 < a
⊢ IsNormal fun x ↦ a ^ x

Tactic:
have ha : 0 < a := zero_lt_one.trans h

Goal state after:
a : Ordinal.{u_1}
h : 1 < a
ha : 0 < a
⊢ IsNormal fun x ↦ a ^ x
Module: Mathlib.SetTheory.Ordinal.Family

Goal state before:
pp: α : Type u_1
inst✝ : Small.{u, u_1} α
f : α → Ordinal.{u}
h : Surjective f
a : α
ha : f a = ⨆ i, succ (f i)
⊢ f a < ⨆ i, succ (f i)

Tactic:
Ordinal.lt_iSup_iff

Goal state after:
α : Type u_1
inst✝ : Small.{u, u_1} α
f : α → Ordinal.{u}
h : Surjective f
a : α
ha : f a = ⨆ i, succ (f i)
⊢ ∃ i, f a < succ (f i)
Module: Mathlib.SetTheory.Ordinal.Exponential

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

Tactic:
obtain rfl | hb := eq_zero_or_pos b

Goal state after:
case inl
a c : Ordinal.{u_1}
⊢ a ^ (0 * c) = (a ^ 0) ^ c

case inr
a b c : Ordinal.{u_1}
hb : 0 < b
⊢ a ^ (b * c) = (a ^ b) ^ c
Module: Mathlib.SetTheory.Ordinal.Exponential

Goal state before:
pp: b u v w x : Ordinal.{u_1}
hv : v < b
hw : w < b ^ u
hu : u < x
⊢ b ^ succ u ≤ b ^ x

Tactic:
exact opow_le_opow_right hv.pos (succ_le_of_lt hu)

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

Goal state before:
pp: b n m : ℕ
h : n ≤ m
⊢ clog b n ≤ clog b m

Tactic:
rcases le_or_gt b 1 with hb | hb
  · rw [clog_of_left_le_one hb]
    exact zero_le _
  · rw [clog_le_iff_le_pow hb]
    exact h.trans (le_pow_clog hb _)

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

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

Tactic:
grw [opow_add, opow_log_le_self b hv, ← le_self_add]

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

Goal state before:
pp: case refine_1
a b : Ordinal.{u_1}
h : a + b = b
⊢ a * ω ≤ b

pp: case refine_2
a b : Ordinal.{u_1}
h : a * ω ≤ b
⊢ a + b = b

Tactic:
· rw [← nfp_add_zero a, ← deriv_zero_right]
    obtain ⟨c, hc⟩ := (mem_range_deriv (isNormal_add_right a)).2 h
    rw [← hc]
    exact (isNormal_deriv _).monotone zero_le

Goal state after:
case refine_2
a b : Ordinal.{u_1}
h : a * ω ≤ b
⊢ a + b = b
Module: Mathlib.SetTheory.Cardinal.Aleph

Goal state before:
pp: o : Ordinal.{u_1}
ho : ω ^ ↑2 ≤ o
⊢ ω < ω ^ ↑2

Tactic:
apply left_lt_opow one_lt_omega0

Goal state after:
o : Ordinal.{u_1}
ho : ω ^ ↑2 ≤ o
⊢ 1 < ↑2
Module: Mathlib.SetTheory.Cardinal.Aleph

Goal state before:
pp: c : Cardinal.{u}
⊢ ℵ_ 1 = lift.{v, u} c ↔ ℵ_ 1 = c

Tactic:
by
  simpa using lift_inj (a := ℵ₁)

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

Goal state before:
pp: case pos
ι : Type u
f : ι → Ordinal.{v}
n : ℕ
hι : Cardinal.lift.{v, u} #ι ≤ Cardinal.lift.{u, v} ↑n
hf : ∀ (i : ι), (f i).card ≤ ↑n
hc : ↑n < ℵ₀
i : ι
⊢ f i ≤ ↑n

Tactic:
simpa using hf i

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

Goal state before:
pp: o : Ordinal.{u_1}
H : (ℵ_ o).IsRegular
⊢ (ω_ o).cof = ℵ_ o

Tactic:
← ord_aleph,

Goal state after:
o : Ordinal.{u_1}
H : (ℵ_ o).IsRegular
⊢ (ℵ_ o).ord.cof = ℵ_ o
Module: Mathlib.SetTheory.Cardinal.Arithmetic

Goal state before:
pp: case a
ι : Type u
inst✝ : Infinite ι
c : ι → Cardinal.{v}
h₁ : ∀ (i : ι), 2 ≤ c i
h₂ : ∀ (i : ι), lift.{u, v} (c i) ≤ lift.{v, u} #ι
⊢ lift.{v, u} (2 ^ #ι) ≤ prod fun i ↦ lift.{u, v} (c i)

Tactic:
← prod_const',

Goal state after:
case a
ι : Type u
inst✝ : Infinite ι
c : ι → Cardinal.{v}
h₁ : ∀ (i : ι), 2 ≤ c i
h₂ : ∀ (i : ι), lift.{u, v} (c i) ≤ lift.{v, u} #ι
⊢ lift.{v, u} (prod fun x ↦ 2) ≤ prod fun i ↦ lift.{u, v} (c i)
Module: Mathlib.SetTheory.Cardinal.Cofinality.Ordinal

Goal state before:
pp: case inl
α : Type u_1
h : (#α).IsStrongPrelimit
r : α → α → Prop
inst✝ : IsWellOrder α r
hr : (#α).ord = type r
ha : #α = 0
this : IsEmpty α
⊢ #{ s // Bounded r s } = 0

Tactic:
rw [mk_eq_zero_iff]

Goal state after:
case inl
α : Type u_1
h : (#α).IsStrongPrelimit
r : α → α → Prop
inst✝ : IsWellOrder α r
hr : (#α).ord = type r
ha : #α = 0
this : IsEmpty α
⊢ IsEmpty { s // Bounded r s }
Module: Mathlib.SetTheory.Cardinal.Arithmetic

Goal state before:
pp: α β : Type u
⊢ #α ≠ lift.{u, u} #β ↔ #α ≠ #β

Tactic:
lift_id

Goal state after:
α β : Type u
⊢ #α ≠ #β ↔ #α ≠ #β
Module: Mathlib.SetTheory.Cardinal.Regular

Goal state before:
pp: c : Cardinal.{u}
ι : Type u
f : ι → Cardinal.{u}
hc : c.IsRegular
hι : #ι < c
⊢ lift.{u, u} #ι < c

Tactic:
lift_id

Goal state after:
c : Cardinal.{u}
ι : Type u
f : ι → Cardinal.{u}
hc : c.IsRegular
hι : #ι < c
⊢ #ι < c
Module: Mathlib.SetTheory.Cardinal.Regular

Goal state before:
pp: ι : Type u
f : ι → Ordinal.{u} → Ordinal.{u}
c : Cardinal.{u}
hc : c.IsRegular
hι : #ι < c
hc' : c ≠ ℵ₀
a : Ordinal.{u}
hf : ∀ (i : ι), ∀ b < c.ord, f i b < c.ord
⊢ lift.{?u.39, u} #ι < c

Tactic:
lift_id

Goal state after:
ι : Type u
f : ι → Ordinal.{u} → Ordinal.{u}
c : Cardinal.{u}
hc : c.IsRegular
hι : #ι < c
hc' : c ≠ ℵ₀
a : Ordinal.{u}
hf : ∀ (i : ι), ∀ b < c.ord, f i b < c.ord
⊢ #ι < c
Module: Mathlib.SetTheory.Cardinal.Arithmetic

Goal state before:
pp: α β : Type u
inst✝ : Infinite α
eq : #α = #β
⊢ 2 ^ lift.{u, u} #α = 2 ^ #α

Tactic:
lift_id

Goal state after:
α β : Type u
inst✝ : Infinite α
eq : #α = #β
⊢ 2 ^ #α = 2 ^ #α
Module: Mathlib.SetTheory.Cardinal.Arithmetic

Goal state before:
pp: α : Type u
β' : Type v
inst✝ : Infinite α
lle : lift.{u, v} #β' ≤ lift.{v, u} #α
⊢ #(β' → α) ≤ #(β' ↪ α)

Tactic:
conv_rhs => rw [← (Equiv.embeddingCongr (.refl _)
      (Cardinal.eq.mp <| mul_eq_self <| aleph0_le_mk α).some).cardinal_eq]

Goal state after:
α : Type u
β' : Type v
inst✝ : Infinite α
lle : lift.{u, v} #β' ≤ lift.{v, u} #α
⊢ #(β' → α) ≤ #(β' ↪ α × α)
Module: Mathlib.SetTheory.Cardinal.Regular

Goal state before:
pp: ι : Type u
f : ι → Ordinal.{u} → Ordinal.{u}
c : Cardinal.{u}
hc : c.IsRegular
hι : #ι < c
hc' : c ≠ ℵ₀
hf : ∀ (i : ι), ∀ b < c.ord, f i b < c.ord
a : Ordinal.{u}
⊢ lift.{?u.39, u} #ι < c

Tactic:
lift_id

Goal state after:
ι : Type u
f : ι → Ordinal.{u} → Ordinal.{u}
c : Cardinal.{u}
hc : c.IsRegular
hι : #ι < c
hc' : c ≠ ℵ₀
hf : ∀ (i : ι), ∀ b < c.ord, f i b < c.ord
a : Ordinal.{u}
⊢ #ι < c
Module: Mathlib.SetTheory.Cardinal.Regular

Goal state before:
pp: c : Cardinal.{u_1}
hc : c.IsInaccessible
⊢ ω_ c.ord = c.ord

Tactic:
← ord_aleph,

Goal state after:
c : Cardinal.{u_1}
hc : c.IsInaccessible
⊢ (ℵ_ c.ord).ord = c.ord
Module: Mathlib.SetTheory.Cardinal.Regular

Goal state before:
pp: ⊢ ω_ Ordinal.univ.{u, v} = Ordinal.univ.{u, v}

Tactic:
simpa using IsInaccessible.univ.omega_ord

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

Goal state before:
pp: α : Type u
β : Type v
inst✝ : Finite α
s : Set α
f : ↑s ↪ β
h : lift.{v, u} #α = lift.{u, v} #β
⊢ Nonempty (↑sᶜ ≃ ↑(range ⇑f)ᶜ)

Tactic:
rw [← lift_mk_eq', mk_compl_eq_mk_compl_finite_lift h]

Goal state after:
α : Type u
β : Type v
inst✝ : Finite α
s : Set α
f : ↑s ↪ β
h : lift.{v, u} #α = lift.{u, v} #β
⊢ lift.{v, u} #↑s = lift.{u, v} #↑(range ⇑f)
Module: Mathlib.Data.DFinsupp.Submonoid

Goal state before:
pp: ι : Type u
γ : Type w
inst✝² : DecidableEq ι
inst✝¹ : AddCommMonoid γ
S : ι → AddSubmonoid γ
inst✝ : (i : ι) → (x : ↥(S i)) → Decidable (x ≠ 0)
x : γ
⊢ x ∈ iSup S ↔ ∃ f, (f.sum fun x xi ↦ ↑xi) = x

Tactic:
rw [AddSubmonoid.mem_iSup_iff_exists_dfinsupp]
  simp_rw [sumAddHom_apply]
  rfl

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)
f : Π₀ (i : ι), β i
H : f.support = ∅
⊢ ∀ (i : ι), f i = 0 i

Tactic:
by simpa [Finset.ext_iff] using H

Goal state after:
Module: Mathlib.Data.Fin.Tuple.Reflection

Goal state before:
pp: case refine_2
α : Type u_1
β : Type u_2
n : ℕ
f : Fin (n + 1) → α → β
v : Fin (n + 1) → α
i✝ : Fin (n + 1)
i : Fin n
⊢ Matrix.vecCons (f 0 (v 0)) (fun i ↦ Matrix.vecTail f i (Matrix.vecTail v i)) i.succ = f i.succ (v i.succ)

Tactic:
Matrix.cons_val_succ

Goal state after:
case refine_2
α : Type u_1
β : Type u_2
n : ℕ
f : Fin (n + 1) → α → β
v : Fin (n + 1) → α
i✝ : Fin (n + 1)
i : Fin n
⊢ Matrix.vecTail f i (Matrix.vecTail v i) = f i.succ (v i.succ)
Module: Mathlib.LinearAlgebra.Dual.Defs

Goal state before:
pp: R : Type u_1
M : Type u_2
inst✝² : CommSemiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
Φ : Submodule R (Dual R M)
x : M
⊢ x ∈ Φ.dualCoannihilator ↔ ∀ φ ∈ Φ, φ x = 0

Tactic:
simp_rw [dualCoannihilator, mem_comap, mem_dualAnnihilator, Module.Dual.eval_apply]

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
⊢ LinearIndependent R ![x + y, y] ↔ LinearIndependent R ![x, y]

Tactic:
← pair_symm_iff,

Goal state after:
R : Type u_2
M : Type u_4
inst✝² : Ring R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
x y : M
⊢ LinearIndependent R ![y, x + y] ↔ LinearIndependent R ![x, y]
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
η : Type u_6
ιs : η → Type u_7
f : (j : η) → ιs j → M
hindep : ∀ (j : η), LinearIndependent R (f j)
hd : ∀ (i : η) (t : Set η), t.Finite → i ∉ t → Disjoint (span R (range (f i))) (⨆ i ∈ t, span R (range (f i)))
a✝ : Nontrivial R
x₁ : η
x₂ y₂ : ιs x₁
hxy : (fun ji ↦ f ji.fst ji.snd) ⟨x₁, x₂⟩ = (fun ji ↦ f ji.fst ji.snd) ⟨x₁, y₂⟩
⊢ Eq.recOn ⋯ ⟨x₁, x₂⟩.snd = ⟨x₁, y₂⟩.snd

Tactic:
LinearIndependent.injective (hindep _) hxy

Goal state after:
case pos
R : Type u_2
M : Type u_4
inst✝² : Ring R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
η : Type u_6
ιs : η → Type u_7
f : (j : η) → ιs j → M
hindep : ∀ (j : η), LinearIndependent R (f j)
hd : ∀ (i : η) (t : Set η), t.Finite → i ∉ t → Disjoint (span R (range (f i))) (⨆ i ∈ t, span R (range (f i)))
a✝ : Nontrivial R
x₁ : η
x₂ y₂ : ιs x₁
hxy : (fun ji ↦ f ji.fst ji.snd) ⟨x₁, x₂⟩ = (fun ji ↦ f ji.fst ji.snd) ⟨x₁, y₂⟩
⊢ Eq.recOn ⋯ ⟨x₁, y₂⟩.snd = ⟨x₁, y₂⟩.snd
Module: Mathlib.Algebra.Group.AddChar

Goal state before:
pp: A : Type u_1
R : Type u_2
inst✝⁴ : AddGroup A
inst✝³ : Fintype A
inst✝² : CommSemiring R
inst✝¹ : IsDomain R
ψ : AddChar A R
inst✝ : CharZero R
⊢ ↑(card A) ≠ 0

Tactic:
exact Nat.cast_ne_zero.2 Fintype.card_ne_zero

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

Goal state before:
pp: R : Type u_1
M : Type u_3
inst✝¹ : Semiring R
inst✝ : Nontrivial R
m : M
s : Set M
⊢ Finsupp.single m 1 ∈ Submodule.map (↑(coeffLinearEquiv R)) (Submodule.span R ((fun x ↦ single x 1) '' s)) ↔ m ∈ s

Tactic:
simp [Submodule.map_span, ← Set.image_comp, Finsupp.single_mem_span_single]

Goal state after:
Module: Mathlib.Algebra.Group.Pointwise.Set.ListOfFn

Goal state before:
pp: case h.mpr
α : Type u_1
inst✝ : Monoid α
a : α
n : ℕ
f : Fin n → Set α
⊢ (∃ x, (List.ofFn ((fun x ↦ ↑x.snd) ∘ x)).prod = a ∧ Sigma.fst ∘ x = f) → ∃ f_1, (List.ofFn fun i ↦ ↑(f_1 i)).prod = a

Tactic:
· rintro ⟨fi, rfl, rfl⟩
    exact ⟨fun i ↦ _, rfl⟩

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:
by
    push_cast
    exact image2_insert_left

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

Goal state before:
pp: α : Type u_1
s : Finset α
r : α → α → Prop
inst✝⁴ : DecidableRel r
inst✝³ : IsTrans α r
inst✝² : Std.Antisymm r
inst✝¹ : Std.Total r
inst✝ : DecidableEq α
a : α
h₁ : ∀ b ∈ s, r a b
h₂ : a ∉ s
⊢ (insert a s).sort r = a :: s.sort r

Tactic:
by
  rw [← cons_eq_insert _ _ h₂, sort_cons r h₁]

Goal state after:
Module: Mathlib.Algebra.Group.UniqueProds.Basic

Goal state before:
pp: G : Type u_1
inst✝ : Mul G
A B : Finset G
a0 b0 : G
h : UniqueMul A B a0 b0
⊢ UniqueMul (map ({ toFun := op, inj' := ⋯ }.trans { toFun := op, inj' := ⋯ }) A)
    (map ({ toFun := op, inj' := ⋯ }.trans { toFun := op, inj' := ⋯ }) B) (op (op a0)) (op (op b0))

Tactic:
exact (mulHom_map_iff _ fun _ _ ↦ by rfl).mpr h

Goal state after: