mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Order.InitialSeg

Goal state before:
pp: case inl
α : Type u_1
β : Type u_2
γ : Type u_3
r✝ : α → α → Prop
s✝ : β → β → Prop
t : γ → γ → Prop
r : α → α → Prop
s : β → β → Prop
a val✝ : α
⊢ Sum.Lex r s (Sum.inl val✝) ({ toFun := Sum.inl, inj' := ⋯, map_rel_iff' := ⋯ } a) →
    Sum.inl val✝ ∈ Set.range ⇑{ toFun := Sum.inl, inj' := ⋯, map_rel_iff' := ⋯ }

Tactic:
exact fun _ => ⟨_, rfl⟩

Goal state after:
Module: Mathlib.Order.InitialSeg

Goal state before:
pp: α : Type u_1
β : Type u_2
r : α → α → Prop
s : β → β → Prop
f : r ≺i s
b : β
⊢ b ∈ {b | s b f.top} → b ∈ ⇑f.toRelEmbedding '' Set.univ

Tactic:
h

Goal state after:
α : Type u_1
β : Type u_2
r : α → α → Prop
s : β → β → Prop
f : r ≺i s
b : β
h : b ∈ {b | s b f.top}
⊢ b ∈ ⇑f.toRelEmbedding '' Set.univ
Module: Mathlib.Order.InitialSeg

Goal state before:
pp: case inr.inl
α : Type u_1
β : Type u_2
γ : Type u_3
r✝ : α → α → Prop
s✝ : β → β → Prop
t : γ → γ → Prop
r : α → α → Prop
s : β → β → Prop
inst✝¹ : IsWellOrder α r
inst✝ : IsWellOrder β s
f✝ : r ≺i Sum.Lex r s
g : s ≺i Sum.Lex r s
h : f✝.top = g.top
f : (Subrel (Sum.Lex r s) fun x ↦ Sum.Lex r s x f✝.top) ≃r r := f✝.subrelIso
⊢ Nonempty ((r ≼i s) ⊕ (s ≼i r))

Tactic:
h

Goal state after:
case inr.inl
α : Type u_1
β : Type u_2
γ : Type u_3
r✝ : α → α → Prop
s✝ : β → β → Prop
t : γ → γ → Prop
r : α → α → Prop
s : β → β → Prop
inst✝¹ : IsWellOrder α r
inst✝ : IsWellOrder β s
f✝ : r ≺i Sum.Lex r s
g : s ≺i Sum.Lex r s
h : f✝.top = g.top
f : (Subrel (Sum.Lex r s) fun x ↦ Sum.Lex r s x g.top) ≃r r
⊢ Nonempty ((r ≼i s) ⊕ (s ≼i r))
Module: Mathlib.Order.ScottContinuity

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝¹ : Preorder α
inst✝ : Preorder β
D : Set (Set α)
x : β
⊢ ScottContinuousOn D (Function.const α x)

Tactic:
by
  rintro s _ ⟨a⟩ _ _ _
  simp [IsLUB, IsLeast, upperBounds, lowerBounds]; grind

Goal state after:
Module: Mathlib.Order.ScottContinuity

Goal state before:
pp: case refine_1
β : Type u_2
inst✝ : SemilatticeSup β
d : Set (β × β)
x✝² : d.Nonempty
x✝¹ : DirectedOn (fun x1 x2 ↦ x1 ≤ x2) d
x✝ : β × β
p₁ p₂ : β
hdp : (∀ (a b : β), (a, b) ∈ d → a ≤ p₁ ∧ b ≤ p₂) ∧ (p₁, p₂) ∈ lowerBounds {x | ∀ (a b : β), (a, b) ∈ d → (a, b) ≤ x}
e1 : ∀ (a b : β), (∀ (b₁ b₂ : β), (b₁, b₂) ∈ d → b₁ ≤ a ∧ b₂ ≤ b) → p₁ ≤ a ∧ p₂ ≤ b
a b₁ b₂ : β
hbd : (b₁, b₂) ∈ d
hba : b₁ ⊔ b₂ = a
⊢ a ≤ p₁ ⊔ p₂

Tactic:
rw [← hba]
    exact sup_le_sup (hdp.1 _ _ hbd).1 (hdp.1 _ _ hbd).2

Goal state after:
Module: Mathlib.Data.Part

Goal state before:
pp: case inl
α : Type u_1
x y z : Part α
hx : x ≤ z
hy : y ≤ z
h : x = none
⊢ x ≤ y ∨ y ≤ x

Tactic:
h

Goal state after:
case inl
α : Type u_1
x y z : Part α
hx : x ≤ z
hy : y ≤ z
h : x = none
⊢ none ≤ y ∨ y ≤ none
Module: Mathlib.Order.BourbakiWitt

Goal state before:
pp: α : Type u_1
inst✝ : ChainCompletePartialOrder α
x : α
f : α → α
le_map : ∀ (x : α), x ≤ f x
⊢ ∀ (c : NonemptyChain α), ↑c ⊆ bot x f → cSup c ∈ bot x f

