mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.RingTheory.TensorProduct.DirectLimitFG

Goal state before:
pp: case h.left
R : Type u_1
S : Type u_2
M : Type u_3
N : Type u_4
inst✝⁶ : CommSemiring R
inst✝⁵ : Semiring S
inst✝⁴ : Algebra R S
inst✝³ : AddCommMonoid M
inst✝² : Module R M
inst✝¹ : AddCommMonoid N
inst✝ : Module R N
f : M →ₗ[R] N
t : S ⊗[R] M
ht : (LinearMap.baseChange S f) t = 0
A : Subalgebra R S
hA : A.FG
ht_memA : t ∈ (rTensor M A.val.toLinearMap).range
u : ↥A ⊗[R] M
hu : (rTensor M A.val.toLinearMap) u = t
this :
  (rTensor N A.val.toLinearMap) ((LinearMap.baseChange (↥A) f) u) = 0 →
    ∃ B, B.FG ∧ ∃ (x : A ≤ B), (rTensor N (Subalgebra.inclusion ⋯).toLinearMap) ((LinearMap.baseChange (↥A) f) u) = 0
hu'✝ : (rTensor N A.val.toLinearMap) ((LinearMap.baseChange (↥A) f) u) = 0
B : Subalgebra R S
hB : B.FG
hAB : A ≤ B
hu' : (rTensor N (Subalgebra.inclusion ⋯).toLinearMap) ((LinearMap.baseChange (↥A) f) u) = 0
⊢ (LinearMap.baseChange (↥B) f) ((rTensor M (Subalgebra.inclusion hAB).toLinearMap) u) = 0

pp: case h.right
R : Type u_1
S : Type u_2
M : Type u_3
N : Type u_4
inst✝⁶ : CommSemiring R
inst✝⁵ : Semiring S
inst✝⁴ : Algebra R S
inst✝³ : AddCommMonoid M
inst✝² : Module R M
inst✝¹ : AddCommMonoid N
inst✝ : Module R N
f : M →ₗ[R] N
t : S ⊗[R] M
ht : (LinearMap.baseChange S f) t = 0
A : Subalgebra R S
hA : A.FG
ht_memA : t ∈ (rTensor M A.val.toLinearMap).range
u : ↥A ⊗[R] M
hu : (rTensor M A.val.toLinearMap) u = t
this :
  (rTensor N A.val.toLinearMap) ((LinearMap.baseChange (↥A) f) u) = 0 →
    ∃ B, B.FG ∧ ∃ (x : A ≤ B), (rTensor N (Subalgebra.inclusion ⋯).toLinearMap) ((LinearMap.baseChange (↥A) f) u) = 0
hu'✝ : (rTensor N A.val.toLinearMap) ((LinearMap.baseChange (↥A) f) u) = 0
B : Subalgebra R S
hB : B.FG
hAB : A ≤ B
hu' : (rTensor N (Subalgebra.inclusion ⋯).toLinearMap) ((LinearMap.baseChange (↥A) f) u) = 0
⊢ (rTensor M B.val.toLinearMap) ((rTensor M (Subalgebra.inclusion hAB).toLinearMap) u) = t

Tactic:
· rw [← rTensor_baseChange, hu']

Goal state after:
case h.right
R : Type u_1
S : Type u_2
M : Type u_3
N : Type u_4
inst✝⁶ : CommSemiring R
inst✝⁵ : Semiring S
inst✝⁴ : Algebra R S
inst✝³ : AddCommMonoid M
inst✝² : Module R M
inst✝¹ : AddCommMonoid N
inst✝ : Module R N
f : M →ₗ[R] N
t : S ⊗[R] M
ht : (LinearMap.baseChange S f) t = 0
A : Subalgebra R S
hA : A.FG
ht_memA : t ∈ (rTensor M A.val.toLinearMap).range
u : ↥A ⊗[R] M
hu : (rTensor M A.val.toLinearMap) u = t
this :
  (rTensor N A.val.toLinearMap) ((LinearMap.baseChange (↥A) f) u) = 0 →
    ∃ B, B.FG ∧ ∃ (x : A ≤ B), (rTensor N (Subalgebra.inclusion ⋯).toLinearMap) ((LinearMap.baseChange (↥A) f) u) = 0
hu'✝ : (rTensor N A.val.toLinearMap) ((LinearMap.baseChange (↥A) f) u) = 0
B : Subalgebra R S
hB : B.FG
hAB : A ≤ B
hu' : (rTensor N (Subalgebra.inclusion ⋯).toLinearMap) ((LinearMap.baseChange (↥A) f) u) = 0
⊢ (rTensor M B.val.toLinearMap) ((rTensor M (Subalgebra.inclusion hAB).toLinearMap) u) = t
Module: Mathlib.RingTheory.PowerSeries.WeierstrassPreparation

Goal state before:
pp: A : Type u_1
inst✝² : CommRing A
inst✝¹ : IsLocalRing A
f : A⟦X⟧
inst✝ : IsPrecomplete (IsLocalRing.maximalIdeal A) A
⊢ f /ʷ 0 = 0

Tactic:
by
  rw [weierstrassDiv, dif_neg (by simp)]

Goal state after:
Module: Mathlib.RingTheory.SimpleModule.Isotypic

Goal state before:
pp: case refine_1
R : Type u_2
M : Type u
inst✝³ : Ring R
inst✝² : AddCommGroup M
inst✝¹ : Module R M
inst✝ : IsSemisimpleModule R M
m : Submodule R M
h : m.IsFullyInvariant
⊢ Subtype.val '' OrderIso.setIsotypicComponents.symm ⟨m, h⟩ ⊆ isotypicComponents R M

pp: case refine_2
R : Type u_2
M : Type u
inst✝³ : Ring R
inst✝² : AddCommGroup M
inst✝¹ : Module R M
inst✝ : IsSemisimpleModule R M
m : Submodule R M
h : m.IsFullyInvariant
⊢ m = sSup (Subtype.val '' OrderIso.setIsotypicComponents.symm ⟨m, h⟩)

pp: case refine_3
R : Type u_2
M : Type u
inst✝³ : Ring R
inst✝² : AddCommGroup M
inst✝¹ : Module R M
inst✝ : IsSemisimpleModule R M
m : Submodule R M
⊢ (∃ s ⊆ isotypicComponents R M, m = sSup s) → m.IsFullyInvariant

Tactic:
· rintro _ ⟨c, _, rfl⟩; exact c.2

Goal state after:
case refine_2
R : Type u_2
M : Type u
inst✝³ : Ring R
inst✝² : AddCommGroup M
inst✝¹ : Module R M
inst✝ : IsSemisimpleModule R M
m : Submodule R M
h : m.IsFullyInvariant
⊢ m = sSup (Subtype.val '' OrderIso.setIsotypicComponents.symm ⟨m, h⟩)

case refine_3
R : Type u_2
M : Type u
inst✝³ : Ring R
inst✝² : AddCommGroup M
inst✝¹ : Module R M
inst✝ : IsSemisimpleModule R M
m : Submodule R M
⊢ (∃ s ⊆ isotypicComponents R M, m = sSup s) → m.IsFullyInvariant
Module: Mathlib.RingTheory.SimpleModule.WedderburnArtin

Goal state before:
pp: R₀ : Type u_1
R : Type u
inst✝⁸ : CommSemiring R₀
inst✝⁷ : Ring R
inst✝⁶ : Algebra R₀ R
M : Type v
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R₀ M
inst✝³ : Module R M
inst✝² : IsScalarTower R₀ R M
inst✝¹ : IsSemisimpleModule R M
inst✝ : Module.Finite R M
n : ℕ
S : Fin n → Submodule R M
d : Fin n → ℕ
left✝ : ∀ (i : Fin n), IsSimpleModule R ↥(S i)
hd : ∀ (i : Fin n), NeZero (d i)
e : End R M ≃ₐ[R₀] (i : Fin n) → Matrix (Fin (d i)) (Fin (d i)) (End R ↥(S i))
⊢ ∃ n D d x x_1,
    (∀ (i : Fin n), NeZero (d i)) ∧ Nonempty (End R M ≃ₐ[R₀] (i : Fin n) → Matrix (Fin (d i)) (Fin (d i)) (D i))

Tactic:
exact ⟨n, _, d, inferInstance, inferInstance, hd, ⟨e⟩⟩

Goal state after:
Module: Mathlib.RingTheory.SimpleModule.WedderburnArtin

Goal state before:
pp: R₀ : Type u_1
R : Type u
inst✝³ : CommSemiring R₀
inst✝² : Ring R
inst✝¹ : Algebra R₀ R
inst✝ : IsSemisimpleRing R
n : ℕ
S : Fin n → Ideal R
d : Fin n → ℕ
left✝ : ∀ (i : Fin n), IsSimpleModule R ↥(S i)
hd : ∀ (i : Fin n), NeZero (d i)
e : R ≃ₐ[R₀] (i : Fin n) → Matrix (Fin (d i)) (Fin (d i)) (Module.End R ↥(S i))ᵐᵒᵖ
⊢ ∃ n D d x x_1, (∀ (i : Fin n), NeZero (d i)) ∧ Nonempty (R ≃ₐ[R₀] (i : Fin n) → Matrix (Fin (d i)) (Fin (d i)) (D i))

Tactic:
exact ⟨n, _, d, inferInstance, inferInstance, hd, ⟨e⟩⟩

Goal state after:
Module: Mathlib.RingTheory.Valuation.Minpoly

Goal state before:
pp: K : Type u_1
inst✝⁴ : Field K
Γ₀ : Type u_2
inst✝³ : LinearOrderedCommGroupWithZero Γ₀
v : Valuation K Γ₀
L : Type u_3
inst✝² : Field L
inst✝¹ : Algebra K L
inst✝ : FiniteDimensional K L
x : L
hx : IsUnit x
h_alg : Algebra.IsAlgebraic K L
hx₀ : IsIntegral K x
hdeg : 0 < finrank K L / (minpoly K x).natDegree
⊢ v ((minpoly K x).coeff 0) ^ (finrank K L / (minpoly K x).natDegree) ≠ 0

Tactic:
rw [ne_eq, pow_eq_zero_iff hdeg.ne.symm, Valuation.zero_iff]

Goal state after:
K : Type u_1
inst✝⁴ : Field K
Γ₀ : Type u_2
inst✝³ : LinearOrderedCommGroupWithZero Γ₀
v : Valuation K Γ₀
L : Type u_3
inst✝² : Field L
inst✝¹ : Algebra K L
inst✝ : FiniteDimensional K L
x : L
hx : IsUnit x
h_alg : Algebra.IsAlgebraic K L
hx₀ : IsIntegral K x
hdeg : 0 < finrank K L / (minpoly K x).natDegree
⊢ ¬(minpoly K x).coeff 0 = 0
Module: Mathlib.RingTheory.Valuation.ValuativeRel.Trivial

Goal state before:
pp: R Γ : Type
inst✝⁵ : Ring R
inst✝⁴ : DecidableEq R
inst✝³ : IsDomain R
inst✝² : LinearOrderedCommGroupWithZero Γ
inst✝¹ : ValuativeRel R
inst✝ : Valuation.Compatible 1
a b : (ValueGroupWithZero R)ˣ
this : (valuation R).IsEquiv 1
⊢ a = b

Tactic:
obtain ⟨r, s, hr⟩ := exists_valuation_posSubmonoid_div_valuation_posSubmonoid_eq a

Goal state after:
R Γ : Type
inst✝⁵ : Ring R
inst✝⁴ : DecidableEq R
inst✝³ : IsDomain R
inst✝² : LinearOrderedCommGroupWithZero Γ
inst✝¹ : ValuativeRel R
inst✝ : Valuation.Compatible 1
a b : (ValueGroupWithZero R)ˣ
this : (valuation R).IsEquiv 1
r s : ↥(posSubmonoid R)
hr : (valuation R) ↑r / (valuation R) ↑s = ↑a
⊢ a = b
Module: Mathlib.RingTheory.WittVector.Compare

Goal state before:
pp: p : ℕ
hp : Fact (Nat.Prime p)
n m : ℕ
hm : n ≤ m
x : TruncatedWittVector p m (ZMod p)
⊢ (zmodEquivTrunc p n) ((zmodEquivTrunc p n).symm ((truncate hm) x)) =
    (zmodEquivTrunc p n) ((ZMod.castHom ⋯ (ZMod (p ^ n))) ((zmodEquivTrunc p m).symm x))

Tactic:
← commutes' _ _ hm

Goal state after:
p : ℕ
hp : Fact (Nat.Prime p)
n m : ℕ
hm : n ≤ m
x : TruncatedWittVector p m (ZMod p)
⊢ (zmodEquivTrunc p n) ((zmodEquivTrunc p n).symm ((truncate hm) x)) =
    (truncate hm) ((zmodEquivTrunc p m) ((zmodEquivTrunc p m).symm x))
Module: Mathlib.RingTheory.WittVector.FrobeniusFractionField

Goal state before:
pp: p : ℕ
hp : Fact (Nat.Prime p)
k : Type u_1
inst✝² : Field k
inst✝¹ : CharP k p
inst✝ : IsAlgClosed k
m n : ℕ
r' q' : 𝕎 k
hr' : r'.coeff 0 ≠ 0
hq' : q'.coeff 0 ≠ 0
hq : ↑p ^ n * q' ∈ nonZeroDivisors (𝕎 k)
b : 𝕎 k := frobeniusRotation p hr' hq'
⊢ frobenius b * r' = q' * b

Tactic:
linear_combination frobenius_frobeniusRotation p hr' hq'

Goal state after:
Module: Mathlib.RingTheory.ZMod.Torsion

Goal state before:
pp: p : ℕ
inst✝ : Fact (Nat.Prime p)
⊢ HasEnoughRootsOfUnity (ZMod p) (p - 1)

Tactic:
have : NeZero (p - 1) := ⟨by have : 2 ≤ p := Nat.Prime.two_le Fact.out; grind⟩
  refine HasEnoughRootsOfUnity.of_card_le ?_
  have := Nat.card_congr (MulEquiv.subgroupCongr (ZMod.rootsOfUnity_eq_top (p := p))).toEquiv
  rw [this]
  simp [Fintype.card_units]

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

Goal state before:
pp: α : Type v
inst✝¹ : LinearOrder α
inst✝ : WellFoundedLT α
ι : Type u
f : ι → Set α
hα : cof α ≠ ℵ₀
hι : lift.{v, u} #ι < lift.{u, v} (cof α)
⊢ IsStationary (⋃₀ range f) ↔ ∃ i, IsStationary (f i)

Tactic:
isStationary_sUnion_iff hα

Goal state after:
α : Type v
inst✝¹ : LinearOrder α
inst✝ : WellFoundedLT α
ι : Type u
f : ι → Set α
hα : cof α ≠ ℵ₀
hι : lift.{v, u} #ι < lift.{u, v} (cof α)
⊢ (∃ x ∈ range f, IsStationary x) ↔ ∃ i, IsStationary (f i)

α : Type v
inst✝¹ : LinearOrder α
inst✝ : WellFoundedLT α
ι : Type u
f : ι → Set α
hα : cof α ≠ ℵ₀
hι : lift.{v, u} #ι < lift.{u, v} (cof α)
⊢ #↑(range f) < cof α
Module: Mathlib.SetTheory.Ordinal.CantorNormalForm

Goal state before:
pp: b e x y : Ordinal.{u_1}
hb : 1 < b
hx : x ≠ 0
hxb : x < b
hy : y < b ^ e
⊢ CNF b (b ^ e * x + y) = (e, x) :: CNF b y

Tactic:
by
  have hb' := hb.ne_bot
  rw [CNF.ne_zero]
  · rw [log_opow_mul_add hb hx hy, log_eq_zero hxb, add_zero,
      mul_add_div _ (opow_ne_zero _ hb'), Ordinal.div_eq_zero_of_lt hy, add_zero,
      mul_add_mod_self, mod_eq_of_lt hy]
  · simp_all

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

Goal state before:
pp: case ind
α : Type u
inst✝ : CompleteLattice α
f g : α →o α
h : f ≤ g
x : α
i : Ordinal.{u}
IH : ∀ y < i, lfpApprox f x y ≤ lfpApprox g x y
⊢ lfpApprox f x i ≤ lfpApprox g x i

Tactic:
| ind i IH
   => 

Goal state after:
case ind
α : Type u
inst✝ : CompleteLattice α
f g : α →o α
h : f ≤ g
x : α
i : Ordinal.{u}
IH : ∀ y < i, lfpApprox f x y ≤ lfpApprox g x y
⊢ lfpApprox f x i ≤ lfpApprox g x i
Module: Mathlib.SetTheory.Ordinal.FixedPointApproximants

Goal state before:
pp: case ind
α : Type u
inst✝ : CompleteLattice α
f : α →o α
x₁ x₂ : α
h : x₁ ≤ x₂
i : Ordinal.{u}
IH : ∀ y < i, lfpApprox f x₁ y ≤ lfpApprox f x₂ y
⊢ lfpApprox f x₁ i ≤ lfpApprox f x₂ i

Tactic:
| ind i IH
   => 

Goal state after:
case ind
α : Type u
inst✝ : CompleteLattice α
f : α →o α
x₁ x₂ : α
h : x₁ ≤ x₂
i : Ordinal.{u}
IH : ∀ y < i, lfpApprox f x₁ y ≤ lfpApprox f x₂ y
⊢ lfpApprox f x₁ i ≤ lfpApprox f x₂ i
Module: Mathlib.SetTheory.Ordinal.CantorNormalForm

Goal state before:
pp: b o : Ordinal.{u_1}
⊢ (coeff b o).support = (map Prod.fst (CNF b o)).toFinset

Tactic:
coeff,

Goal state after:
b o : Ordinal.{u_1}
⊢ { entries := map Prod.toSigma (CNF b o), nodupKeys := ⋯ }.lookupFinsupp.support = (map Prod.fst (CNF b o)).toFinset
Module: Mathlib.SetTheory.Ordinal.CantorNormalForm

Goal state before:
pp: b o e c : Ordinal.{u_1}
h : (e, c) ∈ CNF b o
⊢ (coeff b o) e = c

Tactic:
coeff,

Goal state after:
b o e c : Ordinal.{u_1}
h : (e, c) ∈ CNF b o
⊢ { entries := map Prod.toSigma (CNF b o), nodupKeys := ⋯ }.lookupFinsupp e = c
Module: Mathlib.SetTheory.Ordinal.FixedPointApproximants

Goal state before:
pp: case ind
α : Type u
inst✝ : CompleteLattice α
f : α →o α
x a : α
ha : a ∈ fixedPoints ⇑f
hxa : x ≤ a
i : Ordinal.{u}
IH : ∀ y < i, lfpApprox f x y ≤ a
⊢ lfpApprox f x i ≤ a

Tactic:
| ind i IH
   => 

Goal state after:
case ind
α : Type u
inst✝ : CompleteLattice α
f : α →o α
x a : α
ha : a ∈ fixedPoints ⇑f
hxa : x ≤ a
i : Ordinal.{u}
IH : ∀ y < i, lfpApprox f x y ≤ a
⊢ lfpApprox f x i ≤ a
Module: Mathlib.SetTheory.ZFC.PSet

Goal state before:
pp: ⊢ ∅ = mk PEmpty PEmpty.elim

Tactic:
by
  simp [EmptyCollection.emptyCollection, PSet.empty]

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

Goal state before:
pp: b o : ONote
⊢ Decidable (b.TopBelow o)

Tactic:
cases o

Goal state after:
case zero
b : ONote
⊢ Decidable (b.TopBelow zero)

case oadd
b a✝² : ONote
a✝¹ : ℕ+
a✝ : ONote
⊢ Decidable (b.TopBelow (a✝².oadd a✝¹ a✝))
Module: Mathlib.SetTheory.ZFC.Basic

Goal state before:
pp: x y z : ZFSet.{u_1}
⊢ {x} = {y, z} ↔ x = y ∧ x = z

Tactic:
rw [eq_comm, pair_eq_singleton_iff]

Goal state after:
x y z : ZFSet.{u_1}
⊢ y = x ∧ z = x ↔ x = y ∧ x = z
Module: Mathlib.SetTheory.Ordinal.Veblen

Goal state before:
pp: f : Ordinal.{u} → Ordinal.{u}
hf : IsNormal f
hp : 0 < f 0
o : Ordinal.{u}
ho : IsSuccLimit o
a : Ordinal.{u}
IH : ∀ b < o, veblenWith f b 0 ≤ a
⊢ derivFamily (fun x ↦ veblenWith f ↑x) 0 ≤ a

Tactic:
derivFamily_zero

Goal state after:
f : Ordinal.{u} → Ordinal.{u}
hf : IsNormal f
hp : 0 < f 0
o : Ordinal.{u}
ho : IsSuccLimit o
a : Ordinal.{u}
IH : ∀ b < o, veblenWith f b 0 ≤ a
⊢ nfpFamily (fun x ↦ veblenWith f ↑x) 0 ≤ a
Module: Mathlib.SetTheory.Ordinal.Notation

Goal state before:
pp: o : ONote
b : Ordinal.{0}
x✝ : NFBelow 0 b
h₂ : o.NF
⊢ (0 - o).NFBelow b

Tactic:
cases o

Goal state after:
case zero
b : Ordinal.{0}
x✝ : NFBelow 0 b
h₂ : zero.NF
⊢ (0 - zero).NFBelow b

case oadd
b : Ordinal.{0}
x✝ : NFBelow 0 b
a✝² : ONote
a✝¹ : ℕ+
a✝ : ONote
h₂ : (a✝².oadd a✝¹ a✝).NF
⊢ (0 - a✝².oadd a✝¹ a✝).NFBelow b
Module: Mathlib.SetTheory.Ordinal.Veblen

Goal state before:
pp: case a
o a : Ordinal.{u}
h : a < veblen o a
⊢ veblen o a < veblen o (veblen o a)

Tactic:
veblen_lt_veblen_iff_right

Goal state after:
case a
o a : Ordinal.{u}
h : a < veblen o a
⊢ a < veblen o a
Module: Mathlib.SetTheory.ZFC.Basic

Goal state before:
pp: ⊢ Function.Injective2 pair

Tactic:
intro x x' y y' H
  simp_rw [ZFSet.ext_iff, pair, mem_pair] at H
  obtain rfl : x = x' := And.left <| by simpa [or_and_left] using (H {x}).1 (Or.inl rfl)
  have he : y = x → y = y' := by
    rintro rfl
    simpa [eq_comm] using H {y, y'}
  have hx := H {x, y}
  simp_rw [pair_eq_singleton_iff, true_and, or_true, true_iff] at hx
  refine ⟨rfl, hx.elim he fun hy ↦ Or.elim ?_ he id⟩
  simpa using ZFSet.ext_iff.1 hy y

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

Goal state before:
pp: o : ONote
x✝ : NF 0
h₂ : o.NF
⊢ (0 - o).repr = repr 0 - o.repr

Tactic:
cases o

Goal state after:
case zero
x✝ : NF 0
h₂ : zero.NF
⊢ (0 - zero).repr = repr 0 - zero.repr

case oadd
x✝ : NF 0
a✝² : ONote
a✝¹ : ℕ+
a✝ : ONote
h₂ : (a✝².oadd a✝¹ a✝).NF
⊢ (0 - a✝².oadd a✝¹ a✝).repr = repr 0 - (a✝².oadd a✝¹ a✝).repr
Module: Mathlib.SetTheory.ZFC.Class

Goal state before:
pp: A : Class.{u_1}
x : ZFSet.{u_1}
H : ∀ (y : ZFSet.{u_1}), A y ↔ y = x
y : ZFSet.{u_1}
x✝ : A.iota y
x' : ZFSet.{u_1}
h : {x | ∀ (y : ZFSet.{u_1}), A y ↔ y = x} x'
yx' : y ∈ ↑x'
⊢ ↑x y

Tactic:
← (H x').1 <| (h x').2 rfl

Goal state after:
A : Class.{u_1}
x : ZFSet.{u_1}
H : ∀ (y : ZFSet.{u_1}), A y ↔ y = x
y : ZFSet.{u_1}
x✝ : A.iota y
x' : ZFSet.{u_1}
h : {x | ∀ (y : ZFSet.{u_1}), A y ↔ y = x} x'
yx' : y ∈ ↑x'
⊢ ↑x' y
Module: Mathlib.SetTheory.Ordinal.Notation

Goal state before:
pp: case neg
e₁ : ONote
n₁ : ℕ+
a₁ : ONote
n₂ : ℕ+
a₂ : ONote
h₁ : (e₁.oadd n₁ a₁).NF
this✝ : a₁.NF
this : a₂.NF
h' : (a₁.sub a₂).repr = a₁.repr - a₂.repr
h₂ : (e₁.oadd n₂ a₂).NF
h : e₁.cmp e₁ = Ordering.eq
mn : ↑n₁ - ↑n₂ = 0
en : ¬n₁ = n₂
⊢ repr 0 = (e₁.oadd n₁ a₁).repr - (e₁.oadd n₂ a₂).repr

Tactic:
exact
            (Ordinal.sub_eq_zero_iff_le.2 <|
                le_of_lt <|
                  oadd_lt_oadd_2 h₁ <|
                    lt_of_le_of_ne (tsub_eq_zero_iff_le.1 mn) (mt PNat.eq en)).symm

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

Goal state before:
pp: o : ONote
⊢ 0 * o = 0

Tactic:
cases o

Goal state after:
case zero
⊢ 0 * zero = 0

case oadd
a✝² : ONote
a✝¹ : ℕ+
a✝ : ONote
⊢ 0 * a✝².oadd a✝¹ a✝ = 0
Module: Mathlib.SetTheory.Ordinal.Notation

Goal state before:
pp: o : ONote
⊢ o * 0 = 0

Tactic:
cases o

Goal state after:
case zero
⊢ zero * 0 = 0

case oadd
a✝² : ONote
a✝¹ : ℕ+
a✝ : ONote
⊢ a✝².oadd a✝¹ a✝ * 0 = 0
Module: Mathlib.SetTheory.Ordinal.Notation

Goal state before:
pp: o : ONote
x✝ : NF 0
h₂ : o.NF
⊢ (0 * o).NF

Tactic:
cases o

Goal state after:
case zero
x✝ : NF 0
h₂ : zero.NF
⊢ (0 * zero).NF

case oadd
x✝ : NF 0
a✝² : ONote
a✝¹ : ℕ+
a✝ : ONote
h₂ : (a✝².oadd a✝¹ a✝).NF
⊢ (0 * a✝².oadd a✝¹ a✝).NF
Module: Mathlib.SetTheory.Ordinal.Notation

Goal state before:
pp: o : ONote
x✝ : NF 0
h₂ : o.NF
⊢ (0 * o).repr = repr 0 * o.repr

Tactic:
cases o

Goal state after:
case zero
x✝ : NF 0
h₂ : zero.NF
⊢ (0 * zero).repr = repr 0 * zero.repr

case oadd
x✝ : NF 0
a✝² : ONote
a✝¹ : ℕ+
a✝ : ONote
h₂ : (a✝².oadd a✝¹ a✝).NF
⊢ (0 * a✝².oadd a✝¹ a✝).repr = repr 0 * (a✝².oadd a✝¹ a✝).repr
Module: Mathlib.SetTheory.Ordinal.Notation

Goal state before:
pp: e₁ : ONote
n₁ : ℕ+
a₁ e₂ : ONote
n₂ : ℕ+
a₂ : ONote
h₁ : (e₁.oadd n₁ a₁).NF
h₂ : (e₂.oadd n₂ a₂).NF
IH : ((e₁.oadd n₁ a₁).mul a₂).repr = (e₁.oadd n₁ a₁).repr * a₂.repr
⊢ (Mul.mul (e₁.oadd n₁ a₁) (e₂.oadd n₂ a₂)).repr = (e₁.oadd n₁ a₁).repr * (e₂.oadd n₂ a₂).repr

Tactic:
have ao : repr a₁ + ω ^ repr e₁ * (n₁ : ℕ) = ω ^ repr e₁ * (n₁ : ℕ) := by
      apply add_of_omega0_opow_le h₁.snd'.repr_lt
      simpa using! (mul_le_mul_iff_right₀ <| opow_pos _ omega0_pos).2 (Nat.cast_le.2 n₁.2)

Goal state after:
e₁ : ONote
n₁ : ℕ+
a₁ e₂ : ONote
n₂ : ℕ+
a₂ : ONote
h₁ : (e₁.oadd n₁ a₁).NF
h₂ : (e₂.oadd n₂ a₂).NF
IH : ((e₁.oadd n₁ a₁).mul a₂).repr = (e₁.oadd n₁ a₁).repr * a₂.repr
ao : a₁.repr + ω ^ e₁.repr * ↑↑n₁ = ω ^ e₁.repr * ↑↑n₁
⊢ (Mul.mul (e₁.oadd n₁ a₁) (e₂.oadd n₂ a₂)).repr = (e₁.oadd n₁ a₁).repr * (e₂.oadd n₂ a₂).repr
Module: Mathlib.SetTheory.Ordinal.Notation

Goal state before:
pp: n : ℕ
o : ONote
⊢ o.mulNat n = o * ↑n

Tactic:
cases o

Goal state after:
case zero
n : ℕ
⊢ zero.mulNat n = zero * ↑n

case oadd
n : ℕ
a✝² : ONote
a✝¹ : ℕ+
a✝ : ONote
⊢ (a✝².oadd a✝¹ a✝).mulNat n = a✝².oadd a✝¹ a✝ * ↑n
Module: Mathlib.Tactic.ComputeAsymptotics.Multiseries.Corecursion

Goal state before:
pp: case e'_2.e'_6
α : Type u_1
s t : Stream'.Seq α
h : s.head ≠ t.head
h' : ¬↑s = ↑t
⊢ ¬↑s 0 = ↑t 0

Tactic:
simpa [Stream'.cons]

Goal state after:
Module: Mathlib.Tactic.ComputeAsymptotics.Multiseries.Basis

Goal state before:
pp: basis : Basis
h : WellFormedBasis basis
⊢ ∀ᶠ (x : ℝ) in atTop, ∀ f ∈ basis, 0 < f x

Tactic:
induction basis with
  | nil => simp
  | cons hd tl ih =>
    simp only [WellFormedBasis, List.pairwise_cons, List.mem_cons, forall_eq_or_imp] at h
    simp only [List.mem_cons, forall_eq_or_imp]
    exact (h.right.left.eventually <| eventually_gt_atTop 0).and (ih (by tauto))

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

Goal state before:
pp: case pos
o₁ o₂ : ONote
inst✝¹ : o₁.NF
inst✝ : o₂.NF
N₁ : zero.NF
m : ℕ
e₁ : o₁.split = (zero, m + 1)
r₁ : o₁.repr = zero.repr + ↑(m + 1)
b' : ONote
k : ℕ
e₂ : o₂.split' = (b', k)
left✝ : b'.NF
r₂ : o₂.repr = ω * b'.repr + ↑k
h : m = 0
⊢ ω ^ type emptyRelation * ↑↑⟨1, ⋯⟩ + type emptyRelation = (type emptyRelation + ↑(0 + 1)) ^ (ω * b'.repr + ↑k)

Tactic:
simp [opow_add, opow_mul]

Goal state after:
Module: Mathlib.Tactic.ComputeAsymptotics.Multiseries.Monomial.Basic

Goal state before:
pp: coef : ℝ
exps : UnitMonomial
basis : Basis
h_basis : WellFormedBasis basis
h_length : List.length exps = List.length basis
h_exps : exps.FirstNonzeroIsNeg
t : Monomial := { coef := coef, unit := exps }
⊢ Tendsto (fun a ↦ t.toFun basis a) atTop (𝓝 0)

Tactic:
simp only [toFun, Pi.smul_apply, smul_eq_mul]

Goal state after:
coef : ℝ
exps : UnitMonomial
basis : Basis
h_basis : WellFormedBasis basis
h_length : List.length exps = List.length basis
h_exps : exps.FirstNonzeroIsNeg
t : Monomial := { coef := coef, unit := exps }
⊢ Tendsto (fun a ↦ t.coef * t.unit.toFun basis a) atTop (𝓝 0)
Module: Mathlib.Tactic.ComputeAsymptotics.Multiseries.Monomial.Basic

Goal state before:
pp: coef : ℝ
exps : UnitMonomial
basis : Basis
h_basis : WellFormedBasis basis
h_length : List.length exps = List.length basis
h_coef : 0 < coef
h_exps : exps.FirstNonzeroIsPos
t : Monomial := { coef := coef, unit := exps }
⊢ Tendsto (fun a ↦ t.toFun basis a) atTop atTop

Tactic:
simp only [toFun, Pi.smul_apply, smul_eq_mul]

Goal state after:
coef : ℝ
exps : UnitMonomial
basis : Basis
h_basis : WellFormedBasis basis
h_length : List.length exps = List.length basis
h_coef : 0 < coef
h_exps : exps.FirstNonzeroIsPos
t : Monomial := { coef := coef, unit := exps }
⊢ Tendsto (fun a ↦ t.coef * t.unit.toFun basis a) atTop atTop
Module: Mathlib.Tactic.ComputeAsymptotics.Multiseries.Monomial.Basic

Goal state before:
pp: coef : ℝ
exps : UnitMonomial
basis : Basis
h_basis : WellFormedBasis basis
h_length : List.length exps = List.length basis
h_coef : coef < 0
h_exps : exps.FirstNonzeroIsPos
t : Monomial := { coef := coef, unit := exps }
⊢ Tendsto (fun a ↦ t.toFun basis a) atTop atBot

Tactic:
simp only [toFun, Pi.smul_apply, smul_eq_mul]

Goal state after:
coef : ℝ
exps : UnitMonomial
basis : Basis
h_basis : WellFormedBasis basis
h_length : List.length exps = List.length basis
h_coef : coef < 0
h_exps : exps.FirstNonzeroIsPos
t : Monomial := { coef := coef, unit := exps }
⊢ Tendsto (fun a ↦ t.coef * t.unit.toFun basis a) atTop atBot
Module: Mathlib.Tactic.ComputeAsymptotics.Multiseries.Monomial.Basic

Goal state before:
pp: coef : ℝ
exps : UnitMonomial
basis : Basis
h_exps : exps.AllZero
t : Monomial := { coef := coef, unit := exps }
⊢ Tendsto (fun a ↦ t.toFun basis a) atTop (𝓝 coef)

Tactic:
simp only [toFun, Pi.smul_apply, smul_eq_mul]

Goal state after:
coef : ℝ
exps : UnitMonomial
basis : Basis
h_exps : exps.AllZero
t : Monomial := { coef := coef, unit := exps }
⊢ Tendsto (fun a ↦ t.coef * t.unit.toFun basis a) atTop (𝓝 coef)
Module: Mathlib.Tactic.ComputeAsymptotics.Multiseries.Trimming

Goal state before:
pp: basis_hd : ℝ → ℝ
basis_tl : List (ℝ → ℝ)
ms : MultiseriesExpansion (basis_hd :: basis_tl)
h : ms.IsZero
⊢ ms.seq = Multiseries.nil

Tactic:
by cases h; rw [mk_seq]

Goal state after:
Module: Mathlib.Tactic.ComputeAsymptotics.Multiseries.Trimming

Goal state before:
pp: basis_hd : ℝ → ℝ
basis_tl : List (ℝ → ℝ)
ms : MultiseriesExpansion (basis_hd :: basis_tl)
h : ms.seq = Multiseries.nil
⊢ ms.IsZero

Tactic:
by
    convert IsZero.nil ms.toFun
    simp [h]

Goal state after:
Module: Mathlib.Tactic.LinearCombinationPrime

Goal state before:
pp: α : Type u_1
a a' b b' : α
inst✝¹ : Ring α
inst✝ : IsReduced α
n : ℕ
p : a = b
H : (a' - b') ^ n - (a - b) = 0
⊢ a' = b'

Tactic:
by
  rw [← sub_eq_zero] at p ⊢; apply eq_zero_of_pow_eq_zero (n := n); rwa [sub_eq_zero, p] at H

Goal state after:
Module: Mathlib.Tactic.NormNum.Irrational

Goal state before:
pp: case neg
a b d : ℕ
h_coprime : a.Coprime b
ha : ∀ (x : ℕ), a ≠ x ^ d
q : ℚ
hq : 0 ≤ q
hb_zero : ¬b = 0
x' : ℤ := q.num
y : ℕ := q.den
x : ℕ
h : ↑a / ↑b = (↑↑x / ↑y) ^ d
hx' : x' = ↑x
⊢ False

Tactic:
specialize ha x

Goal state after:
case neg
a b d : ℕ
h_coprime : a.Coprime b
q : ℚ
hq : 0 ≤ q
hb_zero : ¬b = 0
x' : ℤ := q.num
y : ℕ := q.den
x : ℕ
ha : a ≠ x ^ d
h : ↑a / ↑b = (↑↑x / ↑y) ^ d
hx' : x' = ↑x
⊢ False
Module: Mathlib.Tactic.NormNum.IsSquare

Goal state before:
pp: a : ℚ
n d : ℕ
hn : ¬IsSquare n
hnd : n.Coprime d
ha : IsNNRat a n d
⊢ ¬IsSquare a

Tactic:
by
  rw [ha.to_eq rfl rfl, Rat.isSquare_iff, ← Int.cast_natCast n, ← Int.cast_natCast d,
    Rat.num_div_eq_of_coprime]
  · simp [hn]
  · contrapose! hnd
    have : n ≠ 1 := by rintro rfl; simp at hn
    simp_all
  · simpa

Goal state after:
Module: Mathlib.Testing.Plausible.Functions

Goal state before:
pp: case pos
α : Type u
inst✝ : DecidableEq α
x : α
xs : List α
y : α
ys : List α
h₂ : (y :: ys).Nodup
h₀ : (x :: xs).Nodup
h₁ : (x :: xs).length = (y :: ys).length
xs_ih :
  ∀ {ys : List α},
    xs.Nodup → dlookup x (map Prod.toSigma (xs.zip ys)) = some y → ys.Nodup → xs.length = ys.length → (y ∈ ys ↔ x ∈ xs)
⊢ y ∈ y :: ys ↔ x ∈ x :: xs

Tactic:
simp only [List.mem_cons, true_or]

Goal state after: