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

Goal state before:
pp: case cons
α : Type u_2
inst✝¹ : CommSemiring α
inst✝ : DecidableEq α
n : ℕ
a : α
s : Multiset α
hs : s.sum ^ (s.card * n + 1) ∈ span ↑(Multiset.map (fun x ↦ x ^ (n + 1)) s).toFinset
c : ℕ
_hc : c ∈ Finset.range ((s.card + 1) * n + 1 + 1)
⊢ a ^ c * s.sum ^ ((s.card + 1) * n + 1 - c) * ↑(((s.card + 1) * n + 1).choose c) ∈
    span (insert (a ^ (n + 1)) ↑(Multiset.map (fun x ↦ x ^ (n + 1)) s).toFinset)

Tactic:
mem_span_insert

Goal state after:
case cons
α : Type u_2
inst✝¹ : CommSemiring α
inst✝ : DecidableEq α
n : ℕ
a : α
s : Multiset α
hs : s.sum ^ (s.card * n + 1) ∈ span ↑(Multiset.map (fun x ↦ x ^ (n + 1)) s).toFinset
c : ℕ
_hc : c ∈ Finset.range ((s.card + 1) * n + 1 + 1)
⊢ ∃ a_1,
    ∃ z ∈ span ↑(Multiset.map (fun x ↦ x ^ (n + 1)) s).toFinset,
      a ^ c * s.sum ^ ((s.card + 1) * n + 1 - c) * ↑(((s.card + 1) * n + 1).choose c) = a_1 * a ^ (n + 1) + z
Module: Mathlib.Data.Nat.Choose.Sum

Goal state before:
pp: n : ℕ
h0 : n ≠ 0
⊢ ∑ m ∈ range (n + 1), (-1) ^ m * ↑(n.choose m) = 0

Tactic:
Int.alternating_sum_range_choose,

Goal state after:
n : ℕ
h0 : n ≠ 0
⊢ (if n = 0 then 1 else 0) = 0
Module: Mathlib.LinearAlgebra.Finsupp.Pi

Goal state before:
pp: R : Type u_1
M : Type u_2
P : Type u_4
inst✝⁴ : Semiring R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
inst✝¹ : AddCommMonoid P
inst✝ : Module R P
f : P × M →ₗ[R] M
x : ℕ →₀ P
⊢ (f.prodOfFinsuppNat x).2 = f (f.prodOfFinsuppNat ((comapDomain.addMonoidHom ⋯) x))

Tactic:
simp_rw [prodOfFinsuppNat, coe_lsum, sum, Prod.snd_sum]
  rw [← Finset.sum_preimage (· + 1) _ (add_left_injective 1).injOn _ (by simp_all)]
  simp [pow_succ']

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

Goal state before:
pp: α : Type u
f : Filter α
⊢ ¬Disjoint f f ↔ f.NeBot

Tactic:
by rw [disjoint_self, neBot_iff]

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

Goal state before:
pp: α : Type u_1
β : Type u_2
f : α → β
l : Filter α
⊢ l ≤ comap f ⊤

Tactic:
rw [comap_top]

Goal state after:
α : Type u_1
β : Type u_2
f : α → β
l : Filter α
⊢ l ≤ ⊤
Module: Mathlib.Order.Filter.Map

Goal state before:
pp: α : Type u_1
β : Type u_2
g : Filter β
m : α → β
h : g = ⊥
⊢ comap m g = ⊥

Tactic:
rw [h]

Goal state after:
α : Type u_1
β : Type u_2
g : Filter β
m : α → β
h : g = ⊥
⊢ comap m ⊥ = ⊥
Module: Mathlib.Order.Filter.Basic

Goal state before:
pp: α : Type u
s : Set α
⊢ 𝓟 univ = ⊤

Tactic:
principal_univ

Goal state after:
α : Type u
s : Set α
⊢ ⊤ = ⊤
Module: Mathlib.Order.Filter.Map

Goal state before:
pp: case inl
α : Type u_1
β : Type u_2
f : Filter α
h✝ : IsEmpty β
⊢ (comap Prod.fst f).NeBot ↔ f.NeBot ∧ Nonempty β

pp: case inr
α : Type u_1
β : Type u_2
f : Filter α
h✝ : Nonempty β
⊢ (comap Prod.fst f).NeBot ↔ f.NeBot ∧ Nonempty β

Tactic:
· rw [filter_eq_bot_of_isEmpty (f.comap _), ← not_iff_not]; simp [*]

Goal state after:
case inr
α : Type u_1
β : Type u_2
f : Filter α
h✝ : Nonempty β
⊢ (comap Prod.fst f).NeBot ↔ f.NeBot ∧ Nonempty β
Module: Mathlib.Order.Filter.Basic

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

Tactic:
simp only [Filter.Frequently, ← not_and_or, not_or, eventually_and]

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

Goal state before:
pp: α : Type u_1
β : Type u_2
ι : Sort u_4
ι' : Sort u_5
la : Filter α
pa : ι → Prop
sa : ι → Set α
lb : Filter β
pb : ι' → Prop
sb : ι' → Set β
f : α → β
hla : la.HasBasis pa sa
hlb : lb.HasBasis pb sb
⊢ Tendsto f la lb ↔ ∀ (ib : ι'), pb ib → ∃ ia, pa ia ∧ ∀ x ∈ sa ia, f x ∈ sb ib

Tactic:
by
  simp [hlb.tendsto_right_iff, hla.eventually_iff]

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

Goal state before:
pp: α : Type u_1
β : Type u_2
ι : Sort u_4
la : Filter α
pa : ι → Prop
sa : ι → Set α
h : la.HasBasis pa sa
⊢ (la ×ˢ ⊤).HasBasis pa fun x ↦ sa x ×ˢ univ

Tactic:
by
  simpa only [principal_univ] using h.prod_principal univ

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

Goal state before:
pp: α : Type u_1
β : Type u_2
f : α → β
F : Filter β
⊢ ⋂₀ (comap f F).sets = ⋂ U ∈ F, f ⁻¹' U

Tactic:
by
  ext x
  suffices (∀ (A : Set α) (B : Set β), B ∈ F → f ⁻¹' B ⊆ A → x ∈ A) ↔
      ∀ B : Set β, B ∈ F → f x ∈ B by
    simp only [mem_sInter, mem_iInter, Filter.mem_sets, mem_comap, this, and_imp,
      mem_preimage, exists_imp]
  constructor
  · intro h U U_in
    simpa only [Subset.rfl, forall_prop_of_true, mem_preimage] using h (f ⁻¹' U) U U_in
  · intro h V U U_in f_U_V
    exact f_U_V (h U U_in)

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

Goal state before:
pp: α : 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 ∩ W) = f '' f ⁻¹' U

Tactic:
rw [h]

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

Goal state before:
pp: α : Type u_3
β : Type u_4
γ : Type u_5
inst✝¹ : Preorder β
inst✝ : Preorder γ
f : α → β
e : β → γ
l : Filter α
hm : ∀ (b₁ b₂ : β), e b₁ ≤ e b₂ ↔ b₁ ≤ b₂
hu : ∀ (c : γ), ∃ b, c ≤ e b
⊢ Tendsto (e ∘ f) l atTop ↔ Tendsto f l atTop

Tactic:
rw [← comap_embedding_atTop hm hu, tendsto_comap_iff]

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

Goal state before:
pp: n : ℕ
⊢ ∃ x, ↑x = ↑n ∧ ∀ (a : ℕ), ↑a ≤ ↑n ↔ a ≤ x

Tactic:
exact ⟨n, rfl, fun _ ↦ Int.ofNat_le⟩

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
h₃ : ¬N ≤ N₀
x : M
hx₁ : x ∈ N
hx₂ : x ∉ N₀
⊢ False

Tactic:
apply hx₂

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) := ⋯
H : WellFoundedGT { N // N.FG }
N N₀ : Submodule R M
h₁ : N₀.FG
e : N₀ ≤ N
h₂ : ∀ x ∈ {N' | ↑N' ≤ N}, ¬⟨N₀, h₁⟩ < x
h₃ : ¬N ≤ N₀
x : M
hx₁ : x ∈ N
hx₂ : x ∉ N₀
⊢ x ∈ N₀
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
N₁ N₂ : Submodule R M
hN₁ : N₁.FG
hN₂ : N₂.FG
t₁ : Set M
ht₁ : t₁.Finite
span_t₁ : span R t₁ = N₁
t₂ : Set M
ht₂ : t₂.Finite
span_t₂ : span R t₂ = N₂
⊢ span R (t₁ ∪ t₂) = N₁ ⊔ N₂

Tactic:
span_union,

Goal state after:
R : Type u_1
M : Type u_2
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
N₁ N₂ : Submodule R M
hN₁ : N₁.FG
hN₂ : N₂.FG
t₁ : Set M
ht₁ : t₁.Finite
span_t₁ : span R t₁ = N₁
t₂ : Set M
ht₂ : t₂.Finite
span_t₂ : span R t₂ = N₂
⊢ span R t₁ ⊔ span R t₂ = N₁ ⊔ N₂
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
P Q : { P // P.FG }
⊢ P ≤ ⟨↑P ⊔ ↑Q, ⋯⟩

Tactic:
← Subtype.coe_le_coe

Goal state after:
R : Type u_1
M : Type u_2
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
P Q : { P // P.FG }
⊢ ↑P ≤ ↑⟨↑P ⊔ ↑Q, ⋯⟩
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
P Q : { P // P.FG }
⊢ Q ≤ ⟨↑P ⊔ ↑Q, ⋯⟩

Tactic:
← Subtype.coe_le_coe

Goal state after:
R : Type u_1
M : Type u_2
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
P Q : { P // P.FG }
⊢ ↑Q ≤ ↑⟨↑P ⊔ ↑Q, ⋯⟩
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
P Q R : { P // P.FG }
hPR : P ≤ R
hQR : Q ≤ R
⊢ ⟨↑P ⊔ ↑Q, ⋯⟩ ≤ R

Tactic:
← Subtype.coe_le_coe

Goal state after:
R✝ : Type u_1
M : Type u_2
inst✝² : Semiring R✝
inst✝¹ : AddCommMonoid M
inst✝ : Module R✝ M
P Q R : { P // P.FG }
hPR : ↑P ≤ ↑R
hQR : ↑Q ≤ ↑R
⊢ ↑⟨↑P ⊔ ↑Q, ⋯⟩ ≤ ↑R
Module: Mathlib.RingTheory.Finiteness.Basic

Goal state before:
pp: R : Type u_1
inst✝³ : Semiring R
ι : Type u_5
M : ι → Type u_6
inst✝² : Finite ι
inst✝¹ : (i : ι) → AddCommMonoid (M i)
inst✝ : (i : ι) → Module R (M i)
p : (i : ι) → Submodule R (M i)
t : (i : ι) → Set (M i)
htf : ∀ (i : ι), (t i).Finite
hts : ∀ (i : ι), span R (t i) = p i
⊢ ∃ S, S.Finite ∧ span R S = pi univ p

Tactic:
refine
      ⟨⋃ i, (LinearMap.single R _ i) '' t i, Set.finite_iUnion fun i => (htf i).image _, ?_⟩

Goal state after:
R : Type u_1
inst✝³ : Semiring R
ι : Type u_5
M : ι → Type u_6
inst✝² : Finite ι
inst✝¹ : (i : ι) → AddCommMonoid (M i)
inst✝ : (i : ι) → Module R (M i)
p : (i : ι) → Submodule R (M i)
t : (i : ι) → Set (M i)
htf : ∀ (i : ι), (t i).Finite
hts : ∀ (i : ι), span R (t i) = p i
⊢ span R (⋃ i, ⇑(LinearMap.single R M i) '' t i) = pi univ p
Module: Mathlib.Algebra.Order.Module.Defs

Goal state before:
pp: α : Type u_1
β : Type u_2
a : α
b₁ b₂ : β
inst✝⁷ : Ring α
inst✝⁶ : PartialOrder α
inst✝⁵ : IsOrderedRing α
inst✝⁴ : AddCommGroup β
inst✝³ : PartialOrder β
inst✝² : IsOrderedAddMonoid β
inst✝¹ : Module α β
inst✝ : PosSMulMono α β
h : b₁ ≤ b₂
ha : a ≤ 0
⊢ a • b₂ ≤ a • b₁

Tactic:
rw [← neg_neg a, neg_smul, neg_smul (-a), neg_le_neg_iff]
  exact smul_le_smul_of_nonneg_left h (neg_nonneg_of_nonpos ha)

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:
by
  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.Order.DirSupClosed

Goal state before:
pp: α : Type u_1
inst✝ : PartialOrder α
a : α
⊢ DirSupClosed {a}

Tactic:
by
  intro d hda hdn _ b hb
  rw [hdn.subset_singleton_iff] at hda
  subst hda
  exact mem_singleton_of_eq (hb.unique isLUB_singleton)

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

Goal state before:
pp: α : Type u
r : α → α → Prop
inst✝² : IsWellOrder α r
inst✝¹ : Nonempty α
inst✝ : Subsingleton α
⊢ type r = 1

Tactic:
by
  cases nonempty_unique α
  exact (RelIso.ofUniqueOfIrrefl r _).ordinalType_congr

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

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

Tactic:
← add_le_add_iff_left b

Goal state after:
a b c : Ordinal.{u_4}
h : b + c ≤ a
⊢ b + c ≤ b + (a - b)
Module: Mathlib.SetTheory.Ordinal.Basic

Goal state before:
pp: α β : Type u_1
r : α → α → Prop
s : β → β → Prop
inst✝¹ : IsWellOrder α r
inst✝ : IsWellOrder β s
f : r ≼i s
a : α
⊢ (typein s).toRelEmbedding (f a) = (typein r).toRelEmbedding a

Tactic:
← f.transPrincipal_apply _ a,

Goal state after:
α β : Type u_1
r : α → α → Prop
s : β → β → Prop
inst✝¹ : IsWellOrder α r
inst✝ : IsWellOrder β s
f : r ≼i s
a : α
⊢ (f.transPrincipal (typein s)).toRelEmbedding a = (typein r).toRelEmbedding 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
H : StrictMono (Subtype.val ∘ ⇑(enum s hs)) :=
  StrictMono.comp (Subtype.strictMono_coe fun x ↦ x ∈ s) (OrderIso.strictMono (enum s hs))
⊢ IsNormal (Subtype.val ∘ ⇑(enum s hs)) ↔ DirSupClosed s

Tactic:
refine ⟨fun he ↦ by simpa using he.dirSupClosed_range, ?_⟩

Goal state after:
α : Type u_1
inst✝² : LinearOrder α
inst✝¹ : WellFoundedLT α
inst✝ : IsRegularCardinalOrder α
s : Set α
hs : IsCofinal s
H : StrictMono (Subtype.val ∘ ⇑(enum s hs)) :=
  StrictMono.comp (Subtype.strictMono_coe fun x ↦ x ∈ s) (OrderIso.strictMono (enum s hs))
⊢ DirSupClosed s → IsNormal (Subtype.val ∘ ⇑(enum s hs))
Module: Mathlib.SetTheory.Ordinal.Family

Goal state before:
pp: α : Type u_3
β : Type u_4
f : α ⊕ β → Ordinal.{u}
inst✝¹ : Small.{u, u_3} α
inst✝ : Small.{u, u_4} β
⊢ iSup f = max (⨆ a, f (Sum.inl a)) (⨆ b, f (Sum.inr b))

Tactic:
apply (Ordinal.iSup_le _).antisymm (max_le _ _)
  · rintro (i | i)
    · exact le_max_of_le_left (Ordinal.le_iSup (fun x ↦ f (Sum.inl x)) i)
    · exact le_max_of_le_right (Ordinal.le_iSup (fun x ↦ f (Sum.inr x)) i)
  all_goals
    apply csSup_le_csSup' bddAbove_of_small
    rintro i ⟨a, rfl⟩
    apply mem_range_self

Goal state after:
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}
⊢ sSup (range fun a ↦ f ↑a ⋯) = sSup {a | ∃ i, ∃ (hi : i < o), f i hi = a}

Tactic:
range,

Goal state after:
o : Ordinal.{u_3}
f : (a : Ordinal.{u_3}) → a < o → Ordinal.{max u_4 u_3}
⊢ sSup {x | ∃ y, f ↑y ⋯ = x} = sSup {a | ∃ i, ∃ (hi : i < o), f i hi = a}
Module: Mathlib.SetTheory.Ordinal.Family

Goal state before:
pp: ι : 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
⊢ ?m.88 < lsub f

Tactic:
← heq

Goal state after:
ι : 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
⊢ ?m.88 < succ (iSup f)
Module: Mathlib.SetTheory.Ordinal.Family

Goal state before:
pp: ι : Type u_3
f : ι → Ordinal.{max u_4 u_3}
h : iSup f = lsub f
i : ι
⊢ f i < iSup f

Tactic:
rw [h]

Goal state after:
ι : Type u_3
f : ι → Ordinal.{max u_4 u_3}
h : iSup f = lsub f
i : ι
⊢ f i < lsub f
Module: Mathlib.SetTheory.Ordinal.Family

Goal state before:
pp: o : Ordinal.{u}
f : (a : Ordinal.{u}) → a < o → Ordinal.{max u v}
h : o.bsup f = o.blsub f
i : Ordinal.{u}
⊢ ∀ (hi : i < o), f i hi < o.bsup f

Tactic:
rw [h]

Goal state after:
o : Ordinal.{u}
f : (a : Ordinal.{u}) → a < o → Ordinal.{max u v}
h : o.bsup f = o.blsub f
i : Ordinal.{u}
⊢ ∀ (hi : i < o), f i hi < o.blsub f
Module: Mathlib.Data.Nat.Log

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

pp: case inl.hb
b m n : ℕ
h : m ≠ 0 ∨ 1 < b ∧ n ≠ 0
hb : 1 < b
hn : n ≠ 0
⊢ 1 < b

pp: case inl.hy
b m n : ℕ
h : m ≠ 0 ∨ 1 < b ∧ n ≠ 0
hb : 1 < b
hn : n ≠ 0
⊢ n ≠ 0

pp: case inl.hb
b m n : ℕ
h : m ≠ 0 ∨ 1 < b ∧ n ≠ 0
hb : 1 < b
hn : n ≠ 0
⊢ 1 < b

pp: case inl.hy
b m n : ℕ
h : m ≠ 0 ∨ 1 < b ∧ n ≠ 0
hb : 1 < b
hn : n ≠ 0
⊢ n ≠ 0

Tactic:
and_comm

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

case inl.hb
b m n : ℕ
h : m ≠ 0 ∨ 1 < b ∧ n ≠ 0
hb : 1 < b
hn : n ≠ 0
⊢ 1 < b

case inl.hy
b m n : ℕ
h : m ≠ 0 ∨ 1 < b ∧ n ≠ 0
hb : 1 < b
hn : n ≠ 0
⊢ n ≠ 0

case inl.hb
b m n : ℕ
h : m ≠ 0 ∨ 1 < b ∧ n ≠ 0
hb : 1 < b
hn : n ≠ 0
⊢ 1 < b

case inl.hy
b m n : ℕ
h : m ≠ 0 ∨ 1 < b ∧ n ≠ 0
hb : 1 < b
hn : n ≠ 0
⊢ n ≠ 0
Module: Mathlib.Data.Nat.Log

Goal state before:
pp: case inr.inl
b n : ℕ
hb : 1 < b
h : n < b
⊢ log b (0 * b) = log b n

Tactic:
Nat.zero_mul,

Goal state after:
case inr.inl
b n : ℕ
hb : 1 < b
h : n < b
⊢ log b 0 = log b n
Module: Mathlib.SetTheory.Ordinal.Arithmetic

Goal state before:
pp: case inr
m n : ℕ
h : n ≤ m
⊢ ↑(m - n) = ↑m - ↑n

Tactic:
· rw [← add_left_cancel_iff (a := ↑n), ← Nat.cast_add, add_tsub_cancel_of_le h,
      Ordinal.add_sub_cancel_of_le (Nat.cast_le.2 h)]

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:
by
  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 inl
b o : Ordinal.{u_1}
hb : 1 < b
hbo : b ≤ o
h : o % b ^ log b o = 0
⊢ 0 < log b o

Tactic:
exact log_pos hb (one_le_iff_ne_zero.1 (hb.le.trans hbo)) hbo

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

Goal state before:
pp: op : Ordinal.{u_1} → Ordinal.{u_1} → Ordinal.{u_1}
o a b : Ordinal.{u_1}
ha : ∃ n, a < (fun x ↦ ⨆ y, succ (op (↑y).1 (↑y).2))^[n] o
hb : ∃ n, b < (fun x ↦ ⨆ y, succ (op (↑y).1 (↑y).2))^[n] o
⊢ ∃ n, op a b < (fun x ↦ ⨆ y, succ (op (↑y).1 (↑y).2))^[n] o

Tactic:
obtain ⟨m, ha⟩ := ha

Goal state after:
op : Ordinal.{u_1} → Ordinal.{u_1} → Ordinal.{u_1}
o a b : Ordinal.{u_1}
hb : ∃ n, b < (fun x ↦ ⨆ y, succ (op (↑y).1 (↑y).2))^[n] o
m : ℕ
ha : a < (fun x ↦ ⨆ y, succ (op (↑y).1 (↑y).2))^[m] o
⊢ ∃ n, op a b < (fun x ↦ ⨆ y, succ (op (↑y).1 (↑y).2))^[n] o
Module: Mathlib.SetTheory.Ordinal.FixedPoint

Goal state before:
pp: case inl
a b : Ordinal.{u_1}
ha : a = 0
⊢ 0 = b ↔ 0 ∣ b

Tactic:
zero_dvd_iff

Goal state after:
case inl
a b : Ordinal.{u_1}
ha : a = 0
⊢ 0 = b ↔ b = 0
Module: Mathlib.SetTheory.Ordinal.Principal

Goal state before:
pp: o : Ordinal.{u_1}
⊢ IsPrincipal (fun x1 x2 ↦ x1 + x2) (ω ^ o)

Tactic:
obtain rfl | ha' := eq_or_ne o 0

Goal state after:
case inl
⊢ IsPrincipal (fun x1 x2 ↦ x1 + x2) (ω ^ 0)

case inr
o : Ordinal.{u_1}
ha' : o ≠ 0
⊢ IsPrincipal (fun x1 x2 ↦ x1 + x2) (ω ^ o)
Module: Mathlib.SetTheory.Cardinal.Aleph

Goal state before:
pp: o : Ordinal.{u}
⊢ (preAleph (Ordinal.lift.{v, u} o)).ord = preOmega (Ordinal.lift.{v, u} o)

Tactic:
ord_preAleph

Goal state after:
o : Ordinal.{u}
⊢ preOmega (Ordinal.lift.{v, u} o) = preOmega (Ordinal.lift.{v, u} o)
Module: Mathlib.SetTheory.Cardinal.Aleph

Goal state before:
pp: o : Ordinal.{u_1}
ho : IsSuccPrelimit o
⊢ preAleph o = ⨆ a, preAleph ↑a

Tactic:
obtain rfl | h := eq_or_ne o 0

Goal state after:
case inl
ho : IsSuccPrelimit 0
⊢ preAleph 0 = ⨆ a, preAleph ↑a

case inr
o : Ordinal.{u_1}
ho : IsSuccPrelimit o
h : o ≠ 0
⊢ preAleph o = ⨆ a, preAleph ↑a
Module: Mathlib.SetTheory.Cardinal.Arithmetic

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

Tactic:
exact max_lt ha hb

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

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

Tactic:
by
  rw [mul_comm, mul_eq_left hb ha ha']

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

Goal state before:
pp: case refine_2
α : Type u
inst✝¹ : LinearOrder α
inst✝ : WellFoundedLT α
s : Set α
hs : IsCofinal s
t : Set ↑s
ht : IsCofinal t
ht' : typeLT ↑t = (Order.cof α).ord
⊢ typeLT ↑(Subtype.val '' t) = (Order.cof α).ord

Tactic:
rw [← ht']
    exact ((Subtype.strictMono_coe _).strictMonoOn _).orderIso.ordinalType_congr.symm

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

Goal state before:
pp: α : Type u
β' : Type v
⊢ #↑{f | Surjective f} ≠ 0 ↔ Nonempty (β' ↪ α) ∧ (#α = 0 ∨ #β' ≠ 0)

Tactic:
and_comm

Goal state after:
α : Type u
β' : Type v
⊢ #↑{f | Surjective f} ≠ 0 ↔ (#α = 0 ∨ #β' ≠ 0) ∧ Nonempty (β' ↪ α)
Module: Mathlib.SetTheory.Cardinal.Cofinality.Ordinal

Goal state before:
pp: c : Cardinal.{u_1}
hc : ℵ₀ ≤ c
⊢ c < c ^ c.ord.cof

Tactic:
by
  induction c using Cardinal.inductionOn with | mk α
  obtain ⟨_, _, hα⟩ := exists_ord_eq_type_lt α
  have : NoMaxOrder α := by
    rw [← isSuccPrelimit_type_lt_iff, ← hα]
    exact (isSuccLimit_ord hc).isSuccPrelimit
  obtain ⟨s, hs, hs'⟩ := exists_ord_cof_eq α
  rw [hα, cof_type, ← card_ord (Order.cof _), ← hs', card_type, ← prod_const']
  refine (mk_iUnion_le_sum_mk.trans' ?_).trans_lt (sum_lt_prod _ _ fun i ↦ mk_Iio_lt i.1 hα)
  rw [← mk_univ, ← isCofinal_iff_iUnion_Iio_eq_univ.1 hs, iUnion_coe_set]

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

Goal state before:
pp: α : Type u
β : Type v
inst✝ : Finite α
s : Set α
f : ↑s ↪ β
h : Nonempty (α ≃ β)
⊢ ∃ g, ∀ (x : ↑s), g ↑x = f x

Tactic:
apply extend_function.{u, v} f
  rw [← lift_mk_eq'] at h
  rw [← lift_mk_eq', mk_compl_eq_mk_compl_finite_lift h]
  rw [mk_range_eq_of_injective]; exact f.2

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

Goal state before:
pp: ι : Type u
γ : Type w
β : ι → Type v
inst✝² : (i : ι) → Zero (β i)
inst✝¹ : (i : ι) → SMulZeroClass γ (β i)
p : ι → Prop
inst✝ : DecidablePred p
r : γ
f : Π₀ (i : ι), β i
i✝ : ι
⊢ (filter p (r • f)) i✝ = (r • filter p f) i✝

Tactic:
simp [smul_apply, smul_ite]

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

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

Tactic:
ext ⟨i', j'⟩
  dsimp only
  rw [sigmaUncurry_apply]
  obtain rfl | hi := eq_or_ne i i'
  · rw [single_eq_same]
    obtain rfl | hj := eq_or_ne j' j
    · rw [single_eq_same, single_eq_same]
    · rw [single_eq_of_ne hj, single_eq_of_ne]
      simpa using hj
  · simp [hi]

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.Injective (mapRange f hf) ↔ ∀ (i : ι), Function.Injective (f i)

Tactic:
classical exact ⟨fun h i x y eq ↦ single_injective (@h (single i x) (single i y) <| by
    simpa using congr_arg _ eq), fun h _ _ eq ↦ DFinsupp.ext fun i ↦ h i congr($eq i)⟩

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

Goal state before:
pp: ι : Type u
γ : Type w
β : ι → Type v
β₁ : ι → Type v₁
β₂ : ι → Type v₂
κ : Type u_1
inst✝ : (i : ι) → Zero (β i)
h : ι ≃ κ
f : Π₀ (k : κ), β (h.symm k)
i : ι
⊢ 0 ≍ 0

Tactic:
rw [Equiv.symm_apply_apply]

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

Goal state before:
pp: R : Type u_1
inst✝ : CommSemiring R
f : Dual R R
r : R
| f (r * 1)

Tactic:
← smul_eq_mul

Goal state after:
R : Type u_1
inst✝ : CommSemiring R
f : Dual R R
r : R
| f (r • 1)
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
U V : Submodule R M
⊢ U.dualAnnihilator ⊔ V.dualAnnihilator ≤ (U ⊓ V).dualAnnihilator

Tactic:
rw [le_dualAnnihilator_iff_le_dualCoannihilator, dualCoannihilator_sup_eq]

Goal state after:
R : Type u_1
M : Type u_2
inst✝² : CommSemiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
U V : Submodule R M
⊢ U ⊓ V ≤ U.dualAnnihilator.dualCoannihilator ⊓ V.dualAnnihilator.dualCoannihilator
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✝ x y : M
s t : R
h : t • x + s • y = 0 → t = 0 ∧ s = 0
⊢ t • x + s • y = 0 → s = 0 ∧ t = 0

Tactic:
and_comm

Goal state after:
R : Type u_2
M : Type u_4
inst✝² : Ring R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
x✝ y✝ x y : M
s t : R
h : t • x + s • y = 0 → t = 0 ∧ s = 0
⊢ t • x + s • y = 0 → t = 0 ∧ s = 0
Module: Mathlib.Tactic.Module

Goal state before:
pp: R : Type u_2
M : Type u_3
inst✝² : Ring R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
a₁ a₂ : R × M
l₁ l₂ l : NF R M
h : (a₁ ::ᵣ l₁).eval - l₂.eval = l.eval
⊢ (a₁ ::ᵣ l₁).eval - (a₂ ::ᵣ l₂).eval = ((-a₂.1, a₂.2) ::ᵣ l).eval

Tactic:
simp only [eval_cons, neg_smul, neg_add, sub_eq_add_neg, ← h, ← add_assoc]
  congr! 1
  rw [add_comm, add_assoc]

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

Goal state before:

Tactic:
(a * d) • s
        = d • a • s := by rw [mul_comm, mul_smul]
      _ = -(d • c • t) := by rw [eq_neg_iff_add_eq_zero, ← smul_add, h₁, smul_zero]
      _ = (b * c) • s := ?_

Goal state after:
case left
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
h : a * d ≠ b * c
s t : R
hst : s • (a • x + b • y) + t • (c • x + d • y) = 0
h₁ : a • s + c • t = 0
h₂ : b • s + d • t = 0
⊢ -(d • c • t) = (b * c) • s