Tactic:
by
    intro c hc s hs
    exact hs.cSup_mem c (subset_trans hc (sInter_subset_of_mem hs))

Goal state after:
Module: Mathlib.Order.BourbakiWitt

Goal state before:
pp: case base_isLeast.right
α : Type u_1
inst✝ : ChainCompletePartialOrder α
x : α
f : α → α
y : α
le_map : ∀ (x : α), x ≤ f x
hy : IsExtremePt x f y
⊢ x ∈ lowerBounds {z | z ∈ bot x f ∧ (z ≤ y ∨ f y ≤ z)}

Tactic:
· exact fun y h ↦ (bot_isAdmissible le_map).base_isLeast.2 h.1

Goal state after:
Module: Mathlib.Order.BourbakiWitt

Goal state before:
pp: case base_isLeast.right
α : Type u_1
inst✝ : ChainCompletePartialOrder α
x : α
f : α → α
le_map : ∀ (x : α), x ≤ f x
⊢ x ∈ lowerBounds {y | IsExtremePt x f y}

Tactic:
· exact fun y h ↦ (bot_isAdmissible le_map).base_isLeast.2 h.1

Goal state after:
Module: Mathlib.Order.OmegaCompletePartialOrder

Goal state before:
pp: case e'_4
α : Type u_2
β : Type u_3
inst✝¹ : OmegaCompletePartialOrder α
inst✝ : OmegaCompletePartialOrder β
f : α → β
hf : ∃ (hf : Monotone f), ∀ (c : Chain α), f (ωSup c) = ωSup (c.map { toFun := f, monotone' := hf })
d✝ : Set α
c : Chain α
hc : (fun c ↦ Set.range ⇑c) c = d✝
a✝² : d✝.Nonempty
a✝¹ : DirectedOn (fun x1 x2 ↦ x1 ≤ x2) d✝
a✝ : α
hda : IsLUB ((fun c ↦ Set.range ⇑c) c) a✝
⊢ f a✝ = f (ωSup c)

Tactic:
ωSup_eq_of_isLUB hda

Goal state after:
case e'_4
α : Type u_2
β : Type u_3
inst✝¹ : OmegaCompletePartialOrder α
inst✝ : OmegaCompletePartialOrder β
f : α → β
hf : ∃ (hf : Monotone f), ∀ (c : Chain α), f (ωSup c) = ωSup (c.map { toFun := f, monotone' := hf })
d✝ : Set α
c : Chain α
hc : (fun c ↦ Set.range ⇑c) c = d✝
a✝² : d✝.Nonempty
a✝¹ : DirectedOn (fun x1 x2 ↦ x1 ≤ x2) d✝
a✝ : α
hda : IsLUB ((fun c ↦ Set.range ⇑c) c) a✝
⊢ f (ωSup c) = f (ωSup c)
Module: Mathlib.Order.BourbakiWitt

Goal state before:
pp: α : Type u_1
inst✝ : ChainCompletePartialOrder α
x : α
f : α → α
le_map : ∀ (x : α), x ≤ f x
y : α
hy : y ∈ bot x f
⊢ ∀ ⦃y_1 : α⦄, y_1 ∈ bot x f → y ≠ y_1 → (fun x y ↦ (fun x1 x2 ↦ x1 ≤ x2) x y ∨ (fun x1 x2 ↦ x1 ≤ x2) y x) y y_1

Tactic:
z

Goal state after:
α : Type u_1
inst✝ : ChainCompletePartialOrder α
x : α
f : α → α
le_map : ∀ (x : α), x ≤ f x
y : α
hy : y ∈ bot x f
z : α
⊢ z ∈ bot x f → y ≠ z → (fun x y ↦ (fun x1 x2 ↦ x1 ≤ x2) x y ∨ (fun x1 x2 ↦ x1 ≤ x2) y x) y z
Module: Mathlib.SetTheory.Cardinal.Order

Goal state before:
pp: c : Cardinal.{u}
⊢ ℵ₀ < lift.{v, u} c ↔ ℵ₀ < c

Tactic:
simpa using lift_lt (a := ℵ₀)

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

Goal state before:
pp: c : Cardinal.{u_1}
h : ℵ₀ ≤ c
⊢ ↑0 = 0

Tactic:
Nat.cast_zero

Goal state after:
c : Cardinal.{u_1}
h : ℵ₀ ≤ c
⊢ 0 = 0
Module: Mathlib.SetTheory.Cardinal.ENat

Goal state before:
pp: case inl
n : ℕ∞
x : Cardinal.{u_1}
hx : x < ℵ₀
⊢ ↑n ≤ x ↔ n ≤ x.toENatAux

Tactic:
| inl hx =>

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

Goal state before:
pp: case inl
x : Cardinal.{u_1}
n : ℕ
hx : x < ℵ₀
⊢ x.toENatAux ≤ ↑n ↔ x ≤ ↑n

Tactic:
| inl hx =>

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

Goal state before:
pp: case refine_1
α✝ : Type u
h : Fintype α✝
α β : Type u
hβ : Fintype β
e : α ≃ β
⊢ (∀ (f : α → Cardinal.{v}), prod f = lift.{u, v} (∏ i, f i)) →
    ∀ (f : β → Cardinal.{v}), prod f = lift.{u, v} (∏ i, f i)

Tactic:
h

Goal state after:
case refine_1
α✝ : Type u
h✝ : Fintype α✝
α β : Type u
hβ : Fintype β
e : α ≃ β
h : ∀ (f : α → Cardinal.{v}), prod f = lift.{u, v} (∏ i, f i)
⊢ ∀ (f : β → Cardinal.{v}), prod f = lift.{u, v} (∏ i, f i)
Module: Mathlib.SetTheory.Cardinal.Basic

Goal state before:
pp: case refine_3
α✝ : Type u
h : Fintype α✝
α : Type u
hα : Fintype α
⊢ (∀ (f : α → Cardinal.{v}), prod f = lift.{u, v} (∏ i, f i)) →
    ∀ (f : Option α → Cardinal.{v}), prod f = lift.{u, v} (∏ i, f i)

Tactic:
h

Goal state after:
case refine_3
α✝ : Type u
h✝ : Fintype α✝
α : Type u
hα : Fintype α
h : ∀ (f : α → Cardinal.{v}), prod f = lift.{u, v} (∏ i, f i)
⊢ ∀ (f : Option α → Cardinal.{v}), prod f = lift.{u, v} (∏ i, f i)
Module: Mathlib.Algebra.Regular.SMul

Goal state before:
pp: R : Type u_1
M : Type u_3
a b : R
inst✝¹ : Monoid R
inst✝ : MulAction R M
h : a * b = 1
⊢ IsSMulRegular M (a * b)

Tactic:
h

Goal state after:
R : Type u_1
M : Type u_3
a b : R
inst✝¹ : Monoid R
inst✝ : MulAction R M
h : a * b = 1
⊢ IsSMulRegular M 1
Module: Mathlib.Algebra.Regular.SMul

Goal state before:
pp: R : Type u_1
S : Type u_2
M : Type u_3
a : R
s : S
inst✝⁴ : Monoid S
inst✝³ : SMul R M
inst✝² : SMul R S
inst✝¹ : MulAction S M
inst✝ : IsScalarTower R S M
h : a • s = 1
⊢ IsSMulRegular M (a • s)

Tactic:
h

Goal state after:
R : Type u_1
S : Type u_2
M : Type u_3
a : R
s : S
inst✝⁴ : Monoid S
inst✝³ : SMul R M
inst✝² : SMul R S
inst✝¹ : MulAction S M
inst✝ : IsScalarTower R S M
h : a • s = 1
⊢ IsSMulRegular M 1
Module: Mathlib.Algebra.Regular.SMul

Goal state before:
pp: R : Type u_1
G : Type u_4
inst✝¹ : Group G
inst✝ : MulAction G R
g : G
x y : R
⊢ (fun x ↦ g • x) x = (fun x ↦ g • x) y → x = y

Tactic:
h

Goal state after:
R : Type u_1
G : Type u_4
inst✝¹ : Group G
inst✝ : MulAction G R
g : G
x y : R
h : (fun x ↦ g • x) x = (fun x ↦ g • x) y
⊢ x = y
Module: Mathlib.SetTheory.Cardinal.Basic

Goal state before:
pp: c : Cardinal.{u_1}
⊢ c < 1 ↔ c = 0

Tactic:
simpa using lt_succ_bot_iff (a := c)

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

Goal state before:
pp: n : ℕ
⊢ ↑n < ℵ₀

Tactic:
by
  rw [← natCast_add_one_le_iff, ← Nat.cast_add_one, ← lift_mk_fin, aleph0, lift_mk_le.{u}]
  exact ⟨⟨(↑), fun a b => Fin.ext⟩⟩

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

Goal state before:
pp: n : ℕ
h : IsSuccLimit (succ ↑n)
⊢ False

Tactic:
exact Order.not_isSuccLimit_succ _ h

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

Goal state before:
pp: a b : Cardinal.{u_1}
⊢ ℵ₀ ≤ a + b ↔ ℵ₀ ≤ a ∨ ℵ₀ ≤ b

Tactic:
by
  simp only [← not_lt, add_lt_aleph0_iff, not_and_or]

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

Goal state before:
pp: a b : Cardinal.{u_1}
h : ¬a * b < ℵ₀ ↔ ¬(a = 0 ∨ b = 0 ∨ a < ℵ₀ ∧ b < ℵ₀) := Iff.not mul_lt_aleph0_iff
⊢ ℵ₀ ≤ a * b ↔ a ≠ 0 ∧ b ≠ 0 ∧ (ℵ₀ ≤ a ∨ ℵ₀ ≤ b)

Tactic:
not_lt,

Goal state after:
a b : Cardinal.{u_1}
h : ℵ₀ ≤ a * b ↔ ¬(a = 0 ∨ b = 0 ∨ a < ℵ₀ ∧ b < ℵ₀)
⊢ ℵ₀ ≤ a * b ↔ a ≠ 0 ∧ b ≠ 0 ∧ (ℵ₀ ≤ a ∨ ℵ₀ ≤ b)
Module: Mathlib.SetTheory.Cardinal.Basic

Goal state before:
pp: a b : Cardinal.{u_1}
h : ℵ₀ ≤ a * b ↔ ¬a = 0 ∧ ¬b = 0 ∧ (¬a < ℵ₀ ∨ ¬b < ℵ₀)
⊢ ℵ₀ ≤ a * b ↔ a ≠ 0 ∧ b ≠ 0 ∧ (ℵ₀ ≤ a ∨ ℵ₀ ≤ b)

Tactic:
not_lt,

Goal state after:
a b : Cardinal.{u_1}
h : ℵ₀ ≤ a * b ↔ ¬a = 0 ∧ ¬b = 0 ∧ (ℵ₀ ≤ a ∨ ¬b < ℵ₀)
⊢ ℵ₀ ≤ a * b ↔ a ≠ 0 ∧ b ≠ 0 ∧ (ℵ₀ ≤ a ∨ ℵ₀ ≤ b)
Module: Mathlib.SetTheory.Cardinal.Basic

Goal state before:
pp: case inl
α : Type u
A B : Set α
hfin✝ : A.Finite
hlt : A ⊂ B
hfin : Finite ↑B
⊢ #↑A < #↑B

Tactic:
exact card_lt_card_of_right_finite hfin hlt

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

Goal state before:
pp: R : Type u_2
inst✝¹ : CommSemiring R
A : Type u_3
inst✝ : Semiring A
P Q : Algebra R A
h : algebraMap R A = algebraMap R A
r : R
a : A
⊢ (algebraMap R A) r * a = (algebraMap R A) r * a

Tactic:
h

Goal state after:
R : Type u_2
inst✝¹ : CommSemiring R
A : Type u_3
inst✝ : Semiring A
P Q : Algebra R A
h : algebraMap R A = algebraMap R A
r : R
a : A
⊢ (algebraMap R A) r * a = (algebraMap R A) r * a
Module: Mathlib.Algebra.Module.LinearMap.Defs

Goal state before:
pp: R : Type u_1
S : Type u_5
M₃ : Type u_11
inst✝³ : Semiring R
inst✝² : Semiring S
inst✝¹ : AddCommMonoid M₃
inst✝ : Module S M₃
σ : R →+* S
f g : R →ₛₗ[σ] M₃
h : f 1 = g 1
x : R
⊢ σ x • f 1 = σ x • g 1

Tactic:
h

Goal state after:
R : Type u_1
S : Type u_5
M₃ : Type u_11
inst✝³ : Semiring R
inst✝² : Semiring S
inst✝¹ : AddCommMonoid M₃
inst✝ : Module S M₃
σ : R →+* S
f g : R →ₛₗ[σ] M₃
h : f 1 = g 1
x : R
⊢ σ x • g 1 = σ x • g 1
Module: Mathlib.Algebra.Module.LinearMap.Defs

Goal state before:
pp: M : Type u_8
M₂ : Type u_10
inst✝¹ : AddCommMonoid M
inst✝ : AddCommMonoid M₂
f g : M →+ M₂
⊢ f.toNatLinearMap = g.toNatLinearMap → f = g

Tactic:
h

Goal state after:
M : Type u_8
M₂ : Type u_10
inst✝¹ : AddCommMonoid M
inst✝ : AddCommMonoid M₂
f g : M →+ M₂
h : f.toNatLinearMap = g.toNatLinearMap
⊢ f = g
Module: Mathlib.Algebra.Module.LinearMap.Defs

Goal state before:
pp: M : Type u_8
M₂ : Type u_10
inst✝¹ : AddCommGroup M
inst✝ : AddCommGroup M₂
f g : M →+ M₂
⊢ f.toIntLinearMap = g.toIntLinearMap → f = g

Tactic:
h

Goal state after:
M : Type u_8
M₂ : Type u_10
inst✝¹ : AddCommGroup M
inst✝ : AddCommGroup M₂
f g : M →+ M₂
h : f.toIntLinearMap = g.toIntLinearMap
⊢ f = g
Module: Mathlib.GroupTheory.GroupAction.Hom

Goal state before:
pp: M' : Type u_1
X : Type u_5
inst✝⁴ : SMul M' X
Y : Type u_6
inst✝³ : SMul M' Y
F : Type u_8
inst✝² : FunLike F X Y
inst✝¹ : FaithfulSMul M' X
inst✝ : MulActionHomClass F M' X Y
f : F
hf : Function.Injective ⇑f
x✝¹ x✝ : M'
h : ∀ (a : Y), x✝¹ • a = x✝ • a
m : X
⊢ x✝¹ • f m = x✝ • f m

Tactic:
h

Goal state after:
Module: Mathlib.GroupTheory.GroupAction.Hom

Goal state before:
pp: R : Type u_10
inst✝³ : Semiring R
S : Type u_11
inst✝² : Semiring S
N' : Type u_13
inst✝¹ : AddMonoid N'
inst✝ : DistribMulAction S N'
σ : R →* S
f g : R →ₑ+[σ] N'
h : f 1 = g 1
x : R
⊢ σ x • f 1 = σ x • g 1

Tactic:
h

Goal state after:
R : Type u_10
inst✝³ : Semiring R
S : Type u_11
inst✝² : Semiring S
N' : Type u_13
inst✝¹ : AddMonoid N'
inst✝ : DistribMulAction S N'
σ : R →* S
f g : R →ₑ+[σ] N'
h : f 1 = g 1
x : R
⊢ σ x • g 1 = σ x • g 1
Module: Mathlib.Algebra.Module.Torsion.Free

Goal state before:
pp: R : Type u_1
M : Type u_3
inst✝⁴ : Semiring R
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : Nontrivial M
inst✝ : IsAddTorsionFree M
⊢ CharZero R

Tactic:
refine ⟨fun {n m h} ↦ ?_⟩

Goal state after:
R : Type u_1
M : Type u_3
inst✝⁴ : Semiring R
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : Nontrivial M
inst✝ : IsAddTorsionFree M
n m : ℕ
h : ↑n = ↑m
⊢ n = m
Module: Mathlib.Algebra.Module.Submodule.Lattice

Goal state before:
pp: R : Type u_1
M : Type u_3
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
ι : Sort u_4
p : ι → Submodule R M
⊢ ⋂ p_1 ∈ Set.range fun i ↦ p i, ↑p_1 = ⋂ i, ↑(p i)

Tactic:
simp only [Set.mem_range, Set.iInter_exists, Set.iInter_iInter_eq']

Goal state after:
Module: Mathlib.Order.Hom.CompleteLattice

Goal state before:
pp: F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
δ : Type u_5
ι : Sort u_6
κ : ι → Sort u_7
inst✝³ : FunLike F α β
inst✝² : CompleteLattice α
inst✝¹ : CompleteLattice β
inst✝ : sSupHomClass F α β
f : F
a b : α
⊢ f (sSup {a, b}) = f a ⊔ f b

Tactic:
map_sSup

Goal state after:
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
δ : Type u_5
ι : Sort u_6
κ : ι → Sort u_7
inst✝³ : FunLike F α β
inst✝² : CompleteLattice α
inst✝¹ : CompleteLattice β
inst✝ : sSupHomClass F α β
f : F
a b : α
⊢ sSup (⇑f '' {a, b}) = f a ⊔ f b
Module: Mathlib.Algebra.Module.Submodule.Ker

Goal state before:
pp: R : Type u_1
R₂ : Type u_2
M : Type u_5
M₂ : Type u_7
inst✝⁵ : Semiring R
inst✝⁴ : Semiring R₂
inst✝³ : AddCommMonoid M
inst✝² : AddCommMonoid M₂
inst✝¹ : Module R M
inst✝ : Module R₂ M₂
τ₁₂ : R →+* R₂
N : Submodule R M
f : M →ₛₗ[τ₁₂] M₂
⊢ N ≤ f.ker ↔ f ∘ₛₗ N.subtype = 0

Tactic:
rw [SetLike.le_def, LinearMap.ext_iff, Subtype.forall]

Goal state after:
R : Type u_1
R₂ : Type u_2
M : Type u_5
M₂ : Type u_7
inst✝⁵ : Semiring R
inst✝⁴ : Semiring R₂
inst✝³ : AddCommMonoid M
inst✝² : AddCommMonoid M₂
inst✝¹ : Module R M
inst✝ : Module R₂ M₂
τ₁₂ : R →+* R₂
N : Submodule R M
f : M →ₛₗ[τ₁₂] M₂
⊢ (∀ ⦃x : M⦄, x ∈ N → x ∈ f.ker) ↔ ∀ (a : M) (b : a ∈ N), (f ∘ₛₗ N.subtype) ⟨a, b⟩ = 0 ⟨a, b⟩
Module: Mathlib.Algebra.Ring.CharZero

Goal state before:
pp: R : Type u_2
S : Type u_3
inst✝² : NonAssocSemiring R
inst✝¹ : NonAssocSemiring S
ϕ : R →+* S
inst✝ : CharZero S
a b : ℕ
h : ↑a = ↑b
⊢ ϕ ↑a = ϕ ↑b

Tactic:
h

Goal state after:
R : Type u_2
S : Type u_3
inst✝² : NonAssocSemiring R
inst✝¹ : NonAssocSemiring S
ϕ : R →+* S
inst✝ : CharZero S
a b : ℕ
h : ↑a = ↑b
⊢ ϕ ↑b = ϕ ↑b
Module: Mathlib.Algebra.Ring.CharZero

Goal state before:
pp: R : Type u_2
S : Type u_3
inst✝¹ : NonAssocSemiring R
inst✝ : NonAssocSemiring S
ϕ : R →+* S
hϕ : Injective ⇑ϕ
hR : CharZero R
a b : ℕ
⊢ ↑a = ↑b → a = b

Tactic:
h

Goal state after:
R : Type u_2
S : Type u_3
inst✝¹ : NonAssocSemiring R
inst✝ : NonAssocSemiring S
ϕ : R →+* S
hϕ : Injective ⇑ϕ
hR : CharZero R
a b : ℕ
h : ↑a = ↑b
⊢ a = b
Module: Mathlib.Algebra.Ring.Center

Goal state before:
pp: M : Type u_1
inst✝ : NonUnitalNonAssocRing M
a : M
ha : a ∈ center M
x✝¹ x✝ : M
⊢ -a * (x✝¹ * x✝) = -a * x✝¹ * x✝

Tactic:
by rw [neg_mul, ha.left_assoc, neg_mul, neg_mul]

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

Goal state before:
pp: R : Type u_1
A : Type u_2
inst✝⁴ : CommRing R
inst✝³ : Ring A
inst✝² : Algebra R A
inst✝¹ : IsDomain R
inst✝ : IsDomain A
⊢ IsTorsionFree R A ↔ Injective ⇑(algebraMap R A)

Tactic:
rw [isTorsionFree_iff_faithfulSMul, faithfulSMul_iff_algebraMap_injective]

Goal state after:
Module: Mathlib.Algebra.Prime.Lemmas

Goal state before:
pp: M : Type u_1
inst✝¹ : CommMonoidWithZero M
inst✝ : IsCancelMulZero M
p a : M
n : ℕ
hp : Prime p
x : M
hb : ¬p ^ 2 ∣ p * x
hbdiv : p ∣ (p * x) ^ n
y : M
hy : a ^ n.succ * (p * x) ^ n = p ^ n.succ * y
⊢ p ^ n * (a ^ n.succ * x ^ n) = a ^ n.succ * (p * x) ^ n

Tactic:
mul_pow,

Goal state after:
M : Type u_1
inst✝¹ : CommMonoidWithZero M
inst✝ : IsCancelMulZero M
p a : M
n : ℕ
hp : Prime p
x : M
hb : ¬p ^ 2 ∣ p * x
hbdiv : p ∣ (p * x) ^ n
y : M
hy : a ^ n.succ * (p * x) ^ n = p ^ n.succ * y
⊢ p ^ n * (a ^ n.succ * x ^ n) = a ^ n.succ * (p ^ n * x ^ n)
Module: Mathlib.Algebra.Ring.Subring.Basic

Goal state before:
pp: R : Type u_1
inst✝ : Ring R
s : Set R
C : R → Prop
x : R
hx : x ∈ closure s
h1 : C 1
hneg1 : C (-1)
hs : ∀ z ∈ s, ∀ (n : R), C n → C (z * n)
ha : ∀ {x y : R}, C x → C y → C (x + y)
⊢ C x

Tactic:
by
  have h0 : C 0 := add_neg_cancel (1 : R) ▸ ha h1 hneg1
  rcases exists_list_of_mem_closure hx with ⟨L, HL, rfl⟩
  clear hx
  induction L with
  | nil => exact h0
  | cons hd tl ih => ?_
  rw [List.forall_mem_cons] at HL
  suffices C (List.prod hd) by
    rw [List.map_cons, List.sum_cons]
    exact ha this (ih HL.2)
  replace HL := HL.1
  clear ih tl
  rsuffices ⟨L, HL', HP | HP⟩ :
    ∃ L : List R, (∀ x ∈ L, x ∈ s) ∧ (List.prod hd = List.prod L ∨ List.prod hd = -List.prod L)
  · rw [HP]
    clear HP HL hd
    induction L with
    | nil => exact h1
    | cons hd tl ih =>
      rw [List.forall_mem_cons] at HL'
      rw [List.prod_cons]
      exact hs _ HL'.1 _ (ih HL'.2)
  · rw [HP]
    clear HP HL hd
    induction L with
    | nil => exact hneg1
    | cons hd tl ih =>
      rw [List.prod_cons, neg_mul_eq_mul_neg]
      rw [List.forall_mem_cons] at HL'
      exact hs _ HL'.1 _ (ih HL'.2)
  induction hd with
  | nil => exact ⟨[], List.forall_mem_nil _, Or.inl rfl⟩
  | cons hd tl ih => ?_
  rw [List.forall_mem_cons] at HL
  rcases ih HL.2 with ⟨L, HL', HP | HP⟩ <;> rcases HL.1 with hhd | hhd
  · exact
      ⟨hd::L, List.forall_mem_cons.2 ⟨hhd, HL'⟩,
        Or.inl <| by rw [List.prod_cons, List.prod_cons, HP]⟩
  · exact ⟨L, HL', Or.inr <| by rw [List.prod_cons, hhd, neg_one_mul, HP]⟩
  · exact
      ⟨hd::L, List.forall_mem_cons.2 ⟨hhd, HL'⟩,
        Or.inr <| by rw [List.prod_cons, List.prod_cons, HP, neg_mul_eq_mul_neg]⟩
  · exact ⟨L, HL', Or.inl <| by rw [List.prod_cons, hhd, HP, neg_one_mul, neg_neg]⟩

Goal state after:
Module: Mathlib.Algebra.Module.Submodule.Equiv

Goal state before:
pp: R : Type u_1
R₁ : Type u_2
R₂ : Type u_3
R₃ : Type u_4
M : Type u_5
M₁ : Type u_6
M₂ : Type u_7
M₃ : Type u_8
N : Type u_9
inst✝⁴ : Semiring R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
inst✝¹ : AddCommMonoid N
inst✝ : Module R N
p : Submodule R M
q : Submodule R ↥p
x : M
hx : x ∈ map p.subtype q
⊢ ↥q

Tactic:
refine ⟨⟨x, ?_⟩, ?_⟩

Goal state after:
case refine_1
R : Type u_1
R₁ : Type u_2
R₂ : Type u_3
R₃ : Type u_4
M : Type u_5
M₁ : Type u_6
M₂ : Type u_7
M₃ : Type u_8
N : Type u_9
inst✝⁴ : Semiring R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
inst✝¹ : AddCommMonoid N
inst✝ : Module R N
p : Submodule R M
q : Submodule R ↥p
x : M
hx : x ∈ map p.subtype q
⊢ x ∈ p

case refine_2
R : Type u_1
R₁ : Type u_2
R₂ : Type u_3
R₃ : Type u_4
M : Type u_5
M₁ : Type u_6
M₂ : Type u_7
M₃ : Type u_8
N : Type u_9
inst✝⁴ : Semiring R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
inst✝¹ : AddCommMonoid N
inst✝ : Module R N
p : Submodule R M
q : Submodule R ↥p
x : M
hx : x ∈ map p.subtype q
⊢ ⟨x, ?refine_1⟩ ∈ q
Module: Mathlib.Algebra.Module.Submodule.Equiv

Goal state before:
pp: R : Type u_1
R₁ : Type u_2
R₂ : Type u_3
R₃ : Type u_4
M : Type u_5
M₁ : Type u_6
M₂ : Type u_7
M₃ : Type u_8
N : Type u_9
inst✝⁸ : CommSemiring R
inst✝⁷ : AddCommMonoid M
inst✝⁶ : AddCommMonoid M₁
inst✝⁵ : AddCommMonoid M₂
inst✝⁴ : AddCommMonoid M₃
inst✝³ : Module R M
inst✝² : Module R M₁
inst✝¹ : Module R M₂
inst✝ : Module R M₃
f : M₁ →ₗ[R] M₂ →ₗ[R] M
i : M₃ →ₗ[R] M
hi : Injective ⇑i
hf : ∀ (x : M₁) (y : M₂), (f x) y ∈ i.range
e : ↥i.range ≃ₗ[R] M₃ := (LinearEquiv.ofInjective i hi).symm
t : R
x : M₁
y : M₂
⊢ (↑e ∘ₗ codRestrict i.range (f (t • x)) ⋯) y = ((RingHom.id R) t • ↑e ∘ₗ codRestrict i.range (f x) ⋯) y

Tactic:
simp [f.map_smul, ← e.map_smul, codRestrict]

Goal state after:
Module: Mathlib.Order.ModularLattice

Goal state before:
pp: α : Type u_1
inst✝ : Lattice α
h : ∀ (x y z : α), x ⊓ z ⊔ y ⊓ z = (x ⊓ z ⊔ y) ⊓ z
x✝ y z : α
xz : x✝ ≤ z
⊢ (x✝ ⊓ z ⊔ y) ⊓ z ≤ x✝ ⊓ z ⊔ y ⊓ z

Tactic:
h

Goal state after:
α : Type u_1
inst✝ : Lattice α
h : ∀ (x y z : α), x ⊓ z ⊔ y ⊓ z = (x ⊓ z ⊔ y) ⊓ z
x✝ y z : α
xz : x✝ ≤ z
⊢ (x✝ ⊓ z ⊔ y) ⊓ z ≤ (x✝ ⊓ z ⊔ y) ⊓ z
Module: Mathlib.Order.ModularLattice

Goal state before:
pp: α : Type u_1
a b c : α
inst✝² : Lattice α
inst✝¹ : OrderBot α
inst✝ : IsModularLattice α
h₁ : Disjoint a (b ⊔ c)
h₂ : Disjoint b (c ⊔ a)
⊢ Disjoint c (a ⊔ b)

Tactic:
by
  rw [sup_comm] at h₂ ⊢
  rw [disjoint_comm]
  exact (h₁.mono_right le_sup_right).disjoint_sup_left_of_disjoint_sup_right h₂

Goal state after:
Module: Mathlib.Order.SupClosed

Goal state before:
pp: α : Type u_3
inst✝ : LinearOrder α
s : Set α
a : α
ha : a ∈ s
b : α
hb : b ∈ s
⊢ max a b ∈ s

Tactic:
cases le_total a b <;> simp [*]

Goal state after:
Module: Mathlib.Order.Atoms

Goal state before:
pp: α : Type u_4
inst✝ : Preorder α
⊢ IsStronglyCoatomic αᵒᵈ ↔ IsStronglyAtomic α

Tactic:
rw [← isStronglyAtomic_dual_iff_is_stronglyCoatomic]

Goal state after:
α : Type u_4
inst✝ : Preorder α
⊢ IsStronglyAtomic αᵒᵈᵒᵈ ↔ IsStronglyAtomic α
Module: Mathlib.Order.Atoms

Goal state before:
pp: ι : Sort u_1
α✝ : Type u_2
β : Type u_3
inst✝² : PartialOrder α✝
α : Type u_4
a b : α
inst✝¹ : Preorder α
inst✝ : PredOrder α
⊢ IsStronglyCoatomic α

Tactic:
rw [← isStronglyAtomic_dual_iff_is_stronglyCoatomic]

Goal state after:
ι : Sort u_1
α✝ : Type u_2
β : Type u_3
inst✝² : PartialOrder α✝
α : Type u_4
a b : α
inst✝¹ : Preorder α
inst✝ : PredOrder α
⊢ IsStronglyAtomic αᵒᵈ
Module: Mathlib.LinearAlgebra.Span.Defs

Goal state before:
pp: case pos
R : Type u_1
M : Type u_4
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
p : Submodule R M
S : Set (Submodule R M) := {T | ∃ m ∈ p, m ≠ 0 ∧ T = R ∙ m}
m : M
hm : m ∈ p
h : m = 0
⊢ m ∈ sSup {T | ∃ m ∈ p, m ≠ 0 ∧ T = R ∙ m}

Tactic:
h

Goal state after:
case pos
R : Type u_1
M : Type u_4
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
p : Submodule R M
S : Set (Submodule R M) := {T | ∃ m ∈ p, m ≠ 0 ∧ T = R ∙ m}
m : M
hm : m ∈ p
h : m = 0
⊢ 0 ∈ sSup {T | ∃ m ∈ p, m ≠ 0 ∧ T = R ∙ m}
Module: Mathlib.Order.SupIndep

Goal state before:
pp: α : Type u_1
ι : Type u_3
inst✝¹ : Lattice α
inst✝ : OrderBot α
s t : Finset ι
f : ι → α
i : ι
hs : s.SupIndep f
hts : t ⊆ s
hi : i ∈ s
hf : ∀ (i : ι), f i ≠ ⊥
⊢ f i ≤ t.sup f ↔ i ∈ t

Tactic:
by
  refine ⟨fun h => ?_, le_sup⟩
  by_contra hit
  exact hf i (disjoint_self.1 <| (hs hts hi hit).mono_right h)

Goal state after:
Module: Mathlib.Order.Atoms

Goal state before:
pp: α : Type u_2
β : Type u_3
inst✝⁴ : PartialOrder α
inst✝³ : PartialOrder β
inst✝² : OrderBot α
inst✝¹ : IsAtomic α
inst✝ : OrderBot β
l : α → β
u : β → α
gi : GaloisInsertion l u
hbot : u ⊥ = ⊥
h_atom : ∀ (a : α), IsAtom a → u (l a) = a
a : α
⊢ IsAtom (l a) ↔ IsAtom a

Tactic:
refine ⟨fun hla => ?_, fun ha => gi.isAtom_of_u_bot hbot ((h_atom a ha).symm ▸ ha)⟩

Goal state after:
α : Type u_2
β : Type u_3
inst✝⁴ : PartialOrder α
inst✝³ : PartialOrder β
inst✝² : OrderBot α
inst✝¹ : IsAtomic α
inst✝ : OrderBot β
l : α → β
u : β → α
gi : GaloisInsertion l u
hbot : u ⊥ = ⊥
h_atom : ∀ (a : α), IsAtom a → u (l a) = a
a : α
hla : IsAtom (l a)
⊢ IsAtom a
Module: Mathlib.Order.Atoms

Goal state before:
pp: α : Type u_2
inst✝³ : Lattice α
inst✝² : OrderTop α
inst✝¹ : IsLowerModularLattice α
inst✝ : IsCoatomistic α
⊢ IsStronglyCoatomic α

Tactic:
rw [← isStronglyAtomic_dual_iff_is_stronglyCoatomic]

Goal state after:
α : Type u_2
inst✝³ : Lattice α
inst✝² : OrderTop α
inst✝¹ : IsLowerModularLattice α
inst✝ : IsCoatomistic α
⊢ IsStronglyAtomic αᵒᵈ
Module: Mathlib.Order.SupIndep

Goal state before:
pp: α : Type u_1
ι : Type u_3
inst✝² : Lattice α
inst✝¹ : IsModularLattice α
inst✝ : OrderBot α
s : Finset ι
f : ι → α
u v : Finset ι
hs : s.SupIndep f
hu : u ⊆ s
hv : v ⊆ s
huv : Disjoint u v
⊢ Disjoint (u.sup f) (v.sup f)

Tactic:
induction u using Finset.induction generalizing v with
  | empty => simp
  | insert x u hx ih =>
    grind [= SupIndep, Disjoint.disjoint_sup_left_of_disjoint_sup_right]

Goal state after: