mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Algebra.BigOperators.Intervals

Goal state before:
pp: α : Type u_1
M : Type u_3
inst✝⁵ : CommMonoid M
inst✝⁴ : AddCommMonoid α
inst✝³ : PartialOrder α
inst✝² : IsOrderedCancelAddMonoid α
inst✝¹ : ExistsAddOfLE α
inst✝ : LocallyFiniteOrder α
f : α → M
a b c : α
⊢ ∏ x ∈ Ico a b, f (x + c) = ∏ x ∈ map (addRightEmbedding c) (Ico a b), f x

Tactic:
prod_map

Goal state after:
α : Type u_1
M : Type u_3
inst✝⁵ : CommMonoid M
inst✝⁴ : AddCommMonoid α
inst✝³ : PartialOrder α
inst✝² : IsOrderedCancelAddMonoid α
inst✝¹ : ExistsAddOfLE α
inst✝ : LocallyFiniteOrder α
f : α → M
a b c : α
⊢ ∏ x ∈ Ico a b, f (x + c) = ∏ x ∈ Ico a b, f ((addRightEmbedding c) x)
Module: Mathlib.Algebra.BigOperators.Intervals

Goal state before:
pp: case inl
M : Type u_3
inst✝ : CommMonoid M
f : ℕ → M
k m n : ℕ
h : m ≤ n + 1
this : ∀ i < m, i ≤ n
hkm : k < m
⊢ ∏ j ∈ Ico k m, f (n - j) = ∏ j ∈ Ico (n + 1 - m) (n + 1 - k), f j

Tactic:
rw [← Nat.Ico_image_const_sub_eq_Ico (this _ hkm)]
    refine (prod_image ?_).symm
    simp only [mem_Ico, Set.InjOn, mem_coe]
    rintro i ⟨_, im⟩ j ⟨_, jm⟩ Hij
    rw [← tsub_tsub_cancel_of_le (this _ im), Hij, tsub_tsub_cancel_of_le (this _ jm)]

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

Goal state before:
pp: n : ℕ
⊢ n • (n - 1) = n * (n - 1)

Tactic:
Nat.nsmul_eq_mul

Goal state after:
n : ℕ
⊢ n * (n - 1) = n * (n - 1)
Module: Mathlib.Algebra.BigOperators.NatAntidiagonal

Goal state before:
pp: M : Type u_1
inst✝ : CommMonoid M
n : ℕ
f : ℕ × ℕ → M
⊢ f (0, n + 1) *
      ∏
        x ∈
          map ({ toFun := Nat.succ, inj' := Nat.succ_injective }.prodMap (Function.Embedding.refl ℕ)) (antidiagonal n),
        f x =
    f (0, n + 1) * ∏ p ∈ antidiagonal n, f (p.1 + 1, p.2)

Tactic:
prod_map

Goal state after:
M : Type u_1
inst✝ : CommMonoid M
n : ℕ
f : ℕ × ℕ → M
⊢ f (0, n + 1) *
      ∏ x ∈ antidiagonal n,
        f (({ toFun := Nat.succ, inj' := Nat.succ_injective }.prodMap (Function.Embedding.refl ℕ)) x) =
    f (0, n + 1) * ∏ p ∈ antidiagonal n, f (p.1 + 1, p.2)
Module: Mathlib.RingTheory.Ideal.Span

Goal state before:
pp: α : Type u
inst✝ : Semiring α
⊢ span 1 = ⊤

Tactic:
rw [← Set.singleton_one, span_singleton_one]

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

Goal state before:
pp: case inl
α : Type u
inst✝ : CommSemiring α
I : Ideal α
a : α
ha : IsIdempotentElem a
haI : a ∉ I
⊢ 1 ∉ ↑I

pp: case inr
α : Type u
inst✝ : CommSemiring α
I : Ideal α
a✝ : α
ha : IsIdempotentElem a✝
haI : a✝ ∉ I
⊢ a✝ ∉ ↑I

Tactic:
exacts [I.ne_top_iff_one.mp (ne_of_mem_of_not_mem' Submodule.mem_top haI).symm, haI]

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

Goal state before:
pp: R : Type u_5
inst✝ : CommRing R
I : Ideal R
hqf : IsField (R ⧸ I)
⊢ I.IsMaximal

Tactic:
apply Ideal.isMaximal_iff.2

Goal state after:
R : Type u_5
inst✝ : CommRing R
I : Ideal R
hqf : IsField (R ⧸ I)
⊢ 1 ∉ I ∧ ∀ (J : Ideal R) (x : R), I ≤ J → x ∉ I → x ∈ J → 1 ∈ J
Module: Mathlib.RingTheory.Ideal.Quotient.Basic

Goal state before:
pp: case mk.mk.mk
ι : Type u_1
ι' : Type u_2
R : Type u_3
S : Type u_4
inst✝¹ : Ring R
I J : Ideal R
a✝ b✝ : R
inst✝ : I.IsTwoSided
r✝ : R ⧸ I
a : R
s✝ : R ⧸ I
b : R
x✝ : (ι → R) ⧸ pi fun x ↦ I
c : ι → R
⊢ (Quot.mk (⇑(Submodule.quotientRel I)) a + Quot.mk (⇑(Submodule.quotientRel I)) b) •
      Quot.mk (⇑(Submodule.quotientRel (pi fun x ↦ I))) c =
    Quot.mk (⇑(Submodule.quotientRel I)) a • Quot.mk (⇑(Submodule.quotientRel (pi fun x ↦ I))) c +
      Quot.mk (⇑(Submodule.quotientRel I)) b • Quot.mk (⇑(Submodule.quotientRel (pi fun x ↦ I))) c

Tactic:
exact congr_arg _ (add_smul _ _ _)

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

Goal state before:
pp: R : Type u_1
α : Type u_3
M : Type u_4
inst✝³ : AddCommMonoid M
inst✝² : Semiring R
inst✝¹ : Module R M
a : α
inst✝ : Subsingleton α
m : M
b : α
⊢ ((uniqueLinearEquiv R M a).symm m) b = m

Tactic:
simp [Subsingleton.elim b a]

Goal state after:
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).1 = x 0

Tactic:
prodOfFinsuppNat,

Goal state after:
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
⊢ (((Finsupp.lsum ℕ) fun n ↦ ((inr R P M ∘ₗ f) ^ n) ∘ₗ inl R P M) x).1 = x 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:
prodOfFinsuppNat,

Goal state after:
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
⊢ (((Finsupp.lsum ℕ) fun n ↦ ((inr R P M ∘ₗ f) ^ n) ∘ₗ inl R P M) x).2 =
    f (((Finsupp.lsum ℕ) fun n ↦ ((inr R P M ∘ₗ f) ^ n) ∘ₗ inl R P M) ((comapDomain.addMonoidHom ⋯) x))
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
inj : Injective ⇑f
n : ℕ
ih :
  ∀ m < n,
    ∀ ⦃x y : ℕ →₀ P⦄,
      let s := x.support ∪ y.support;
      ∀ (ne : s.Nonempty), m = s.max' ne → f.prodOfFinsuppNat x = f.prodOfFinsuppNat y → x = y
x y : ℕ →₀ P
s : Finset ℕ := ⋯
ne✝ : s.Nonempty
hn : n = s.max' ne✝
eq : f.prodOfFinsuppNat x = f.prodOfFinsuppNat y
ne : ¬(comapDomain.addMonoidHom ⋯) x = (comapDomain.addMonoidHom ⋯) y
⊢ (((comapDomain.addMonoidHom ⋯) x).support ∪ ((comapDomain.addMonoidHom ⋯) y).support).Nonempty

Tactic:
contrapose! ne

Goal state after:
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
inj : Injective ⇑f
n : ℕ
ih :
  ∀ m < n,
    ∀ ⦃x y : ℕ →₀ P⦄,
      let s := x.support ∪ y.support;
      ∀ (ne : s.Nonempty), m = s.max' ne → f.prodOfFinsuppNat x = f.prodOfFinsuppNat y → x = y
x y : ℕ →₀ P
s : Finset ℕ := x.support ∪ y.support
ne✝ : s.Nonempty
hn : n = s.max' ne✝
eq : f.prodOfFinsuppNat x = f.prodOfFinsuppNat y
ne : ((comapDomain.addMonoidHom ⋯) x).support ∪ ((comapDomain.addMonoidHom ⋯) y).support = ∅
⊢ (comapDomain.addMonoidHom ⋯) x = (comapDomain.addMonoidHom ⋯) y
Module: Mathlib.Order.Filter.Bases.Basic

Goal state before:
pp: α : Type u_1
ι : Sort u_4
l : Filter α
p : ι → Prop
s : ι → Set α
h : l.HasBasis p s
⊢ ⋯.filter = l

Tactic:
ext U
  simp [h.mem_iff, IsBasis.mem_filter_iff]

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

Goal state before:
pp: α : Type u_1
s✝ s : Set α
⊢ s ∈ ⨆ a ∈ s✝, pure a ↔ s ∈ 𝓟 s✝

Tactic:
simp [Set.subset_def]

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

Goal state before:
pp: α : Type u_1
ι : Type u_6
ι' : ι → Type u_7
dom : Set ι
hdom : dom.Nonempty
l : ι → Filter α
s : (i : ι) → ι' i → Set α
p : (i : ι) → ι' i → Prop
hl : ∀ i ∈ dom, (l i).HasBasis (p i) (s i)
h : DirectedOn (l ⁻¹'o GE.ge) dom
⊢ (⨅ i ∈ dom, l i).HasBasis (fun ii' ↦ ii'.fst ∈ dom ∧ p ii'.fst ii'.snd) fun ii' ↦ s ii'.fst ii'.snd

Tactic:
refine ⟨fun t => ?_⟩
  rw [mem_biInf_of_directed h hdom, Sigma.exists]
  grind +splitIndPred

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

Goal state before:
pp: α : Type u_1
β : Type u_2
g₁ g₂ : Filter β
m : α → β
⊢ comap m (g₁ ⊔ g₂) = comap m g₁ ⊔ comap m g₂

Tactic:
by
  rw [sup_eq_iSup, comap_iSup, iSup_bool_eq, Bool.cond_true, Bool.cond_false]

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

Goal state before:
pp: α : Type u_1
β : Type u_2
f : Filter β
m : α → β
hm : Surjective m
⊢ (range m)ᶜ ∈ f ↔ f = ⊥

Tactic:
hm.range_eq,

Goal state after:
α : Type u_1
β : Type u_2
f : Filter β
m : α → β
hm : Surjective m
⊢ univᶜ ∈ f ↔ f = ⊥
Module: Mathlib.Order.Filter.Tendsto

Goal state before:
pp: α : Type u_1
β : Type u_2
f : α → β
s : Set β
l : Filter α
t : Set β
⊢ t ∈ map f (l ⊓ 𝓟 (f ⁻¹' s)) ↔ t ∈ map f l ⊓ 𝓟 s

Tactic:
simp only [mem_map', mem_inf_principal, mem_ofPred_eq, mem_preimage]

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

Goal state before:
pp: α : Type u_1
β : Type u_2
ι : Sort u_4
l : Filter α
p : ι → Prop
s : ι → Set α
f : β → α
hl : l.HasBasis p s
t : Set β
i : ι
⊢ s i ⊆ {y | ∀ ⦃x : β⦄, f x = y → x ∈ t} ↔ f ⁻¹' s i ⊆ t

Tactic:
exact ⟨fun h x hx => h hx rfl, fun h y hy x hx => h <| by rwa [mem_preimage, hx]⟩

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

Goal state before:
pp: α : Type u
s t : Set α
l : Filter α
⊢ s ∩ t =ᶠ[l] t ↔ ∀ᶠ (x : α) in l, x ∈ t → x ∈ s

Tactic:
by
  rw [inter_comm, inter_eventuallyEq_left]

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

Goal state before:
pp: α : Type u_1
β : Type u_2
f : Filter α
m : α → Filter β
p : β → Prop
⊢ (∃ᶠ (y : β) in f.bind m, p y) ↔ ∃ᶠ (x : α) in f, ∃ᶠ (y : β) in m x, p y

Tactic:
rw [← not_iff_not]

Goal state after:
α : Type u_1
β : Type u_2
f : Filter α
m : α → Filter β
p : β → Prop
⊢ (¬∃ᶠ (y : β) in f.bind m, p y) ↔ ¬∃ᶠ (x : α) in f, ∃ᶠ (y : β) in m x, p y
Module: Mathlib.Order.Filter.AtTopBot.Basic

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

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

Goal state after:
Module: Mathlib.Algebra.GroupWithZero.Action.TransferInstance

Goal state before:
pp: M : Type u_1
M₀ : Type u_2
A : Type u_3
B : Type u_4
e : A ≃ B
inst✝¹ : Zero B
inst✝ : SMulZeroClass M B
this : Zero A := e.zero
⊢ SMulZeroClass M A

Tactic:
exact {
    e.smul M with
    smul_zero := by simp [smul_def, zero_def]
  }

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

Goal state before:
pp: case mpr
A : Type u
inst✝² : Semiring A
M : Type v
inst✝¹ : AddCommMonoid M
inst✝ : Module A M
N : Submodule A M
G : Type w
w✝ : Finite G
g : G → M
hg : span A (range g) = N
⊢ N.FG

Tactic:
have := Fintype.ofFinite (range g)

Goal state after:
case mpr
A : Type u
inst✝² : Semiring A
M : Type v
inst✝¹ : AddCommMonoid M
inst✝ : Module A M
N : Submodule A M
G : Type w
w✝ : Finite G
g : G → M
hg : span A (range g) = N
this : Fintype ↑(range g)
⊢ N.FG
Module: Mathlib.RingTheory.Finiteness.Defs

Goal state before:
pp: R : Type u_1
M : Type u_2
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
s : Set M
⊢ (span R s).FG ↔ ∃ s', ↑s' ⊆ s ∧ span R s = span R ↑s'

Tactic:
by
  constructor
  · intro ⟨s'', hs''⟩
    obtain ⟨s', hs's, hss'⟩ := subset_span_finite_of_subset_span <| hs'' ▸ subset_span
    refine ⟨s', hs's, ?_⟩
    apply le_antisymm
    · rwa [← hs'', span_le]
    · rw [span_le]
      exact le_trans hs's subset_span
  · intro ⟨s', _, h⟩
    exact ⟨s', h.symm⟩

Goal state after:
Module: Mathlib.Order.Cofinal

Goal state before:
pp: α : Type u_1
inst✝¹ : LE α
inst✝ : Nonempty α
s : Set α
hs : IsCofinal s
⊢ s.Nonempty

Tactic:
inhabit α
  exact (hs default).imp fun _ ↦ And.left

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

Goal state before:
pp: case empty
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) ⋯
⊢ motive (span R ↑∅) ⋯

Tactic:
simp [bot]

Goal state after:
Module: Mathlib.Order.DirSupClosed

Goal state before:
pp: α : Type u_1
D : Set (Set α)
inst✝ : Preorder α
ι : Sort u_2
f : ι → Set α
hs : ∀ (i : ι), DirSupClosedOn D (f i)
⊢ DirSupClosedOn D (⋂ i, f i)

Tactic:
rw [← sInter_range f]
  exact DirSupClosedOn.sInter (by simpa)

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

Goal state before:
pp: R : Type u_1
M : Type u_4
inst✝⁶ : Semiring R
inst✝⁵ : AddCommMonoid M
inst✝⁴ : Module R M
S : Type u_7
P : Type u_6
inst✝³ : Semiring S
inst✝² : AddCommMonoid P
inst✝¹ : Module S P
σ : R →+* S
inst✝ : RingHomSurjective σ
f : M →ₛₗ[σ] P
hf : Function.Bijective ⇑f
x✝ : Module.Finite S P
⊢ f.range.FG

Tactic:
LinearMap.range_eq_top.mpr hf.surjective,

Goal state after:
R : Type u_1
M : Type u_4
inst✝⁶ : Semiring R
inst✝⁵ : AddCommMonoid M
inst✝⁴ : Module R M
S : Type u_7
P : Type u_6
inst✝³ : Semiring S
inst✝² : AddCommMonoid P
inst✝¹ : Module S P
σ : R →+* S
inst✝ : RingHomSurjective σ
f : M →ₛₗ[σ] P
hf : Function.Bijective ⇑f
x✝ : Module.Finite S P
⊢ ⊤.FG
Module: Mathlib.SetTheory.Ordinal.Arithmetic

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
r : α → α → Prop
s : β → β → Prop
t : γ → γ → Prop
a b c : Ordinal.{u}
x✝² x✝¹ x✝ : WellOrder
⊢ ∀ {a b : (x✝.α × x✝¹.α) × x✝².α},
    Prod.Lex x✝.r (Prod.Lex x✝¹.r x✝².r) ((prodAssoc x✝.α x✝¹.α x✝².α) a) ((prodAssoc x✝.α x✝¹.α x✝².α) b) ↔
      Prod.Lex (Prod.Lex x✝.r x✝¹.r) x✝².r a b

Tactic:
by grind [Prod.mk.injEq]

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

Goal state before:
pp: a b : Ordinal.{u_4}
hb : 0 < b
⊢ a = 1 * a

Tactic:
rw [one_mul a]

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

Goal state before:
pp: case neg
β : Type u_3
inst✝¹ : LinearOrder β
inst✝ : NoMaxOrder β
f : β → Ordinal.{u}
hf : StrictMono f
hf' : ¬BddAbove (range f)
⊢ ⨆ i, f i + 1 ≤ ⨆ i, f i

Tactic:
rw [ciSup_of_not_bddAbove hf', ciSup_of_not_bddAbove]

Goal state after:
case neg
β : Type u_3
inst✝¹ : LinearOrder β
inst✝ : NoMaxOrder β
f : β → Ordinal.{u}
hf : StrictMono f
hf' : ¬BddAbove (range f)
⊢ ¬BddAbove (range fun i ↦ f i + 1)
Module: Mathlib.SetTheory.Ordinal.Enum

Goal state before:
pp: s t : Set Ordinal.{u}
hs : ¬BddAbove s
hst : s ⊆ t
a : Ordinal.{u}
⊢ enumOrd t a ≤ enumOrd s a

Tactic:
rw [enumOrd, enumOrd]

Goal state after:
s t : Set Ordinal.{u}
hs : ¬BddAbove s
hst : s ⊆ t
a : Ordinal.{u}
⊢ sInf (t ∩ {b | ∀ c < a, enumOrd t c < b}) ≤ sInf (s ∩ {b | ∀ c < a, enumOrd s c < b})
Module: Mathlib.SetTheory.Ordinal.Family

Goal state before:
pp: f : (a : Ordinal.{u_3}) → a < 1 → Ordinal.{max u_3 u_4}
⊢ bsup 1 f = f 0 ⋯

Tactic:
by
  simp_rw [← iSup_eq_bsup, ciSup_unique, familyOfBFamily, familyOfBFamily', typein_one_toType]

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

Goal state before:
pp: case a
a c : Ordinal.{u_4}
hc : c < a
b d : Ordinal.{u_4}
hd : d ≠ 0
H : a * d ≠ 0
⊢ b / d ≤ (a * b + c) / (a * d)

Tactic:
← mul_le_iff_le_div H,

Goal state after:
case a
a c : Ordinal.{u_4}
hc : c < a
b d : Ordinal.{u_4}
hd : d ≠ 0
H : a * d ≠ 0
⊢ a * d * (b / d) ≤ a * b + c
Module: Mathlib.Data.Nat.Log

Goal state before:
pp: b : ℕ
⊢ Monotone (log b)

Tactic:
refine monotone_nat_of_le_succ fun n => ?_

Goal state after:
b n : ℕ
⊢ log b n ≤ log b (n + 1)
Module: Mathlib.SetTheory.Ordinal.Arithmetic

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
r : α → α → Prop
s : β → β → Prop
t : γ → γ → Prop
⊢ CharZero Ordinal.{u_4}

Tactic:
refine ⟨fun a b h ↦ ?_⟩
  rwa [← Cardinal.ord_natCast, ← Cardinal.ord_natCast, Cardinal.ord_inj, Nat.cast_inj] at h

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

Goal state before:
pp: ⊢ IsSuccLimit ω

Tactic:
rw [isSuccLimit_iff, isSuccPrelimit_iff_succ_lt]

Goal state after:
⊢ ω ≠ 0 ∧ ∀ a < ω, succ a < ω
Module: Mathlib.SetTheory.Ordinal.Principal

Goal state before:
pp: o : Ordinal.{u}
ho₁ : 1 < o
ho : IsPrincipal (fun x1 x2 ↦ x1 + x2) o
⊢ IsSuccLimit o

Tactic:
rw [isSuccLimit_iff, isSuccPrelimit_iff_succ_lt]

Goal state after:
o : Ordinal.{u}
ho₁ : 1 < o
ho : IsPrincipal (fun x1 x2 ↦ x1 + x2) o
⊢ o ≠ 0 ∧ ∀ a < o, succ a < o
Module: Mathlib.SetTheory.Ordinal.Principal

Goal state before:
pp: case refine_1.inr
o : Ordinal.{u}
ho : IsPrincipal (fun x1 x2 ↦ x1 + x2) o
a : Ordinal.{u}
hao : a < o
ho₁ : o ≤ 1
⊢ a + o = o

Tactic:
cases le_one_iff.1 ho₁ <;> simp_all

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

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

Tactic:
rw [← one_le_iff_pos] at hb₁'

Goal state after:
case inr.inr
a b : Ordinal.{u}
hb₁ : b ≠ 1
hb : IsPrincipal (fun x1 x2 ↦ x1 + x2) b
h✝ : 0 < a
hb₁' : 1 ≤ b
⊢ IsPrincipal (fun x1 x2 ↦ x1 + x2) (a * b)
Module: Mathlib.SetTheory.Cardinal.Arithmetic

Goal state before:
pp: case inl
a b : Cardinal.{u_1}
ha : ℵ₀ ≤ a
⊢ a + b ≤ max (max a b) ℵ₀

Tactic:
rw [add_eq_max ha]

Goal state after:
case inl
a b : Cardinal.{u_1}
ha : ℵ₀ ≤ a
⊢ max a b ≤ max (max a b) ℵ₀
Module: Mathlib.SetTheory.Cardinal.Cofinality.Ordinal

Goal state before:
pp: f : Ordinal.{u_1} → Ordinal.{u_1}
hf : IsNormal f
a : Ordinal.{u_1}
⊢ a.cof ≤ (f a).cof

Tactic:
by
  cases a using limitRecOn with
  | zero => simp
  | add_one a =>
    rw [cof_add_one, Cardinal.one_le_iff_ne_zero, cof_eq_zero.ne]
    exact (hf.strictMono (lt_succ a)).ne_zero
  | limit a ha => rw [cof_map_of_isNormal hf ha]

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

Goal state before:
pp: o : Ordinal.{u}
⊢ (succ o).IsFundamentalSequence 1 fun x x_1 ↦ o

Tactic:
refine ⟨?_, @fun i j hi hj h => ?_, blsub_const Ordinal.one_ne_zero o⟩
  · rw [cof_succ, ord_one]
  · rw [lt_one_iff_zero] at hi hj
    rw [hi, hj] at h
    exact h.false.elim

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

Goal state before:
pp: o : Ordinal.{u}
⊢ o.cof = sInf {a | ∃ ι f, lsub f = o ∧ #ι = a}

Tactic:
by
  refine le_antisymm (le_csInf (cof_lsub_def_nonempty o) ?_) (csInf_le' ?_)
  · rintro a ⟨ι, f, hf, rfl⟩
    rw [← hf]
    exact cof_iSup_add_one_le f
  · rcases Order.cof_eq (α := o.ToType) with ⟨S, hS, hS'⟩
    let f : S → Ordinal := fun s => typein LT.lt s.val
    refine ⟨S, f, le_antisymm (lsub_le fun i => typein_lt_self (o := o) i)
      (le_of_forall_lt fun a ha => ?_), by rwa [cof_toType] at hS'⟩
    rw [← type_toType o] at ha
    rcases hS (enum (· < ·) ⟨a, ha⟩) with ⟨b, hb, hb'⟩
    rw [← not_lt, ← typein_le_typein, typein_enum] at hb'
    exact hb'.trans_lt (lt_lsub.{u, u} f ⟨b, hb⟩)

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

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

Tactic:
lift_lift

Goal state after:
α : Type u
β' : Type v
inst✝ : Infinite α
lle : lift.{u, v} #β' ≤ lift.{v, u} #α
⊢ lift.{max u v, u} #α = lift.{max v u, u} #α + lift.{u, v} #β'
Module: Mathlib.Data.Finsupp.ToDFinsupp

Goal state before:
pp: ι : Type u_1
η : ι → Type u_4
N : Type u_5
inst✝² : DecidableEq ι
inst✝¹ : Zero N
inst✝ : (i : ι) → (x : η i →₀ N) → Decidable (x ≠ 0)
f : (i : ι) × η i →₀ N
a✝ : ι
⊢ a✝ ∈ (sigmaFinsuppEquivDFinsupp f).support ↔ a✝ ∈ f.splitSupport

Tactic:
rw [DFinsupp.mem_support_toFun]

Goal state after:
ι : Type u_1
η : ι → Type u_4
N : Type u_5
inst✝² : DecidableEq ι
inst✝¹ : Zero N
inst✝ : (i : ι) → (x : η i →₀ N) → Decidable (x ≠ 0)
f : (i : ι) × η i →₀ N
a✝ : ι
⊢ (sigmaFinsuppEquivDFinsupp f) a✝ ≠ 0 ↔ a✝ ∈ f.splitSupport
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₁
f : Dual R M₁
⊢ (dualMap f).range = R ∙ f

Tactic:
ext m
  rw [Submodule.mem_span_singleton]
  refine ⟨fun ⟨r, hr⟩ ↦ ⟨r 1, ?_⟩, fun ⟨r, hr⟩ ↦ ⟨r • LinearMap.id, ?_⟩⟩
  · ext; simp [dualMap_apply', ← hr]
  · ext; simp [dualMap_apply', ← hr]

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

Goal state before:
pp: R : Type u_1
M : Type u_2
M' : Type u_3
inst✝⁴ : CommSemiring R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
inst✝¹ : AddCommMonoid M'
inst✝ : Module R M'
B : M →ₗ[R] M' →ₗ[R] R
⊢ B.range.dualCoannihilator = B.flip.ker

Tactic:
ext x; simp [LinearMap.ext_iff (f := B.flip x)]

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

Goal state before:
pp: case refine_1
R : Type u_2
M : Type u_4
inst✝² : Ring R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
x y : M
u v : R
hu : IsUnit u
hv : IsUnit v
s t : R
h : (s * ↑hu.unit⁻¹) • u • x + (t * ↑hv.unit⁻¹) • v • y = 0 → s * ↑hu.unit⁻¹ = 0 ∧ t * ↑hv.unit⁻¹ = 0
hst : s • x + t • y = 0
⊢ s = 0 ∧ t = 0

Tactic:
simp only [Units.mul_left_eq_zero] at h

Goal state after:
case refine_1
R : Type u_2
M : Type u_4
inst✝² : Ring R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
x y : M
u v : R
hu : IsUnit u
hv : IsUnit v
s t : R
hst : s • x + t • y = 0
h : (s * ↑hu.unit⁻¹) • u • x + (t * ↑hv.unit⁻¹) • v • y = 0 → s = 0 ∧ t = 0
⊢ s = 0 ∧ t = 0
Module: Mathlib.LinearAlgebra.LinearIndependent.Lemmas

Goal state before:
pp: case refine_2
R : Type u_2
M : Type u_4
inst✝² : Ring R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
x y : M
u v : R
hu : IsUnit u
hv : IsUnit v
s t : R
h : (s * ↑hu.unit) • x + (t * ↑hv.unit) • y = 0 → s * ↑hu.unit = 0 ∧ t * ↑hv.unit = 0
hst : s • u • x + t • v • y = 0
⊢ s = 0 ∧ t = 0

Tactic:
simp only [Units.mul_left_eq_zero] at h

Goal state after:
case refine_2
R : Type u_2
M : Type u_4
inst✝² : Ring R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
x y : M
u v : R
hu : IsUnit u
hv : IsUnit v
s t : R
hst : s • u • x + t • v • y = 0
h : (s * ↑hu.unit) • x + (t * ↑hv.unit) • y = 0 → s = 0 ∧ t = 0
⊢ s = 0 ∧ t = 0
Module: Mathlib.LinearAlgebra.Isomorphisms

Goal state before:
pp: R : Type u_1
M : Type u_2
M₂ : Type u_3
M₃ : Type u_4
inst✝⁶ : Ring R
inst✝⁵ : AddCommGroup M
inst✝⁴ : AddCommGroup M₂
inst✝³ : AddCommGroup M₃
inst✝² : Module R M
inst✝¹ : Module R M₂
inst✝ : Module R M₃
f : M →ₗ[R] M₂
S T : Submodule R M
h✝ h : S ≤ T
x : M
hx : x ∈ ↑T
⊢ (S.mapQ T LinearMap.id h) (S.mkQ x) = 0

Tactic:
mkQ_apply,

Goal state after:
R : Type u_1
M : Type u_2
M₂ : Type u_3
M₃ : Type u_4
inst✝⁶ : Ring R
inst✝⁵ : AddCommGroup M
inst✝⁴ : AddCommGroup M₂
inst✝³ : AddCommGroup M₃
inst✝² : Module R M
inst✝¹ : Module R M₂
inst✝ : Module R M₃
f : M →ₗ[R] M₂
S T : Submodule R M
h✝ h : S ≤ T
x : M
hx : x ∈ ↑T
⊢ (S.mapQ T LinearMap.id h) (Quotient.mk x) = 0
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
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
⊢ (a * d) • t = a • d • t

Tactic:
rw [mul_smul]

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

Goal state before:
pp: case right
ι : Type u'
R : Type u_2
M : Type u_4
inst✝² : Ring R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
v : ι → M
I : Set ι
hIlinind : LinearIndepOn R v I
i : ι
hi : i ∉ I
J : Set ι := I ∪ {i}
hImaximal : LinearIndepOn R v J → I = J
hJ : J = I ∪ {i}
memJ : ∀ {x : ι}, x ∈ J ↔ x = i ∨ x ∈ I
hiJ : i ∈ J
h : ¬LinearIndepOn R v J
f : ι →₀ R
supp_f : f ∈ Finsupp.supported R R J
sum_f : ∑ i ∈ f.support, f i • v i = 0
f_ne : f ≠ 0
⊢ ∃ a, a ≠ 0 ∧ a • v i ∈ span R (v '' I)

Tactic:
have hfi : f i ≠ 0 := by
      contrapose hIlinind
      refine linearDepOn_iff.mpr ⟨f, ?_, sum_f, f_ne⟩
      simp only [Finsupp.mem_supported, hJ] at supp_f ⊢
      rintro x hx
      refine (memJ.mp (supp_f hx)).resolve_left ?_
      rintro rfl
      exact (Finsupp.mem_support_iff.mp hx) hIlinind

Goal state after:
case right
ι : Type u'
R : Type u_2
M : Type u_4
inst✝² : Ring R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
v : ι → M
I : Set ι
hIlinind : LinearIndepOn R v I
i : ι
hi : i ∉ I
J : Set ι := I ∪ {i}
hImaximal : LinearIndepOn R v J → I = J
hJ : J = I ∪ {i}
memJ : ∀ {x : ι}, x ∈ J ↔ x = i ∨ x ∈ I
hiJ : i ∈ J
h : ¬LinearIndepOn R v J
f : ι →₀ R
supp_f : f ∈ Finsupp.supported R R J
sum_f : ∑ i ∈ f.support, f i • v i = 0
f_ne : f ≠ 0
hfi : f i ≠ 0
⊢ ∃ a, a ≠ 0 ∧ a • v i ∈ span R (v '' I)