mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Algebra.BigOperators.Group.Finset.Piecewise

Goal state before:
pp: case neg
ι : Type u_1
M : Type u_3
inst✝¹ : CommMonoid M
inst✝ : DecidableEq ι
s : Finset ι
a : ι
b : (x : ι) → a = x → M
h : a ∉ s
⊢ (∏ x ∈ s, if h : a = x then b x h else 1) = 1

Tactic:
· rw [Finset.prod_eq_one]
    grind

Goal state after:
Module: Mathlib.Algebra.BigOperators.Group.Finset.Piecewise

Goal state before:
pp: case neg
ι : Type u_1
M : Type u_3
inst✝¹ : CommMonoid M
inst✝ : DecidableEq ι
s : Finset ι
a : ι
b : (x : ι) → x = a → M
h : a ∉ s
⊢ (∏ x ∈ s, if h : x = a then b x h else 1) = 1

Tactic:
· rw [Finset.prod_eq_one]
    grind

Goal state after:
Module: Mathlib.Control.Applicative

Goal state before:
pp: F : Type u → Type w
G : Type v → Type u
inst✝³ : Applicative F
inst✝² : Applicative G
inst✝¹ : LawfulApplicative F
inst✝ : LawfulApplicative G
α β γ : Type v
⊢ ∀ {α β : Type v} (x : Comp F G α) (y : Comp F G β), x <* y = const β <$> x <*> y

Tactic:
by intros; rfl

Goal state after:
Module: Mathlib.Control.Applicative

Goal state before:
pp: F : Type u → Type w
G : Type v → Type u
inst✝³ : Applicative F
inst✝² : Applicative G
inst✝¹ : LawfulApplicative F
inst✝ : LawfulApplicative G
α β γ : Type v
⊢ ∀ {α β : Type v} (x : Comp F G α) (y : Comp F G β), x *> y = const α id <$> x <*> y

Tactic:
by intros; rfl

Goal state after:
Module: Mathlib.Dynamics.FixedPoints.Basic

Goal state before:
pp: α : Type u_1
f g : α → α
h : Function.Commute f g
⊢ Set.InvOn f g (fixedPoints (f ∘ g)) (fixedPoints (f ∘ g))

Tactic:
simpa only [h.comp_eq] using Function.invOn_fixedPoints_comp f g

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

Goal state before:
pp: α : Type u_3
inst✝ : SemilatticeSup α
f : α →o α
h : ∀ (a₁ a₂ : α), f (a₁ ⊔ a₂) ≤ f a₁ ⊔ a₂
n₁ n₂ : ℕ
a₁ a₂ : α
h' : ∀ (n : ℕ) (a₁ a₂ : α), (⇑f)^[n] (a₁ ⊔ a₂) ≤ (⇑f)^[n] a₁ ⊔ a₂
⊢ (⇑f)^[n₁] ((⇑f)^[n₂] (a₁ ⊔ a₂)) = (⇑f)^[n₁] ((⇑f)^[n₂] (a₂ ⊔ a₁))

Tactic:
by rw [sup_comm]

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

Goal state before:
pp: α : Type u_3
inst✝ : SemilatticeSup α
f : α →o α
h : ∀ (a₁ a₂ : α), f (a₁ ⊔ a₂) ≤ f a₁ ⊔ a₂
n₁ n₂ : ℕ
a₁ a₂ : α
h' : ∀ (n : ℕ) (a₁ a₂ : α), (⇑f)^[n] (a₁ ⊔ a₂) ≤ (⇑f)^[n] a₁ ⊔ a₂
⊢ (⇑f)^[n₁] ((⇑f)^[n₂] a₂ ⊔ a₁) = (⇑f)^[n₁] (a₁ ⊔ (⇑f)^[n₂] a₂)

Tactic:
by rw [sup_comm]

Goal state after:
Module: Mathlib.Order.OmegaCompletePartialOrder

Goal state before:
pp: ι : Sort u_1
α : Type u_2
β : Type u_3
γ : Type u_4
δ : Type u_5
c : Chain (Part α)
i : ℕ
x : α
⊢ x ∈ c i → x ∈ Part.ωSup c

Tactic:
hx

Goal state after:
ι : Sort u_1
α : Type u_2
β : Type u_3
γ : Type u_4
δ : Type u_5
c : Chain (Part α)
i : ℕ
x : α
hx : x ∈ c i
⊢ x ∈ Part.ωSup c
Module: Mathlib.Order.OmegaCompletePartialOrder

Goal state before:
pp: ι : Sort u_1
α : Type u_2
β : Type u_3
γ : Type u_4
δ : Type u_5
⊢ ∀ (c : Chain (Part α)) (x : Part α), (∀ (i : ℕ), c i ≤ x) → Part.ωSup c ≤ x

Tactic:
by
    rintro c x hx a ha
    replace ha := mem_chain_of_mem_ωSup ha
    obtain ⟨i, ha⟩ := ha
    apply hx i
    rw [← ha]
    apply mem_some

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

Goal state before:
pp: case refine_1
α : Type u
β : Type v
f : α → β
g : β → α
hf : Injective f
hg : Injective g
R : α → β → Prop
hp₁ : ∀ (a : α), R a (f a)
hp₂ : ∀ (b : β), R (g b) b
hβ : Nonempty β
F : Set α →o Set α := { toFun := fun s ↦ (g '' (f '' s)ᶜ)ᶜ, monotone' := ⋯ }
s : Set α := OrderHom.lfp F
hs : (g '' (f '' s)ᶜ)ᶜ = s
hns : g '' (f '' s)ᶜ = sᶜ
g' : α → β := invFun g
g'g : LeftInverse g' g
hg'ns : g' '' sᶜ = (f '' s)ᶜ
h : α → β := s.piecewise f g'
this : Surjective h
x : α
⊢ x ∈ sᶜ → ∀ ⦃x₂ : α⦄, x₂ ∈ sᶜ → g' x = g' x₂ → x = x₂

Tactic:
hx

Goal state after:
case refine_1
α : Type u
β : Type v
f : α → β
g : β → α
hf : Injective f
hg : Injective g
R : α → β → Prop
hp₁ : ∀ (a : α), R a (f a)
hp₂ : ∀ (b : β), R (g b) b
hβ : Nonempty β
F : Set α →o Set α := { toFun := fun s ↦ (g '' (f '' s)ᶜ)ᶜ, monotone' := ⋯ }
s : Set α := OrderHom.lfp F
hs : (g '' (f '' s)ᶜ)ᶜ = s
hns : g '' (f '' s)ᶜ = sᶜ
g' : α → β := invFun g
g'g : LeftInverse g' g
hg'ns : g' '' sᶜ = (f '' s)ᶜ
h : α → β := s.piecewise f g'
this : Surjective h
x : α
hx : x ∈ sᶜ
⊢ ∀ ⦃x₂ : α⦄, x₂ ∈ sᶜ → g' x = g' x₂ → x = x₂
Module: Mathlib.SetTheory.Cardinal.SchroederBernstein

Goal state before:
pp: case refine_2
α : Type u
β : Type v
f : α → β
g : β → α
hf : Injective f
hg : Injective g
R : α → β → Prop
hp₁ : ∀ (a : α), R a (f a)
hp₂ : ∀ (b : β), R (g b) b
hβ : Nonempty β
F : Set α →o Set α := { toFun := fun s ↦ (g '' (f '' s)ᶜ)ᶜ, monotone' := ⋯ }
s : Set α := OrderHom.lfp F
hs : (g '' (f '' s)ᶜ)ᶜ = s
hns : g '' (f '' s)ᶜ = sᶜ
g' : α → β := invFun g
g'g : LeftInverse g' g
hg'ns : g' '' sᶜ = (f '' s)ᶜ
h : α → β := s.piecewise f g'
this : Surjective h
x : α
⊢ x ∈ s → ∀ y ∉ s, f x ≠ g' y

Tactic:
hx

Goal state after:
case refine_2
α : Type u
β : Type v
f : α → β
g : β → α
hf : Injective f
hg : Injective g
R : α → β → Prop
hp₁ : ∀ (a : α), R a (f a)
hp₂ : ∀ (b : β), R (g b) b
hβ : Nonempty β
F : Set α →o Set α := { toFun := fun s ↦ (g '' (f '' s)ᶜ)ᶜ, monotone' := ⋯ }
s : Set α := OrderHom.lfp F
hs : (g '' (f '' s)ᶜ)ᶜ = s
hns : g '' (f '' s)ᶜ = sᶜ
g' : α → β := invFun g
g'g : LeftInverse g' g
hg'ns : g' '' sᶜ = (f '' s)ᶜ
h : α → β := s.piecewise f g'
this : Surjective h
x : α
hx : x ∈ s
⊢ ∀ y ∉ s, f x ≠ g' y
Module: Mathlib.SetTheory.Cardinal.Order

Goal state before:
pp: a : Cardinal.{u}
h✝ : succ (lift.{v, u} a) < lift.{v, u} (succ a)
b : Cardinal.{u}
h : succ (lift.{v, u} a) ≤ lift.{v, u} a
hb : lift.{v, u} b = succ (lift.{v, u} a)
⊢ False

Tactic:
exact h.not_gt (lt_succ _)

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

Goal state before:
pp: c : Cardinal.{u_1}
hc : c.IsStrongLimit
⊢ IsSuccLimit c

Tactic:
rw [Cardinal.isSuccLimit_iff]

Goal state after:
c : Cardinal.{u_1}
hc : c.IsStrongLimit
⊢ c ≠ 0 ∧ IsSuccPrelimit c
Module: Mathlib.SetTheory.Cardinal.Order

Goal state before:
pp: α : Type u
x✝ : Nonempty (Cardinal.{u} ↪ α)
f : Cardinal.{u} → α
hf : Injective f
g : α → Cardinal.{u} := invFun f
x : α
hx : g x = 2 ^ Cardinal.sum g
this : g x ≤ Cardinal.sum g
⊢ Cardinal.sum g < g x

Tactic:
hx

Goal state after:
α : Type u
x✝ : Nonempty (Cardinal.{u} ↪ α)
f : Cardinal.{u} → α
hf : Injective f
g : α → Cardinal.{u} := invFun f
x : α
hx : g x = 2 ^ Cardinal.sum g
this : g x ≤ Cardinal.sum g
⊢ Cardinal.sum g < 2 ^ Cardinal.sum g
Module: Mathlib.Order.OmegaCompletePartialOrder

Goal state before:
pp: α : Type u_2
inst✝ : OmegaCompletePartialOrder α
f : α →𝒄 α
x : α
h : x ≤ f x
a : α
h_a : f a ≤ a
h_x_le_a : x ≤ a
n : ℕ
⊢ (iterateChain (↑f) x h) n ≤ a

Tactic:
induction n with
  | zero => exact h_x_le_a
  | succ n h_ind =>
    have : iterateChain f x h (n.succ) = f (iterateChain f x h n) :=
      Function.iterate_succ_apply' ..
    rw [this]
    exact le_trans (f.monotone h_ind) h_a

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

Goal state before:
pp: case inr
c : Cardinal.{u}
d : Cardinal.{v}
h : ∀ (n : ℕ), ↑n ≤ c ↔ ↑n ≤ d
h' : ℵ₀ ≤ c ↔ ℵ₀ ≤ d
hc : ¬ℵ₀ ≤ c
hd : ¬ℵ₀ ≤ d
⊢ toNat c = toNat d

Tactic:
apply eq_of_forall_le_iff
    rw [← cast_toNat_of_lt_aleph0 (not_le.mp hc), ← cast_toNat_of_lt_aleph0 (not_le.mp hd)] at h
    simpa using h

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

Goal state before:
pp: case e'_3
ι : Sort u_1
f : ι → Cardinal.{v}
⊢ (range fun i ↦ lift.{u, v} (f i)) = lift.{u, v} '' range f

Tactic:
simp_rw [← comp_apply (f := lift), range_comp]

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

Goal state before:
pp: h : Small.{u, max (u + 1) (v + 1)} Cardinal.{max u v}
this : BddAbove univ
⊢ False

Tactic:
exact not_bddAbove_univ this

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

Goal state before:
pp: ⊢ IsSuccLimit ℵ₀

Tactic:
rw [Cardinal.isSuccLimit_iff]

Goal state after:
⊢ ℵ₀ ≠ 0 ∧ IsSuccPrelimit ℵ₀
Module: Mathlib.SetTheory.Cardinal.Basic

Goal state before:
pp: α : Type u
n : ℕ
t : Set α
H : ∀ (s : Finset α), ↑s ⊆ t → s.card ≤ n
⊢ #↑t ≤ ↑n

Tactic:
apply card_le_of (fun s ↦ ?_)

Goal state after:
α : Type u
n : ℕ
t : Set α
H : ∀ (s : Finset α), ↑s ⊆ t → s.card ≤ n
s : Finset ↑t
⊢ s.card ≤ n
Module: Mathlib.SetTheory.Cardinal.Basic

Goal state before:
pp: α β : Type u
f : α → β
s : Set β
h : Injective f
h2 : s ⊆ range f
⊢ #↑(f ⁻¹' s) = #↑s

Tactic:
convert! mk_preimage_of_injective_of_subset_range_lift.{u, u} f s h h2 using 1 <;> rw [lift_id]

Goal state after:
Module: Mathlib.Algebra.Group.Action.Prod

Goal state before:
pp: case e_4.e_3
M : Type u_1
N : Type u_2
P : Type u_3
E : Type u_4
α : Type u_5
β : Type u_6
inst✝¹ : Monoid M
inst✝ : Monoid N
hM : MulAction M α
hN : MulAction N α
snd✝ : SMulCommClass M N α
⊢ compHom α (MonoidHom.inr M N) = hN

Tactic:
ext n a; (conv_rhs => rw [← hM.one_smul (SMul.smul n a)]); rfl

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

Goal state before:
pp: R : Type u_1
R₁ : Type u_2
R₂ : Type u_3
R₃ : Type u_4
S : Type u_5
S₃ : Type u_6
T : Type u_7
M : Type u_8
M₁ : Type u_9
M₂ : Type u_10
M₃ : Type u_11
N₂ : Type u_12
N₃ : Type u_13
inst✝¹⁴ : Semiring R₁
inst✝¹³ : Semiring R₂
inst✝¹² : Semiring R₃
inst✝¹¹ : AddCommMonoid M
inst✝¹⁰ : AddCommMonoid M₂
inst✝⁹ : AddCommMonoid M₃
inst✝⁸ : AddCommGroup N₂
inst✝⁷ : AddCommGroup N₃
inst✝⁶ : Module R₁ M
inst✝⁵ : Module R₂ M₂
inst✝⁴ : Module R₃ M₃
inst✝³ : Module R₂ N₂
inst✝² : Module R₃ N₃
σ₁₂ : R₁ →+* R₂
σ₂₃ : R₂ →+* R₃
σ₁₃ : R₁ →+* R₃
inst✝¹ : RingHomCompTriple σ₁₂ σ₂₃ σ₁₃
inst✝ : Subsingleton M
f : M →ₛₗ[σ₁₂] M₂
x : M
⊢ 0 = default 0

Tactic:
map_zero

Goal state after:
R : Type u_1
R₁ : Type u_2
R₂ : Type u_3
R₃ : Type u_4
S : Type u_5
S₃ : Type u_6
T : Type u_7
M : Type u_8
M₁ : Type u_9
M₂ : Type u_10
M₃ : Type u_11
N₂ : Type u_12
N₃ : Type u_13
inst✝¹⁴ : Semiring R₁
inst✝¹³ : Semiring R₂
inst✝¹² : Semiring R₃
inst✝¹¹ : AddCommMonoid M
inst✝¹⁰ : AddCommMonoid M₂
inst✝⁹ : AddCommMonoid M₃
inst✝⁸ : AddCommGroup N₂
inst✝⁷ : AddCommGroup N₃
inst✝⁶ : Module R₁ M
inst✝⁵ : Module R₂ M₂
inst✝⁴ : Module R₃ M₃
inst✝³ : Module R₂ N₂
inst✝² : Module R₃ N₃
σ₁₂ : R₁ →+* R₂
σ₂₃ : R₂ →+* R₃
σ₁₃ : R₁ →+* R₃
inst✝¹ : RingHomCompTriple σ₁₂ σ₂₃ σ₁₃
inst✝ : Subsingleton M
f : M →ₛₗ[σ₁₂] M₂
x : M
⊢ 0 = 0
Module: Mathlib.GroupTheory.GroupAction.Hom

Goal state before:
pp: M' : Type u_1
M : Type u_2
N : Type u_3
P : Type u_4
φ : M → N
ψ : N → P
χ : M → P
X : Type u_5
inst✝⁴ : SMul M X
inst✝³ : SMul M' X
Y : Type u_6
inst✝² : SMul N Y
inst✝¹ : SMul M' Y
Z : Type u_7
inst✝ : SMul P Z
g : Y →ₑ[ψ] Z
f : X →ₑ[φ] Y
κ : CompTriple φ ψ χ
m : M
x : X
⊢ (ψ ∘ φ) m • g (f x) = χ m • g (f x)

Tactic:
by rw [κ.comp_eq]

Goal state after:
Module: Mathlib.Algebra.Module.LinearMap.End

Goal state before:
pp: R : Type u_1
M : Type u_4
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
f : End R M
m : M
k l : ℕ
hk : k ≤ l
hm : (f ^ k) m = 0
⊢ (f ^ (l - k)) 0 = 0

Tactic:
map_zero

Goal state after:
R : Type u_1
M : Type u_4
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
f : End R M
m : M
k l : ℕ
hk : k ≤ l
hm : (f ^ k) m = 0
⊢ 0 = 0
Module: Mathlib.Algebra.Ring.PUnit

Goal state before:
pp: ⊢ ∀ (a : PUnit), 0 * a = 0

Tactic:
by intros; rfl

Goal state after:
Module: Mathlib.Algebra.Ring.PUnit

Goal state before:
pp: ⊢ ∀ (a : PUnit), a * 0 = 0

Tactic:
by intros; rfl

Goal state after:
Module: Mathlib.Algebra.Ring.PUnit

Goal state before:
pp: ⊢ ∀ (a b c : PUnit), a * (b + c) = a * b + a * c

Tactic:
by intros; rfl

Goal state after:
Module: Mathlib.Algebra.Ring.PUnit

Goal state before:
pp: ⊢ ∀ (a b c : PUnit), (a + b) * c = a * c + b * c

Tactic:
by intros; rfl

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

Goal state before:
pp: R : Type u_1
M : Type u_2
inst✝² : Monoid R
inst✝¹ : AddCommMonoid M
inst✝ : DistribMulAction R M
x y : { v // v ≠ 0 }
a : Rˣ
ha : (fun m ↦ m • ↑y) a = ↑x
⊢ (fun m ↦ m • y) a = x

Tactic:
by ext; simpa

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

Goal state before:
pp: R : Type u_1
R₂ : Type u_2
K : Type u_3
S : Type u_4
M : Type u_5
M₁ : Type u_6
M₂ : Type u_7
M₃ : Type u_8
inst✝⁹ : Semiring R
inst✝⁸ : Semiring R₂
inst✝⁷ : AddCommMonoid M
inst✝⁶ : AddCommMonoid M₂
inst✝⁵ : Module R M
inst✝⁴ : Module R₂ M₂
σ₁₂ : R →+* R₂
σ₂₁ : R₂ →+* R
inst✝³ : RingHomInvPair σ₁₂ σ₂₁
inst✝² : RingHomInvPair σ₂₁ σ₁₂
inst✝¹ : Subsingleton R
inst✝ : Subsingleton R₂
⊢ Unique (M ≃ₛₗ[σ₁₂] M₂)

Tactic:
haveI := Module.subsingleton R M
  haveI := Module.subsingleton R₂ M₂
  infer_instance

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

Goal state before:
pp: case inl
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✝ : SupSet α
x✝ : CompleteLattice β
⊢ ⊥ = sSup ((fun x ↦ ⊥) '' ∅)

pp: case inr
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✝ : SupSet α
x✝ : CompleteLattice β
s : Set α
hs : s.Nonempty
⊢ ⊥ = sSup ((fun x ↦ ⊥) '' s)

Tactic:
· rw [Set.image_empty, sSup_empty]

Goal state after:
case inr
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✝ : SupSet α
x✝ : CompleteLattice β
s : Set α
hs : s.Nonempty
⊢ ⊥ = sSup ((fun x ↦ ⊥) '' s)
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 α
x : α × α
s : Set (α × α)
⊢ (sSup s).1 ⊔ (sSup s).2 = sSup ((fun x ↦ x.1 ⊔ x.2) '' s)

Tactic:
simp_rw [Prod.fst_sSup, Prod.snd_sSup, sSup_image, iSup_sup_eq]

Goal state after:
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₂
p : Submodule R M
q : Submodule R₂ M₂
f : M →ₛₗ[τ₁₂] M₂
hf : ∀ x ∈ p, f x ∈ q
⊢ (f.restrict hf).ker = comap p.subtype f.ker

Tactic:
by
  rw [restrict_eq_codRestrict_domRestrict, ker_codRestrict, ker_domRestrict]

Goal state after:
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₂
f : M →ₛₗ[τ₁₂] M₂
hf : Injective ⇑f
x : M
⊢ x ∈ f.ker → x ∈ ⊥

Tactic:
hx

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₂
f : M →ₛₗ[τ₁₂] M₂
hf : Injective ⇑f
x : M
hx : x ∈ f.ker
⊢ x ∈ ⊥
Module: Mathlib.Algebra.Module.Submodule.Ker

Goal state before:
pp: R : Type u_1
R₂ : Type u_2
R₃ : Type u_3
K : Type u_4
M : Type u_5
M₁ : Type u_6
M₂ : Type u_7
M₃ : Type u_8
V : Type u_9
V₂ : Type u_10
inst✝⁹ : Semiring R
inst✝⁸ : Semiring R₂
inst✝⁷ : Semiring R₃
inst✝⁶ : AddCommMonoid M
inst✝⁵ : AddCommMonoid M₂
inst✝⁴ : AddCommMonoid M₃
inst✝³ : Module R M
inst✝² : Module R₂ M₂
inst✝¹ : Module R₃ M₃
τ₁₂ : R →+* R₂
τ₂₃ : R₂ →+* R₃
τ₁₃ : R →+* R₃
inst✝ : RingHomCompTriple τ₁₂ τ₂₃ τ₁₃
f : M →ₗ[R] M
n : ℕ
x : M
h : (f ^ n) x = 0
c : ℕ
w : n ≤ n + c
⊢ (f ^ c) 0 = 0

Tactic:
map_zero

Goal state after:
R : Type u_1
R₂ : Type u_2
R₃ : Type u_3
K : Type u_4
M : Type u_5
M₁ : Type u_6
M₂ : Type u_7
M₃ : Type u_8
V : Type u_9
V₂ : Type u_10
inst✝⁹ : Semiring R
inst✝⁸ : Semiring R₂
inst✝⁷ : Semiring R₃
inst✝⁶ : AddCommMonoid M
inst✝⁵ : AddCommMonoid M₂
inst✝⁴ : AddCommMonoid M₃
inst✝³ : Module R M
inst✝² : Module R₂ M₂
inst✝¹ : Module R₃ M₃
τ₁₂ : R →+* R₂
τ₂₃ : R₂ →+* R₃
τ₁₃ : R →+* R₃
inst✝ : RingHomCompTriple τ₁₂ τ₂₃ τ₁₃
f : M →ₗ[R] M
n : ℕ
x : M
h : (f ^ n) x = 0
c : ℕ
w : n ≤ n + c
⊢ 0 = 0
Module: Mathlib.Algebra.Group.ULift

Goal state before:
pp: α : Type u
β : Type v
x y : ULift α
inst✝ : MulOneClass α
⊢ ∀ (x y : ULift α), Equiv.ulift (x * y) = Equiv.ulift x * Equiv.ulift y

Tactic:
by intros; rfl

Goal state after:
Module: Mathlib.Algebra.GroupWithZero.ULift

Goal state before:
pp: α : Type u
inst✝ : MulZeroOneClass α
⊢ ∀ (a b : ULift α), Equiv.ulift (a * b) = Equiv.ulift a * Equiv.ulift b

Tactic:
by intros; rfl

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

Goal state before:
pp: K : Type u_9
V : Type u_10
V₂ : Type u_11
inst✝⁴ : Semifield K
inst✝³ : AddCommMonoid V
inst✝² : Module K V
inst✝¹ : AddCommMonoid V₂
inst✝ : Module K V₂
f : V →ₗ[K] V₂
p : Submodule K V
a : K
h : a ≠ 0
⊢ map f p ≤ map (a • f) p

Tactic:
rw [map_le_iff_le_comap, ← comap_smul f _ a h, ← map_le_iff_le_comap]

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

Goal state before:
pp: R : Type u
S : Type v
inst✝¹ : NonAssocSemiring R
inst✝ : NonAssocSemiring S
s : Set R
sm : Submonoid R
hm : ↑sm = s
sa : AddSubmonoid R
ha : ↑sa = s
⊢ 0 ∈ s

Tactic:
exact ha ▸ sa.zero_mem

Goal state after:
Module: Mathlib.Algebra.Ring.Prod

Goal state before:
pp: R : Type u_1
R' : Type u_2
S : Type u_3
S' : Type u_4
T : Type u_5
inst✝¹ : Distrib R
inst✝ : Distrib S
x✝² x✝¹ x✝ : R × S
⊢ (x✝² + x✝¹) * x✝ = x✝² * x✝ + x✝¹ * x✝

Tactic:
ext <;> exact right_distrib ..

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

Goal state before:
pp: case add
R : Type u
inst✝ : NonUnitalNonAssocRing R
s : Set R
x x✝ y✝ : R
hx✝ : x✝ ∈ closure s
hy✝ : y✝ ∈ closure s
hx : x✝ ∈ AddSubgroup.closure ↑(Subsemigroup.closure s)
hy : y✝ ∈ AddSubgroup.closure ↑(Subsemigroup.closure s)
⊢ x✝ + y✝ ∈ AddSubgroup.closure ↑(Subsemigroup.closure s)

Tactic:
exact add_mem hx hy

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

Goal state before:
pp: R : Type u_1
A : Type u_2
inst✝⁷ : CommSemiring R
inst✝⁶ : Semiring A
inst✝⁵ : Algebra R A
inst✝⁴ : FaithfulSMul R A
G : Type u_3
inst✝³ : Monoid G
inst✝² : MulSemiringAction G A
inst✝¹ : SMul G R
inst✝ : SMulDistribClass G R A
x✝ : R
⊢ 1 • x✝ = x✝

Tactic:
by
    apply FaithfulSMul.algebraMap_injective R A
    rw [algebraMap.smul', one_smul]

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

Goal state before:
pp: case add
R : Type u
inst✝ : NonAssocRing R
s : Set R
x x✝ y✝ : R
hx✝ : x✝ ∈ closure s
hy✝ : y✝ ∈ closure s
hx : x✝ ∈ AddSubgroup.closure ↑(Submonoid.closure s)
hy : y✝ ∈ AddSubgroup.closure ↑(Submonoid.closure s)
⊢ x✝ + y✝ ∈ AddSubgroup.closure ↑(Submonoid.closure s)

Tactic:
exact add_mem hx hy

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

Goal state before:
pp: M : Type u_1
N : Type u_2
inst✝⁵ : CommMonoidWithZero M
inst✝⁴ : CommMonoidWithZero N
F : Type u_3
G : Type u_4
inst✝³ : FunLike F M N
inst✝² : MonoidWithZeroHomClass F M N
inst✝¹ : FunLike G N M
inst✝ : MulHomClass G N M
f : F
g : G
p : M
hinv : ∀ (a : M), g (f a) = a
hp : Prime (f p)
a b : M
h : p ∣ a * b
⊢ f p ∣ f a * f b

Tactic:
convert! map_dvd f h

Goal state after:
M : Type u_1
N : Type u_2
inst✝⁵ : CommMonoidWithZero M
inst✝⁴ : CommMonoidWithZero N
F : Type u_3
G : Type u_4
inst✝³ : FunLike F M N
inst✝² : MonoidWithZeroHomClass F M N
inst✝¹ : FunLike G N M
inst✝ : MulHomClass G N M
f : F
g : G
p : M
hinv : ∀ (a : M), g (f a) = a
hp : Prime (f p)
a b : M
h : p ∣ a * b
⊢ f a * f b = f (a * b)
Module: Mathlib.Algebra.GroupWithZero.Associated

Goal state before:
pp: R : Type u_2
inst✝² : CommMonoidWithZero R
inst✝¹ : IsCancelMulZero R
inst✝ : Subsingleton Rˣ
p₁ p₂ : R
k₁ k₂ : ℕ
hp₁ : Prime p₁
hp₂ : Prime p₂
hk₁ : 0 < k₂
h : p₁ ^ k₁ = p₂ ^ k₂
⊢ p₁ = p₂

Tactic:
rw [← associated_iff_eq] at h ⊢
  apply h.of_pow_associated_of_prime' hp₁ hp₂ hk₁

Goal state after:
Module: Mathlib.Algebra.GroupWithZero.Associated

Goal state before:
pp: M : Type u_1
inst✝ : CommMonoid M
a : Associates M
⊢ IsUnit a ↔ a = ⊥

Tactic:
Associates.isUnit_iff_eq_one,

Goal state after:
M : Type u_1
inst✝ : CommMonoid M
a : Associates M
⊢ a = 1 ↔ a = ⊥
Module: Mathlib.Algebra.Ring.Subring.Basic

Goal state before:
pp: case a
R : Type u
S : Type v
inst✝¹ : NonAssocRing R
inst✝ : NonAssocRing S
f : R →+* S
s : Subring R
x : R
⊢ x ∈ comap f (map f s) → x ∈ s ⊔ closure (⇑f ⁻¹' {0})

Tactic:
hx

Goal state after:
case a
R : Type u
S : Type v
inst✝¹ : NonAssocRing R
inst✝ : NonAssocRing S
f : R →+* S
s : Subring R
x : R
hx : x ∈ comap f (map f s)
⊢ x ∈ s ⊔ closure (⇑f ⁻¹' {0})
Module: Mathlib.Algebra.GroupWithZero.Action.Pointwise.Set

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝² : Zero α
inst✝¹ : Mul α
inst✝ : NoZeroDivisors α
s t : Set α
h : s * t = 0
⊢ s = 0 ∨ t = 0

Tactic:
by_contra! H
    have hst : (s * t).Nonempty := h.symm.subst zero_nonempty
    rw [Ne, ← hst.of_smul_left.subset_zero_iff, Ne, ← hst.of_smul_right.subset_zero_iff] at H
    simp only [not_subset, mem_zero] at H
    obtain ⟨⟨a, hs, ha⟩, b, ht, hb⟩ := H
    exact (eq_zero_or_eq_zero_of_mul_eq_zero <| h.subset <| mul_mem_mul hs ht).elim ha hb

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

Goal state before:
pp: R : Type uR
A₁ : Type uA₁
A₂ : Type uA₂
A₃ : Type uA₃
A₁' : Type uA₁'
A₂' : Type uA₂'
A₃' : Type uA₃'
inst✝¹² : CommSemiring R
inst✝¹¹ : Semiring A₁
inst✝¹⁰ : Semiring A₂
inst✝⁹ : Semiring A₃
inst✝⁸ : Semiring A₁'
inst✝⁷ : Semiring A₂'
inst✝⁶ : Semiring A₃'
inst✝⁵ : Algebra R A₁
inst✝⁴ : Algebra R A₂
inst✝³ : Algebra R A₃
inst✝² : Algebra R A₁'
inst✝¹ : Algebra R A₂'
inst✝ : Algebra R A₃'
e✝ e : A₁ ≃ₐ[R] A₂
e' : A₁' ≃ₐ[R] A₂'
ψ : A₂ ≃ₐ[R] A₂'
a✝ : A₂
⊢ e' (e'.symm (ψ (e (e.symm a✝)))) = ψ a✝

Tactic:
apply_symm_apply

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

Goal state before:
pp: R : Type u_1
R₂ : Type u_3
M : Type u_5
M₂ : Type u_7
inst✝⁵ : Semiring R
inst✝⁴ : Semiring R₂
inst✝³ : AddCommMonoid M
inst✝² : AddCommMonoid M₂
module_M : Module R M
module_M₂ : Module R₂ M₂
σ₁₂ : R →+* R₂
σ₂₁ : R₂ →+* R
f : M →ₛₗ[σ₁₂] M₂
inst✝¹ : RingHomInvPair σ₁₂ σ₂₁
inst✝ : RingHomInvPair σ₂₁ σ₁₂
h : Bijective ⇑f
x : M₂
⊢ (ofBijective f h) ((ofBijective f h).symm x) = x

Tactic:
apply_symm_apply

Goal state after:
R : Type u_1
R₂ : Type u_3
M : Type u_5
M₂ : Type u_7
inst✝⁵ : Semiring R
inst✝⁴ : Semiring R₂
inst✝³ : AddCommMonoid M
inst✝² : AddCommMonoid M₂
module_M : Module R M
module_M₂ : Module R₂ M₂
σ₁₂ : R →+* R₂
σ₂₁ : R₂ →+* R
f : M →ₛₗ[σ₁₂] M₂
inst✝¹ : RingHomInvPair σ₁₂ σ₂₁
inst✝ : RingHomInvPair σ₂₁ σ₁₂
h : Bijective ⇑f
x : M₂
⊢ x = x
Module: Mathlib.Data.Finset.Lattice.Prod

Goal state before:
pp: α : Type u_2
β : Type u_3
γ : Type u_4
inst✝¹ : SemilatticeSup α
inst✝ : OrderBot α
s : Finset β
t : Finset γ
f : β × γ → α
⊢ (s ×ˢ t).sup f = t.sup fun i' ↦ s.sup fun i ↦ f (i, i')

Tactic:
rw [sup_product_left, Finset.sup_comm]

Goal state after:
Module: Mathlib.Order.ModularLattice

Goal state before:
pp: α : Type u_1
inst✝¹ : Lattice α
inst✝ : IsModularLattice α
x y z a b : α
⊢ Icc a (b ⊔ a) = Icc a (a ⊔ b)

Tactic:
by rw [sup_comm]

Goal state after:
Module: Mathlib.Order.ModularLattice

Goal state before:
pp: α : Type u_1
inst✝¹ : Lattice α
inst✝ : IsModularLattice α
x y z a b : α
⊢ Ioo a (b ⊔ a) = Ioo a (a ⊔ b)

Tactic:
by rw [sup_comm]

Goal state after:
Module: Mathlib.Order.Atoms

Goal state before:
pp: α : Type u_2
inst✝ : PartialOrder α
a : α
b : ↑(Ici a)
⊢ (range ⇑(OrderEmbedding.subtype fun c ↦ a ≤ c)).OrdConnected

Tactic:
simpa only [OrderEmbedding.coe_subtype, Subtype.range_coe_subtype] using! Set.ordConnected_Ici

Goal state after:
Module: Mathlib.Order.Atoms

Goal state before:
pp: case mp
α : Type u_2
inst✝¹ : LE α
inst✝ : BoundedOrder α
i : IsSimpleOrder α
⊢ IsSimpleOrder αᵒᵈ

pp: case mpr
α : Type u_2
inst✝¹ : LE α
inst✝ : BoundedOrder α
i : IsSimpleOrder αᵒᵈ
⊢ IsSimpleOrder α

Tactic:
· exact
      { eq_bot_or_eq_top := fun a => Or.symm (eq_bot_or_eq_top (OrderDual.ofDual a) : _ ∨ _) }

Goal state after:
case mpr
α : Type u_2
inst✝¹ : LE α
inst✝ : BoundedOrder α
i : IsSimpleOrder αᵒᵈ
⊢ IsSimpleOrder α
Module: Mathlib.Order.Atoms

Goal state before:
pp: α : Type u_2
inst✝⁴ : Lattice α
inst✝³ : BoundedOrder α
inst✝² : IsModularLattice α
inst✝¹ : ComplementedLattice α
inst✝ : IsAtomic α
x y : α
xy : IsCompl x y
a : α
ha : IsAtom a
ay : a ≤ y
b : α
xb : b ∈ Set.Ici x
hb : IsCompl (⋯.IicOrderIsoIci ⟨a, ay⟩) ⟨b, xb⟩
⊢ IsAtom ⟨a, ay⟩

Tactic:
apply ha.Iic

Goal state after: