mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.SetTheory.Ordinal.Principal

Goal state before:
pp: b o : Ordinal.{u}
hb : 1 < b
ho : IsPrincipal (fun x1 x2 ↦ x1 * x2) (b ^ o)
⊢ IsPrincipal (fun x1 x2 ↦ x1 + x2) o

Tactic:
intro x y hx hy
  have := ho ((opow_lt_opow_iff_right hb).2 hx) ((opow_lt_opow_iff_right hb).2 hy)
  dsimp only at *
  rwa [← opow_add, opow_lt_opow_iff_right hb] at this

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

Goal state before:
pp: γ : Type u
inst✝¹ : LinearOrder γ
inst✝ : NoMaxOrder γ
f : γ → Ordinal.{u}
hf : StrictMono f
⊢ (⨆ i, f i).cof = Order.cof γ

Tactic:
simpa using lift_cof_iSup hf

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

Goal state before:
pp: case refine_1
a b : Cardinal.{u_1}
h : a + b = a
⊢ ℵ₀ ≤ a ∧ b ≤ a ∨ b = 0

Tactic:
rcases le_or_gt ℵ₀ a with ha | ha
    · left
      use ha
      rw [← not_lt]
      apply fun hb => ne_of_gt _ h
      intro hb
      exact hb.trans_le (self_le_add_left b a)
    right
    rw [← h, add_lt_aleph0_iff, lt_aleph0, lt_aleph0] at ha
    rcases ha with ⟨⟨n, rfl⟩, ⟨m, rfl⟩⟩
    norm_cast at h ⊢
    rw [← add_right_inj, h, add_zero]

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

Goal state before:
pp: α : Type u_1
inst✝¹ : LinearOrder α
inst✝ : WellFoundedLT α
i : α
h : (#α).ord = typeLT α
hα : ℵ₀ ≤ #α
⊢ #↑(insert i (Iio i)) < #α

Tactic:
mk_insert self_notMem_Iio

Goal state after:
α : Type u_1
inst✝¹ : LinearOrder α
inst✝ : WellFoundedLT α
i : α
h : (#α).ord = typeLT α
hα : ℵ₀ ≤ #α
⊢ #↑(Iio i) + 1 < #α
Module: Mathlib.SetTheory.Cardinal.Aleph

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

Tactic:
by
  simpa using lift_lt (b := ω₁)

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

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

Tactic:
grw [le_ciSup hf i]

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

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

Tactic:
obtain ⟨n, rfl⟩ := lt_aleph0.1 hc

Goal state after:
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).card ≤ ↑n
Module: Mathlib.SetTheory.Ordinal.FundamentalSequence

Goal state before:
pp: f : Ordinal.{u} → Ordinal.{u}
hf : IsNormal f
a o : Ordinal.{u}
ha : IsSuccLimit a
g : (b : Ordinal.{u}) → b < o → Ordinal.{u}
hg : a.IsFundamentalSequence o g
⊢ (f a).IsFundamentalSequence o fun b hb ↦ f (g b hb)

Tactic:
by
  refine ⟨?_, @fun i j _ _ h => hf.strictMono (hg.2.1 _ _ h), ?_⟩
  · grind [Ordinal.IsFundamentalSequence, cof_map_of_isNormal]
  · rw [@blsub_comp.{u, u, u} a _ (fun b _ => f b) (@fun i j _ _ h => hf.strictMono.monotone h) g
        hg.2.2]
    exact IsNormal.blsub_eq.{u, u} hf ha

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

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

Tactic:
exact fun c' hc' => (power_lt_aleph0 h hc').le.trans (le_max_right _ _)

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

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

Tactic:
conv_rhs => rw [← mk_bounded_subset h hr]

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

Goal state before:
pp: case inl
c : Cardinal.{u_1}
hc : c < ℵ₀
⊢ ¬(succ c).IsSingular

Tactic:
obtain ⟨n, rfl⟩ := lt_aleph0.1 hc

Goal state after:
case inl
n : ℕ
hc : ↑n < ℵ₀
⊢ ¬(succ ↑n).IsSingular
Module: Mathlib.Data.DFinsupp.Defs

Goal state before:
pp: ι : Type u
γ : Type w
β : ι → Type v
β₁ : ι → Type v₁
β₂ : ι → Type v₂
inst✝¹ : (i : ι) → Zero (β i)
p : ι → Prop
inst✝ : DecidablePred p
x : Π₀ (i : ι), β i
xs : { s // ∀ (i : ι), i ∈ s ∨ x.toFun i = 0 }
i : ι
H : x i = 0
⊢ (if p i then x i else 0) = 0

Tactic:
by simp only [H, ite_self]

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

Goal state before:
pp: case neg
ι : Type u
β : ι → Type v
inst✝¹ : (i : ι) → Zero (β i)
inst✝ : DecidableEq ι
i j : ι
xi : β i
xj : β j
h : single i xi = single j xj
hij : ¬i = j
h_coe : ⇑(single i xi) = ⇑(single j xj)
hci : (single i xi) i = (single j xj) i
hcj : (single i xi) j = (single j xj) j
⊢ i = j ∧ xi ≍ xj ∨ xi = 0 ∧ xj = 0

Tactic:
rw [DFinsupp.single_eq_same] at hci hcj

Goal state after:
case neg
ι : Type u
β : ι → Type v
inst✝¹ : (i : ι) → Zero (β i)
inst✝ : DecidableEq ι
i j : ι
xi : β i
xj : β j
h : single i xi = single j xj
hij : ¬i = j
h_coe : ⇑(single i xi) = ⇑(single j xj)
hci : xi = (single j xj) i
hcj : (single i xi) j = xj
⊢ i = j ∧ xi ≍ xj ∨ xi = 0 ∧ xj = 0
Module: Mathlib.Data.Finsupp.ToDFinsupp

Goal state before:
pp: ι : Type u_1
M : Type u_3
inst✝¹ : DecidableEq ι
inst✝ : Zero M
i : ι
m : M
i✝ : ι
⊢ (single i m).toDFinsupp i✝ = (DFinsupp.single i m) i✝

Tactic:
simp [Finsupp.single_apply, DFinsupp.single_apply]

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

Goal state before:
pp: ι : Type u_1
M : Type u_3
inst✝² : DecidableEq ι
inst✝¹ : Zero M
inst✝ : (m : M) → Decidable (m ≠ 0)
i : ι
m : M
a✝ : ι
⊢ (single i m).toFinsupp a✝ = (Finsupp.single i m) a✝

Tactic:
simp [Finsupp.single_apply, DFinsupp.single_apply]

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

Goal state before:
pp: ι : Type u
γ : Type w
β : ι → Type v
β₁ : ι → Type v₁
β₂ : ι → Type v₂
inst✝² : (i : ι) → AddZeroClass (β i)
inst✝¹ : (i : ι) → AddZeroClass (β₁ i)
inst✝ : (i : ι) → AddZeroClass (β₂ i)
e : (i : ι) → β₁ i ≃+ β₂ i
x : Π₀ (i : ι), β₁ i
⊢ mapRange (fun i ↦ (fun x ↦ (e i).symm x) ∘ fun x ↦ (e i) x) ?h x = x

Tactic:
AddEquiv.symm_comp_self

Goal state after:
ι : Type u
γ : Type w
β : ι → Type v
β₁ : ι → Type v₁
β₂ : ι → Type v₂
inst✝² : (i : ι) → AddZeroClass (β i)
inst✝¹ : (i : ι) → AddZeroClass (β₁ i)
inst✝ : (i : ι) → AddZeroClass (β₂ i)
e : (i : ι) → β₁ i ≃+ β₂ i
x : Π₀ (i : ι), β₁ i
⊢ mapRange (fun i ↦ id) ⋯ x = x
Module: Mathlib.Data.DFinsupp.Defs

Goal state before:
pp: case h
ι : Type u
γ : Type w
β : ι → Type v
β₁ : ι → Type v₁
β₂ : ι → Type v₂
inst✝² : (i : ι) → AddZeroClass (β i)
inst✝¹ : (i : ι) → AddZeroClass (β₁ i)
inst✝ : (i : ι) → AddZeroClass (β₂ i)
e : (i : ι) → β₁ i ≃+ β₂ i
x : Π₀ (i : ι), β₁ i
⊢ ∀ (i : ι), ((fun x ↦ (e i).symm x) ∘ fun x ↦ (e i) x) 0 = 0

Tactic:
AddEquiv.symm_comp_self

Goal state after:
case h
ι : Type u
γ : Type w
β : ι → Type v
β₁ : ι → Type v₁
β₂ : ι → Type v₂
inst✝² : (i : ι) → AddZeroClass (β i)
inst✝¹ : (i : ι) → AddZeroClass (β₁ i)
inst✝ : (i : ι) → AddZeroClass (β₂ i)
e : (i : ι) → β₁ i ≃+ β₂ i
x : Π₀ (i : ι), β₁ i
⊢ ∀ (i : ι), id 0 = 0
Module: Mathlib.LinearAlgebra.LinearIndependent.Lemmas

Goal state before:
pp: ι : Type u'
ι' : Type u_1
R : Type u_2
M : Type u_4
M' : Type u_5
inst✝⁴ : Semiring R
inst✝³ : AddCommMonoid M
inst✝² : AddCommMonoid M'
inst✝¹ : Module R M
inst✝ : Module R M'
v : ι → M
v' : ι' → M'
hv : LinearIndependent R v
hv' : LinearIndependent R v'
⊢ linearCombination R (Sum.elim (⇑(inl R M M') ∘ v) (⇑(inr R M M') ∘ v')) =
    (linearCombination R v).prodMap (linearCombination R v') ∘ₗ ↑(sumFinsuppLEquivProdFinsupp R)

Tactic:
ext (_ | _)

Goal state after:
case inl.fst
ι : Type u'
ι' : Type u_1
R : Type u_2
M : Type u_4
M' : Type u_5
inst✝⁴ : Semiring R
inst✝³ : AddCommMonoid M
inst✝² : AddCommMonoid M'
inst✝¹ : Module R M
inst✝ : Module R M'
v : ι → M
v' : ι' → M'
hv : LinearIndependent R v
hv' : LinearIndependent R v'
val✝ : ι
⊢ ((linearCombination R (Sum.elim (⇑(inl R M M') ∘ v) (⇑(inr R M M') ∘ v')) ∘ₗ lsingle (Sum.inl val✝)) 1).1 =
    ((((linearCombination R v).prodMap (linearCombination R v') ∘ₗ ↑(sumFinsuppLEquivProdFinsupp R)) ∘ₗ
          lsingle (Sum.inl val✝))
        1).1

case inl.snd
ι : Type u'
ι' : Type u_1
R : Type u_2
M : Type u_4
M' : Type u_5
inst✝⁴ : Semiring R
inst✝³ : AddCommMonoid M
inst✝² : AddCommMonoid M'
inst✝¹ : Module R M
inst✝ : Module R M'
v : ι → M
v' : ι' → M'
hv : LinearIndependent R v
hv' : LinearIndependent R v'
val✝ : ι
⊢ ((linearCombination R (Sum.elim (⇑(inl R M M') ∘ v) (⇑(inr R M M') ∘ v')) ∘ₗ lsingle (Sum.inl val✝)) 1).2 =
    ((((linearCombination R v).prodMap (linearCombination R v') ∘ₗ ↑(sumFinsuppLEquivProdFinsupp R)) ∘ₗ
          lsingle (Sum.inl val✝))
        1).2

case inr.fst
ι : Type u'
ι' : Type u_1
R : Type u_2
M : Type u_4
M' : Type u_5
inst✝⁴ : Semiring R
inst✝³ : AddCommMonoid M
inst✝² : AddCommMonoid M'
inst✝¹ : Module R M
inst✝ : Module R M'
v : ι → M
v' : ι' → M'
hv : LinearIndependent R v
hv' : LinearIndependent R v'
val✝ : ι'
⊢ ((linearCombination R (Sum.elim (⇑(inl R M M') ∘ v) (⇑(inr R M M') ∘ v')) ∘ₗ lsingle (Sum.inr val✝)) 1).1 =
    ((((linearCombination R v).prodMap (linearCombination R v') ∘ₗ ↑(sumFinsuppLEquivProdFinsupp R)) ∘ₗ
          lsingle (Sum.inr val✝))
        1).1

case inr.snd
ι : Type u'
ι' : Type u_1
R : Type u_2
M : Type u_4
M' : Type u_5
inst✝⁴ : Semiring R
inst✝³ : AddCommMonoid M
inst✝² : AddCommMonoid M'
inst✝¹ : Module R M
inst✝ : Module R M'
v : ι → M
v' : ι' → M'
hv : LinearIndependent R v
hv' : LinearIndependent R v'
val✝ : ι'
⊢ ((linearCombination R (Sum.elim (⇑(inl R M M') ∘ v) (⇑(inr R M M') ∘ v')) ∘ₗ lsingle (Sum.inr val✝)) 1).2 =
    ((((linearCombination R v).prodMap (linearCombination R v') ∘ₗ ↑(sumFinsuppLEquivProdFinsupp R)) ∘ₗ
          lsingle (Sum.inr val✝))
        1).2
Module: Mathlib.LinearAlgebra.DFinsupp

Goal state before:
pp: ι : Type u_1
R : Type u_3
N : Type u_6
inst✝² : Semiring R
inst✝¹ : AddCommMonoid N
inst✝ : Module R N
s : Finset ι
p : ι → Submodule R N
a : N
μ : (i : ι) → ↥(p i)
hμ : ∑ i ∈ s, ↑(μ i) = a
x : ι
hx : x ∈ s
⊢ ↑((DFinsupp.mk s fun i ↦ ⟨↑(μ ↑i), ⋯⟩) x) = ↑(μ x)

Tactic:
rw [mk_of_mem hx]

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

Goal state before:
pp: R : Type u_2
M : Type u_4
M' : Type u_5
inst✝⁴ : Semiring R
inst✝³ : AddCommMonoid M
inst✝² : AddCommMonoid M'
inst✝¹ : Module R M
inst✝ : Module R M'
s : Set M
t : Set M'
hs : LinearIndependent R fun (x : ↑s) ↦ ↑x
ht : LinearIndependent R fun (x : ↑t) ↦ ↑x
a✝ : Nontrivial R
e : ↑s ⊕ ↑t ≃ ↑(⇑(inl R M M') '' s ∪ ⇑(inr R M M') '' t) :=
  Equiv.ofBijective (Sum.elim (fun i ↦ ⟨(inl R M M') ↑i, ⋯⟩) fun i ↦ ⟨(inr R M M') ↑i, ⋯⟩) ⋯
⊢ (fun x ↦ ↑x) ∘ ⇑e = Sum.elim (⇑(inl R M M') ∘ fun x ↦ ↑x) (⇑(inr R M M') ∘ fun x ↦ ↑x)

Tactic:
ext (_ | _)

Goal state after:
case inl.fst
R : Type u_2
M : Type u_4
M' : Type u_5
inst✝⁴ : Semiring R
inst✝³ : AddCommMonoid M
inst✝² : AddCommMonoid M'
inst✝¹ : Module R M
inst✝ : Module R M'
s : Set M
t : Set M'
hs : LinearIndependent R fun (x : ↑s) ↦ ↑x
ht : LinearIndependent R fun (x : ↑t) ↦ ↑x
a✝ : Nontrivial R
e : ↑s ⊕ ↑t ≃ ↑(⇑(inl R M M') '' s ∪ ⇑(inr R M M') '' t) := ⋯
val✝ : ↑s
⊢ (((fun x ↦ ↑x) ∘ ⇑e) (Sum.inl val✝)).1 =
    (Sum.elim (⇑(inl R M M') ∘ fun x ↦ ↑x) (⇑(inr R M M') ∘ fun x ↦ ↑x) (Sum.inl val✝)).1

case inl.snd
R : Type u_2
M : Type u_4
M' : Type u_5
inst✝⁴ : Semiring R
inst✝³ : AddCommMonoid M
inst✝² : AddCommMonoid M'
inst✝¹ : Module R M
inst✝ : Module R M'
s : Set M
t : Set M'
hs : LinearIndependent R fun (x : ↑s) ↦ ↑x
ht : LinearIndependent R fun (x : ↑t) ↦ ↑x
a✝ : Nontrivial R
e : ↑s ⊕ ↑t ≃ ↑(⇑(inl R M M') '' s ∪ ⇑(inr R M M') '' t) := ⋯
val✝ : ↑s
⊢ (((fun x ↦ ↑x) ∘ ⇑e) (Sum.inl val✝)).2 =
    (Sum.elim (⇑(inl R M M') ∘ fun x ↦ ↑x) (⇑(inr R M M') ∘ fun x ↦ ↑x) (Sum.inl val✝)).2

case inr.fst
R : Type u_2
M : Type u_4
M' : Type u_5
inst✝⁴ : Semiring R
inst✝³ : AddCommMonoid M
inst✝² : AddCommMonoid M'
inst✝¹ : Module R M
inst✝ : Module R M'
s : Set M
t : Set M'
hs : LinearIndependent R fun (x : ↑s) ↦ ↑x
ht : LinearIndependent R fun (x : ↑t) ↦ ↑x
a✝ : Nontrivial R
e : ↑s ⊕ ↑t ≃ ↑(⇑(inl R M M') '' s ∪ ⇑(inr R M M') '' t) := ⋯
val✝ : ↑t
⊢ (((fun x ↦ ↑x) ∘ ⇑e) (Sum.inr val✝)).1 =
    (Sum.elim (⇑(inl R M M') ∘ fun x ↦ ↑x) (⇑(inr R M M') ∘ fun x ↦ ↑x) (Sum.inr val✝)).1

case inr.snd
R : Type u_2
M : Type u_4
M' : Type u_5
inst✝⁴ : Semiring R
inst✝³ : AddCommMonoid M
inst✝² : AddCommMonoid M'
inst✝¹ : Module R M
inst✝ : Module R M'
s : Set M
t : Set M'
hs : LinearIndependent R fun (x : ↑s) ↦ ↑x
ht : LinearIndependent R fun (x : ↑t) ↦ ↑x
a✝ : Nontrivial R
e : ↑s ⊕ ↑t ≃ ↑(⇑(inl R M M') '' s ∪ ⇑(inr R M M') '' t) := ⋯
val✝ : ↑t
⊢ (((fun x ↦ ↑x) ∘ ⇑e) (Sum.inr val✝)).2 =
    (Sum.elim (⇑(inl R M M') ∘ fun x ↦ ↑x) (⇑(inr R M M') ∘ fun x ↦ ↑x) (Sum.inr val✝)).2
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
⊢ map S.mkQ T ≤ (S.mapQ T LinearMap.id h).ker

Tactic:
rintro _ ⟨x, hx, rfl⟩

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.mkQ x ∈ (S.mapQ T LinearMap.id h).ker
Module: Mathlib.Algebra.Group.AddChar

Goal state before:
pp: R : Type u_1
M : Type u_2
inst✝¹ : Ring R
inst✝ : CommMonoid M
ψ : AddChar R M
n : ℕ
x : R
⊢ (ψ ^ n) x = (ψ.mulShift ↑n) x

Tactic:
pow_apply,

Goal state after:
R : Type u_1
M : Type u_2
inst✝¹ : Ring R
inst✝ : CommMonoid M
ψ : AddChar R M
n : ℕ
x : R
⊢ ψ x ^ n = (ψ.mulShift ↑n) x
Module: Mathlib.Data.Finset.NAry

Goal state before:
pp: α : Type u_1
β : Type u_3
γ : Type u_5
inst✝¹ : DecidableEq γ
f : α → β → γ
s : Finset α
t t' : Finset β
inst✝ : DecidableEq β
⊢ ↑(image₂ f s (t ∩ t')) ⊆ ↑(image₂ f s t ∩ image₂ f s t')

Tactic:
by
    push_cast
    exact image2_inter_subset_right

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

Goal state before:
pp: R : Type u_1
S : Type u_2
G : Type u_3
M : Type u_4
N : Type u_5
O : Type u_6
ι : Type u_7
inst✝¹ : Semiring R
x y : R[M]
r r₁ r₂ : R
m m' m₁ m₂ m₁' m₂' : M
A : Type u_8
inst✝ : SMulZeroClass A R
⊢ SMul.smul = NSMul.nsmul

Tactic:
by
  with_reducible_and_instances rfl

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

Goal state before:
pp: R : Type u_1
S : Type u_2
G : Type u_3
M : Type u_4
N : Type u_5
O : Type u_6
ι : Type u_7
inst✝² : Semiring R
x✝ y : R[M]
r r₁ r₂ : R
m m' m₁ m₂ m₁' m₂' : M
A : Type u_8
inst✝¹ : SMulZeroClass A R
inst✝ : Monoid A
a : Aˣ
x : R[M]
⊢ a • x = ↑a • x

Tactic:
by
  with_reducible_and_instances rfl

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

Goal state before:
pp: case H.inr
R : Type u_1
A : Type u_2
inst✝⁴ : Semiring R
inst✝³ : IsCancelAdd R
inst✝² : IsLeftCancelMulZero R
inst✝¹ : Mul A
inst✝ : UniqueProds A
f g₁ g₂ : R[A]
eq : f * g₁ = f * g₂
ih :
  ∀ s ∈ g₁.coeff.support ∪ g₂.coeff.support,
    ∀ {g₁_1 g₂_1 : R[A]},
      (fun x ↦ f * x) g₁_1 = (fun x ↦ f * x) g₂_1 →
        g₁_1.coeff.support ∪ g₂_1.coeff.support = (g₁.coeff.support ∪ g₂.coeff.support).erase s → g₁_1 = g₂_1
h✝ : (g₁.coeff.support ∪ g₂.coeff.support).Nonempty
hf : f.coeff.support.Nonempty
af : A
haf : af ∈ f.coeff.support
ag : A
hag : ag ∈ g₁.coeff.support ∪ g₂.coeff.support
uniq : UniqueMul f.coeff.support (g₁.coeff.support ∪ g₂.coeff.support) af ag
h : f.coeff af * g₂.coeff ag = f.coeff af * g₁.coeff ag
this : g₂.coeff ag = g₁.coeff ag
⊢ g₁ = g₂

Tactic:
← g₁.erase_add_single ag,

Goal state after:
case H.inr
R : Type u_1
A : Type u_2
inst✝⁴ : Semiring R
inst✝³ : IsCancelAdd R
inst✝² : IsLeftCancelMulZero R
inst✝¹ : Mul A
inst✝ : UniqueProds A
f g₁ g₂ : R[A]
ih :
  ∀ s ∈ g₁.coeff.support ∪ g₂.coeff.support,
    ∀ {g₁_1 g₂_1 : R[A]},
      (fun x ↦ f * x) g₁_1 = (fun x ↦ f * x) g₂_1 →
        g₁_1.coeff.support ∪ g₂_1.coeff.support = (g₁.coeff.support ∪ g₂.coeff.support).erase s → g₁_1 = g₂_1
h✝ : (g₁.coeff.support ∪ g₂.coeff.support).Nonempty
hf : f.coeff.support.Nonempty
af : A
haf : af ∈ f.coeff.support
ag : A
eq : f * (erase ag g₁ + single ag (g₁.coeff ag)) = f * g₂
hag : ag ∈ g₁.coeff.support ∪ g₂.coeff.support
uniq : UniqueMul f.coeff.support (g₁.coeff.support ∪ g₂.coeff.support) af ag
h : f.coeff af * g₂.coeff ag = f.coeff af * g₁.coeff ag
this : g₂.coeff ag = g₁.coeff ag
⊢ erase ag g₁ + single ag (g₁.coeff ag) = g₂
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
⊢ {ab | ab.1 ∈ A ∧ ab.2 ∈ B ∧ ab.1 * ab.2 = a0 * b0}.Subsingleton

Tactic:
rintro ⟨x1, y1⟩ (hx : x1 ∈ A ∧ y1 ∈ B ∧ x1 * y1 = a0 * b0) ⟨x2, y2⟩
    (hy : x2 ∈ A ∧ y2 ∈ B ∧ x2 * y2 = a0 * b0)

Goal state after:
G : Type u_1
inst✝ : Mul G
A B : Finset G
a0 b0 : G
h : UniqueMul A B a0 b0
x1 y1 : G
hx : x1 ∈ A ∧ y1 ∈ B ∧ x1 * y1 = a0 * b0
x2 y2 : G
hy : x2 ∈ A ∧ y2 ∈ B ∧ x2 * y2 = a0 * b0
⊢ (x1, y1) = (x2, y2)
Module: Mathlib.Algebra.Group.UniqueProds.Basic

Goal state before:
pp: G : Type u
H : Type v
inst✝¹ : Mul G
inst✝ : Mul H
x y : G × H
⊢ (fun t ↦ Bool.rec { down := (x * y).1 } { down := (x * y).2 } t) =
    (fun t ↦ Bool.rec { down := x.1 } { down := x.2 } t) * fun t ↦ Bool.rec { down := y.1 } { down := y.2 } t

Tactic:
ext (_ | _)

Goal state after:
case false
G : Type u
H : Type v
inst✝¹ : Mul G
inst✝ : Mul H
x y : G × H
⊢ (Bool.rec { down := (x * y).1 } { down := (x * y).2 } false).down =
    (((fun t ↦ Bool.rec { down := x.1 } { down := x.2 } t) * fun t ↦ Bool.rec { down := y.1 } { down := y.2 } t)
        false).down

case true
G : Type u
H : Type v
inst✝¹ : Mul G
inst✝ : Mul H
x y : G × H
⊢ (Bool.rec { down := (x * y).1 } { down := (x * y).2 } true).down =
    (((fun t ↦ Bool.rec { down := x.1 } { down := x.2 } t) * fun t ↦ Bool.rec { down := y.1 } { down := y.2 } t)
        true).down
Module: Mathlib.Algebra.Group.UniqueProds.Basic

Goal state before:
pp: G : Type u
H : Type v
inst✝² : Mul G
inst✝¹ : Mul H
f : H →ₙ* G
hf : ∀ ⦃a b c d : H⦄, a * b = c * d → f a = f c ∧ f b = f d → a = c ∧ b = d
inst✝ : UniqueProds G
A B : Finset H
A0 : A.Nonempty
B0 : B.Nonempty
a' : H
ha' : a' ∈ A
ha0 : f a' ∈ image (⇑f) A
b' : H
hb' : b' ∈ B
hb0 : f b' ∈ image (⇑f) B
h : UniqueMul (image (⇑f) A) (image (⇑f) B) (f a') (f b')
⊢ ∃ a0 ∈ A, ∃ b0 ∈ B, UniqueMul A B a0 b0

Tactic:
exact ⟨a', ha', b', hb', UniqueMul.of_mulHom_image f hf h⟩

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

Goal state before:
pp: n : ℕ
i : Fin (n + 1)
k : ℕ
h : #{i}ᶜ = k
j : Fin k
⊢ ({i}ᶜ.orderEmbOfFin h) j = i.succAbove (Fin.cast ⋯ j)

Tactic:
orderEmbOfFin_compl_singleton

Goal state after:
n : ℕ
i : Fin (n + 1)
k : ℕ
h : #{i}ᶜ = k
j : Fin k
⊢ (RelEmbedding.trans (Fin.castOrderIso ⋯).toOrderEmbedding i.succAboveOrderEmb) j = i.succAbove (Fin.cast ⋯ j)
Module: Mathlib.Algebra.Polynomial.Basic

Goal state before:
pp: R : Type u
inst✝ : Semiring R
n m : ℕ
r s : R
⊢ ((monomial n) r * (monomial m) s).toFinsupp = ((monomial (n + m)) (r * s)).toFinsupp

Tactic:
simp only [toFinsupp_monomial, toFinsupp_mul, AddMonoidAlgebra.single_mul_single]

Goal state after:
Module: Mathlib.Algebra.Polynomial.Basic

Goal state before:
pp: R : Type u
inst✝ : Semiring R
a : R
⊢ (C a * X).toFinsupp = single 1 a

Tactic:
by
  rw [C_mul_X_eq_monomial, toFinsupp_monomial]

Goal state after:
Module: Mathlib.Algebra.Polynomial.Basic

Goal state before:
pp: R : Type u
inst✝ : Semiring R
n : ℕ
c : R
h : c ≠ 0
⊢ ((monomial n) c).support = {n}

Tactic:
support_monomial n h

Goal state after:
R : Type u
inst✝ : Semiring R
n : ℕ
c : R
h : c ≠ 0
⊢ {n} = {n}
Module: Mathlib.LinearAlgebra.Finsupp.VectorSpace

Goal state before:
pp: case intro
R : Type u_1
M : Type u_2
n : Type u_3
inst✝⁴ : DecidableEq n
inst✝³ : Semiring R
inst✝² : AddCommMonoid M
inst✝¹ : Module R M
inst✝ : Finite n
b : Basis n R M
i : n
val✝ : Fintype n
⊢ b.equivFun.symm (Pi.single i 1) = b i

Tactic:
simp [Pi.single_apply]

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

Goal state before:
pp: case a.refine_2
R : Type u_1
M : Type u_2
P : Type u_4
inst✝⁴ : Ring R
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : AddCommGroup P
inst✝ : Module R P
f : M →ₗ[R] P
s : Submodule R M
this✝² : DecidableEq R
this✝¹ : DecidableEq M
this✝ : DecidableEq P
t1 : Finset P
ht1 : span R ↑t1 = map f s
t2 : Finset M
ht2 : span R ↑t2 = s ⊓ f.ker
g : P → M
hg : ∀ y ∈ t1, g y ∈ s ∧ f (g y) = y
x : M
hx : x ∈ ↑t2
this : x ∈ s ⊓ f.ker
⊢ x ∈ ↑s

Tactic:
exact this.1

Goal state after:
Module: Mathlib.Data.ENat.Lattice

Goal state before:
pp: ι : Sort u_1
f : ι → ℕ
⊢ ¬IsEmpty ι ↔ Nonempty ι

Tactic:
not_isEmpty_iff

Goal state after:
ι : Sort u_1
f : ι → ℕ
⊢ Nonempty ι ↔ Nonempty ι
Module: Mathlib.Data.ENat.Lattice

Goal state before:
pp: case inr
ι : Sort u_2
f g : ι → ℕ∞
h : ∀ (i j : ι), ∃ k, f i + g j ≤ f k + g k
h✝ : Nonempty ι
i j : ι
⊢ f i + g j ≤ ⨆ i, f i + g i

Tactic:
rcases h i j with ⟨k, hk⟩

Goal state after:
case inr
ι : Sort u_2
f g : ι → ℕ∞
h : ∀ (i j : ι), ∃ k, f i + g j ≤ f k + g k
h✝ : Nonempty ι
i j k : ι
hk : f i + g j ≤ f k + g k
⊢ f i + g j ≤ ⨆ i, f i + g i
Module: Mathlib.Data.ENat.Lattice

Goal state before:
pp: R : Type u_4
inst✝¹ : SMul R ℕ∞
inst✝ : IsScalarTower R ℕ∞ ℕ∞
s : Set ℕ∞
c : R
⊢ c • ⨆ a ∈ s, a = ⨆ a ∈ s, c • a

Tactic:
smul_iSup

Goal state after:
Module: Mathlib.LinearAlgebra.Projection

Goal state before:
pp: S : Type u_5
inst✝² : Semiring S
M : Type u_6
inst✝¹ : AddCommMonoid M
inst✝ : Module S M
f : M →ₗ[S] M
m₁ m₂ : Submodule S M
hf₁ : IsProj m₁ f
hf₂ : IsProj m₂ f
x✝ : M
⊢ x✝ ∈ m₁ ↔ x✝ ∈ m₂

Tactic:
simp [hf₁.mem_iff_map_id, hf₂.mem_iff_map_id]

Goal state after:
Module: Mathlib.Data.ENat.Lattice

Goal state before:
pp: a : ℕ∞
s : Set ℕ∞
⊢ sInf s + a = ⨅ b ∈ s, b + a

Tactic:
by simp [sInf_eq_iInf, iInf_add]

Goal state after:
Module: Mathlib.Data.Rel

Goal state before:
pp: case mp
α : Type u_1
β : Type u_2
R : SetRel α β
⊢ (∃! f, Function.graph f = R) → ∀ (a : α), ∃! b, (a, b) ∈ R

pp: case mpr
α : Type u_1
β : Type u_2
R : SetRel α β
⊢ (∀ (a : α), ∃! b, (a, b) ∈ R) → ∃! f, Function.graph f = R

Tactic:
· rintro ⟨f, rfl, _⟩ x
    simp

Goal state after:
case mpr
α : Type u_1
β : Type u_2
R : SetRel α β
⊢ (∀ (a : α), ∃! b, (a, b) ∈ R) → ∃! f, Function.graph f = R
Module: Mathlib.Order.RelSeries

Goal state before:
pp: α : Type u_1
r : SetRel α α
β : Type u_2
s : SetRel β β
p q : RelSeries r
connect : (p.last, q.head) ∈ r
i : Fin (p.length + q.length + 1)
hi : Fin.castLE (@RelSeries.append._proof_3 α r p q) (Fin.last p.length) < i
x : Fin (p.length + 1 + (q.length + 1)) := Fin.cast ⋯ i.castSucc
y : Fin (p.length + 1 + (q.length + 1)) := Fin.cast ⋯ i.succ
⊢ ↑i = p.length + 1 + (↑i - (p.length + 1))

Tactic:
rw [Nat.add_sub_cancel']

Goal state after:
α : Type u_1
r : SetRel α α
β : Type u_2
s : SetRel β β
p q : RelSeries r
connect : (p.last, q.head) ∈ r
i : Fin (p.length + q.length + 1)
hi : Fin.castLE (@RelSeries.append._proof_3 α r p q) (Fin.last p.length) < i
x : Fin (p.length + 1 + (q.length + 1)) := Fin.cast ⋯ i.castSucc
y : Fin (p.length + 1 + (q.length + 1)) := Fin.cast ⋯ i.succ
⊢ p.length + 1 ≤ ↑i
Module: Mathlib.Order.RelSeries

Goal state before:
pp: case hl
α : Type u_1
r : SetRel α α
p q : RelSeries r
connect : (p.last, q.head) ∈ r
⊢ (p.append q connect).toList.length = (p.toList ++ q.toList).length

pp: case h
α : Type u_1
r : SetRel α α
p q : RelSeries r
connect : (p.last, q.head) ∈ r
⊢ ∀ (i : ℕ) (h₁ : i < (p.append q connect).toList.length) (h₂ : i < (p.toList ++ q.toList).length),
    (p.append q connect).toList[i] = (p.toList ++ q.toList)[i]

Tactic:
· simp; grind

Goal state after:
case h
α : Type u_1
r : SetRel α α
p q : RelSeries r
connect : (p.last, q.head) ∈ r
⊢ ∀ (i : ℕ) (h₁ : i < (p.append q connect).toList.length) (h₂ : i < (p.toList ++ q.toList).length),
    (p.append q connect).toList[i] = (p.toList ++ q.toList)[i]
Module: Mathlib.Order.KrullDimension

Goal state before:
pp: α : Type u_1
inst✝ : Preorder α
a : α
n : ℕ∞
⊢ coheight a ≤ n ↔ ∀ ⦃p : LTSeries α⦄, a ≤ RelSeries.head p → ↑p.length ≤ n

Tactic:
by
  rw [coheight_eq, iSup₂_le_iff]

Goal state after: