mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.SetTheory.Cardinal.Basic

Goal state before:
pp: 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}
⊢ #(Quotient.out (f none) × ((a : α) → Quotient.out (f (some a)))) = lift.{u, v} (∏ i, f i)

Tactic:
mk_prod,

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}
⊢ lift.{max u v, v} #(Quotient.out (f none)) * lift.{v, max u v} #((a : α) → Quotient.out (f (some a))) =
    lift.{u, v} (∏ i, f i)
Module: Mathlib.SetTheory.Cardinal.Basic

Goal state before:
pp: ι : Sort u_1
f : ι → Cardinal.{u_2}
⊢ ⨅ i, f i = 0 ↔ IsEmpty ι ∨ ∃ i, f i = 0

Tactic:
simp [iInf, sInf_eq_zero_iff]

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

Goal state before:
pp: f : Cardinal.{u} → Cardinal.{max u v}
s : Set Cardinal.{u}
hs : Small.{u, u + 1} ↑s
⊢ Small.{max u v, (max u v) + 1} ↑(f '' s)

Tactic:
exact small_lift _

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 < ℵ₀)
⊢ ℵ₀ ≤ a * b ↔ a ≠ 0 ∧ b ≠ 0 ∧ (ℵ₀ ≤ a ∨ ℵ₀ ≤ b)

Tactic:
not_and_or,

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 mpr
α : Type u
x : α
⊢ (∃! y, y ≠ x) → ∃ x y, x ≠ y ∧ {x, y} = univ

Tactic:
rintro ⟨y, hne, hy⟩
    exact ⟨x, y, hne.symm, eq_univ_of_forall fun z => or_iff_not_imp_left.2 (hy z)⟩

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

Goal state before:
pp: case 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.inl M N) = hM

Tactic:
ext m a; (conv_rhs => rw [← hN.one_smul 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 S✝
inst✝¹⁴ : AddCommMonoid M
inst✝¹³ : AddCommMonoid M₁
inst✝¹² : AddCommMonoid M₂
inst✝¹¹ : AddCommMonoid M₃
inst✝¹⁰ : Module R✝ M
inst✝⁹ : Module R✝ M₂
inst✝⁸ : Module S✝ M₃
σ : R✝ →+* S✝
fₗ✝ : M →ₗ[R✝] M₂
f g : M →ₛₗ[σ] M₃
R : Type u_14
S : Type u_15
inst✝⁷ : Semiring S
inst✝⁶ : SMul R M
inst✝⁵ : Module S M
inst✝⁴ : SMul R M₂
inst✝³ : Module S M₂
inst✝² : SMul R S
inst✝¹ : IsScalarTower R S M
inst✝ : IsScalarTower R S M₂
fₗ : M →ₗ[S] M₂
c : R
x : M
⊢ fₗ (c • x) = c • fₗ x

Tactic:
by rw [← smul_one_smul S c x, ← smul_one_smul S c (fₗ x), map_smul]

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

Goal state before:
pp: R : Type u_1
S : Type u_5
M : Type u_8
M₂ : Type u_10
inst✝⁵ : AddCommMonoid M
inst✝⁴ : AddCommMonoid M₂
inst✝³ : Semiring R
inst✝² : Module R M
inst✝¹ : Semiring S
inst✝ : Module S M₂
σ : R →+* S
f g : M →ₑ+[↑σ] M₂
h : ↑f = ↑g
⊢ f = g

Tactic:
ext m
  exact LinearMap.congr_fun h m

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

Goal state before:
pp: R₁ : Type u_2
R₂ : Type u_3
R₃ : Type u_4
M : Type u_8
M₂ : Type u_10
M₃ : Type u_11
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 σ₁₂ σ₂₃ σ₁₃
g : M₂ →ₛₗ[σ₂₃] M₃
c : M
⊢ (g ∘ₛₗ 0) c = 0 c

Tactic:
comp_apply,

Goal state after:
R₁ : Type u_2
R₂ : Type u_3
R₃ : Type u_4
M : Type u_8
M₂ : Type u_10
M₃ : Type u_11
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 σ₁₂ σ₂₃ σ₁₃
g : M₂ →ₛₗ[σ₂₃] M₃
c : M
⊢ g (0 c) = 0 c
Module: Mathlib.Algebra.Module.Equiv.Defs

Goal state before:
pp: R✝ : Type u_1
R₁ : Type u_2
R₂ : Type u_3
R₃ : Type u_4
R₄ : Type u_5
S✝ : Type u_6
M : 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
S : Type u_14
R : Type u_15
V : Type u_16
W : Type u_17
G : Type u_18
inst✝¹⁴ : Semiring R
inst✝¹³ : Semiring S
inst✝¹² : AddCommMonoid V
inst✝¹¹ : Module R V
inst✝¹⁰ : Module S V
inst✝⁹ : AddCommMonoid W
inst✝⁸ : Module R W
inst✝⁷ : Module S W
inst✝⁶ : AddCommMonoid G
inst✝⁵ : Module R G
inst✝⁴ : Module S G
inst✝³ : SMulCommClass R S W
inst✝² : SMul S R
inst✝¹ : IsScalarTower S R V
inst✝ : IsScalarTower S R W
α : Sˣ
e : V ≃ₗ[R] W
x✝ : V
⊢ (fun x ↦ ↑α⁻¹ • e.symm x) ((↑α • ↑e).toFun x✝) = x✝

Tactic:
simp [LinearMapClass.map_smul_of_tower e.symm, smul_smul]

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

Goal state before:
pp: M : Type u_2
N : Type u_3
φ : M → N
X : Type u_5
inst✝¹ : SMul M X
Y : Type u_6
inst✝ : SMul N Y
f : X →ₑ[φ] Y
x : X
⊢ ((MulActionHom.id N).comp f) x = f x

Tactic:
comp_apply,

Goal state after:
M : Type u_2
N : Type u_3
φ : M → N
X : Type u_5
inst✝¹ : SMul M X
Y : Type u_6
inst✝ : SMul N Y
f : X →ₑ[φ] Y
x : X
⊢ (MulActionHom.id N) (f x) = f x
Module: Mathlib.GroupTheory.GroupAction.Hom

Goal state before:
pp: M : Type u_2
N : Type u_3
φ : M → N
X : Type u_5
inst✝¹ : SMul M X
Y : Type u_6
inst✝ : SMul N Y
f : X →ₑ[φ] Y
x : X
⊢ (f.comp (MulActionHom.id M)) x = f x

Tactic:
comp_apply,

Goal state after:
M : Type u_2
N : Type u_3
φ : M → N
X : Type u_5
inst✝¹ : SMul M X
Y : Type u_6
inst✝ : SMul N Y
f : X →ₑ[φ] Y
x : X
⊢ f ((MulActionHom.id M) x) = f x
Module: Mathlib.GroupTheory.GroupAction.Hom

Goal state before:
pp: M : Type u_1
inst✝⁵ : Monoid M
N : Type u_2
inst✝⁴ : Monoid N
φ : M →* N
A : Type u_4
inst✝³ : Monoid A
inst✝² : MulDistribMulAction M A
B : Type u_5
inst✝¹ : Monoid B
inst✝ : MulDistribMulAction N B
f : A →ₑ*[φ] B
x : A
⊢ ((MulDistribMulActionHom.id N).comp f) x = f x

Tactic:
comp_apply,

Goal state after:
M : Type u_1
inst✝⁵ : Monoid M
N : Type u_2
inst✝⁴ : Monoid N
φ : M →* N
A : Type u_4
inst✝³ : Monoid A
inst✝² : MulDistribMulAction M A
B : Type u_5
inst✝¹ : Monoid B
inst✝ : MulDistribMulAction N B
f : A →ₑ*[φ] B
x : A
⊢ (MulDistribMulActionHom.id N) (f x) = f x
Module: Mathlib.GroupTheory.GroupAction.Hom

Goal state before:
pp: M : Type u_1
inst✝⁵ : Monoid M
N : Type u_2
inst✝⁴ : Monoid N
φ : M →* N
A : Type u_4
inst✝³ : Monoid A
inst✝² : MulDistribMulAction M A
B : Type u_5
inst✝¹ : Monoid B
inst✝ : MulDistribMulAction N B
f : A →ₑ*[φ] B
x : A
⊢ (f.comp (MulDistribMulActionHom.id M)) x = f x

Tactic:
comp_apply,

Goal state after:
M : Type u_1
inst✝⁵ : Monoid M
N : Type u_2
inst✝⁴ : Monoid N
φ : M →* N
A : Type u_4
inst✝³ : Monoid A
inst✝² : MulDistribMulAction M A
B : Type u_5
inst✝¹ : Monoid B
inst✝ : MulDistribMulAction N B
f : A →ₑ*[φ] B
x : A
⊢ f ((MulDistribMulActionHom.id M) x) = f x
Module: Mathlib.GroupTheory.GroupAction.Hom

Goal state before:
pp: M : Type u_1
inst✝⁵ : Monoid M
N : Type u_2
inst✝⁴ : Monoid N
φ : M →* N
R : Type u_10
inst✝³ : Semiring R
inst✝² : MulSemiringAction M R
S : Type u_12
inst✝¹ : Semiring S
inst✝ : MulSemiringAction N S
f : R →ₑ+*[φ] S
x : R
⊢ ((MulSemiringActionHom.id N).comp f) x = f x

Tactic:
comp_apply,

Goal state after:
M : Type u_1
inst✝⁵ : Monoid M
N : Type u_2
inst✝⁴ : Monoid N
φ : M →* N
R : Type u_10
inst✝³ : Semiring R
inst✝² : MulSemiringAction M R
S : Type u_12
inst✝¹ : Semiring S
inst✝ : MulSemiringAction N S
f : R →ₑ+*[φ] S
x : R
⊢ (MulSemiringActionHom.id N) (f x) = f x
Module: Mathlib.GroupTheory.GroupAction.Hom

Goal state before:
pp: M : Type u_1
inst✝⁵ : Monoid M
N : Type u_2
inst✝⁴ : Monoid N
φ : M →* N
R : Type u_10
inst✝³ : Semiring R
inst✝² : MulSemiringAction M R
S : Type u_12
inst✝¹ : Semiring S
inst✝ : MulSemiringAction N S
f : R →ₑ+*[φ] S
x : R
⊢ (f.comp (MulSemiringActionHom.id M)) x = f x

Tactic:
comp_apply,

Goal state after:
M : Type u_1
inst✝⁵ : Monoid M
N : Type u_2
inst✝⁴ : Monoid N
φ : M →* N
R : Type u_10
inst✝³ : Semiring R
inst✝² : MulSemiringAction M R
S : Type u_12
inst✝¹ : Semiring S
inst✝ : MulSemiringAction N S
f : R →ₑ+*[φ] S
x : R
⊢ f ((MulSemiringActionHom.id M) x) = f x
Module: Mathlib.Algebra.Module.Torsion.Free

Goal state before:
pp: R : Type u_1
M : Type u_3
inst✝³ : Semiring R
inst✝² : AddCommMonoid M
inst✝¹ : Module R M
r : R
m : M
inst✝ : IsTorsionFree R M
hr : IsRegular r
⊢ r • m = 0 ↔ m = 0

Tactic:
rw [← hr.smul_right_inj (m₁ := m), smul_zero]

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

Goal state before:
pp: case succ
R : Type u_1
R₂ : Type u_2
M : Type u_4
M₂ : Type u_6
inst✝⁵ : Semiring R
inst✝⁴ : AddCommMonoid M
inst✝³ : Module R M
inst✝² : Semiring R₂
inst✝¹ : AddCommMonoid M₂
inst✝ : Module R₂ M₂
σ₁₂ : R →+* R₂
f : M →ₛₗ[σ₁₂] M₂
g : End R M
g₂ : End R₂ M₂
h : g₂ ∘ₛₗ f = f ∘ₛₗ g
k : ℕ
ih : (g₂ ^ k) ∘ₛₗ f = f ∘ₛₗ (g ^ k)
⊢ f ∘ₛₗ (g ∘ₗ g ^ k) = f ∘ₛₗ (g * g ^ k)

Tactic:
mul_eq_comp

Goal state after:
case succ
R : Type u_1
R₂ : Type u_2
M : Type u_4
M₂ : Type u_6
inst✝⁵ : Semiring R
inst✝⁴ : AddCommMonoid M
inst✝³ : Module R M
inst✝² : Semiring R₂
inst✝¹ : AddCommMonoid M₂
inst✝ : Module R₂ M₂
σ₁₂ : R →+* R₂
f : M →ₛₗ[σ₁₂] M₂
g : End R M
g₂ : End R₂ M₂
h : g₂ ∘ₛₗ f = f ∘ₛₗ g
k : ℕ
ih : (g₂ ^ k) ∘ₛₗ f = f ∘ₛₗ (g ^ k)
⊢ f ∘ₛₗ (g ∘ₗ g ^ k) = f ∘ₛₗ (g ∘ₗ g ^ k)
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
n : ℕ
⊢ f' ^ n * f' = (f' ^ n) ∘ₗ f'

Tactic:
mul_eq_comp

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
n : ℕ
⊢ (f' ^ n) ∘ₗ f' = (f' ^ n) ∘ₗ f'
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
n : ℕ
⊢ f' * f' ^ n = f' ∘ₗ f' ^ n

Tactic:
mul_eq_comp

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
n : ℕ
⊢ f' ∘ₗ f' ^ n = f' ∘ₗ f' ^ n
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
n : ℕ
⊢ f' ^ (n + 1) = f' ∘ₗ f' ^ n

Tactic:
by rw [pow_succ', mul_eq_comp]

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

Goal state before:
pp: G : Type u''
S : Type u'
R : Type u
M : Type v
ι : Type w
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
C : Set M
nonempty : C.Nonempty
linearComb : ∀ x ∈ C, ∀ y ∈ C, ∀ (a b : R), a • x + b • y ∈ C
c : R
x : M
hx : x ∈ C
⊢ c • x ∈ C

Tactic:
simpa using linearComb x hx x hx c 0

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

Goal state before:
pp: G : Type u''
S : Type u'
R : Type u
M : Type v
ι : Type w
inst✝⁵ : Semiring R
inst✝⁴ : AddCommMonoid M
module_M : Module R M
p q : Submodule R M
r : R
x✝ y : M
inst✝³ : Semiring S
inst✝² : SMul S R
inst✝¹ : Module S M
inst✝ : IsScalarTower S R M
a b : S
x : ↥p
⊢ (a + b) • x = a • x + b • x

Tactic:
by ext; simp [add_smul]

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

Goal state before:
pp: G : Type u''
S : Type u'
R : Type u
M : Type v
ι : Type w
T : Type u_1
inst✝⁹ : Semiring R
inst✝⁸ : AddCommMonoid M
inst✝⁷ : Semiring S
inst✝⁶ : Module R M
inst✝⁵ : SMul S R
inst✝⁴ : Module S M
inst✝³ : IsScalarTower S R M
inst✝² : SetLike T M
inst✝¹ : AddSubmonoidClass T M
inst✝ : SMulMemClass T R M
t : T
x✝² x✝¹ : S
x✝ : ↥t
⊢ (x✝² + x✝¹) • x✝ = x✝² • x✝ + x✝¹ • x✝

Tactic:
by ext; simp [add_smul]

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

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₂
inst✝³ : Module R M
inst✝² : Module R₂ M₂
σ₁₂ : R →+* R₂
f : M →ₛₗ[σ₁₂] M₂
M₂' : Type u_10
inst✝¹ : AddCommMonoid M₂'
inst✝ : Module R₂ M₂'
p : M₂' →ₗ[R₂] M₂
hp : Injective ⇑p
h : ∀ (c : M), f c ∈ range ⇑p
x : M
⊢ (p ∘ₛₗ f.codLift p hp h) x = f x

Tactic:
comp_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₂
inst✝³ : Module R M
inst✝² : Module R₂ M₂
σ₁₂ : R →+* R₂
f : M →ₛₗ[σ₁₂] M₂
M₂' : Type u_10
inst✝¹ : AddCommMonoid M₂'
inst✝ : Module R₂ M₂'
p : M₂' →ₗ[R₂] M₂
hp : Injective ⇑p
h : ∀ (c : M), f c ∈ range ⇑p
x : M
⊢ p ((f.codLift p hp h) x) = f x
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✝³ : SupSet α
inst✝² : SupSet β
inst✝¹ : SupSet γ
inst✝ : SupSet δ
f : sSupHom β γ
g : sSupHom α β
s : Set α
⊢ (⇑f ∘ ⇑g) (sSup s) = sSup (⇑f ∘ ⇑g '' s)

Tactic:
comp_apply,

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✝³ : SupSet α
inst✝² : SupSet β
inst✝¹ : SupSet γ
inst✝ : SupSet δ
f : sSupHom β γ
g : sSupHom α β
s : Set α
⊢ f (g (sSup s)) = sSup (⇑f ∘ ⇑g '' s)
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₂
τ₂₁ : R₂ →+* R
inst✝ : RingHomInvPair τ₁₂ τ₂₁
f : M →ₛₗ[τ₁₂] M₂
g : M₂ →ₛₗ[τ₂₁] M
h : g ∘ₛₗ f = id
m : M
hm : f m = 0
⊢ (g ∘ₛₗ f) m = 0

Tactic:
comp_apply,

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₂
τ₂₁ : R₂ →+* R
inst✝ : RingHomInvPair τ₁₂ τ₂₁
f : M →ₛₗ[τ₁₂] M₂
g : M₂ →ₛₗ[τ₂₁] M
h : g ∘ₛₗ f = id
m : M
hm : f m = 0
⊢ g (f m) = 0
Module: Mathlib.Algebra.Ring.CharZero

Goal state before:
pp: α : Type u_1
R : Type u_2
S : Type u_3
n : ℕ
inst✝¹ : AddMonoidWithOne R
inst✝ : CharZero R
⊢ ↑2 ≠ 0

Tactic:
Nat.cast_ne_zero

Goal state after:
α : Type u_1
R : Type u_2
S : Type u_3
n : ℕ
inst✝¹ : AddMonoidWithOne R
inst✝ : CharZero R
⊢ 2 ≠ 0
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
⊢ comap (a • f) p = ⨅ (_ : a ≠ 0), comap f p

Tactic:
by_cases h : a = 0

Goal state after:
case pos
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
⊢ comap (a • f) p = ⨅ (_ : a ≠ 0), comap f p

case neg
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
⊢ comap (a • f) p = ⨅ (_ : a ≠ 0), comap f p
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
⊢ map (a • f) p = ⨆ (_ : a ≠ 0), map f p

Tactic:
by_cases h : a = 0

Goal state after:
case pos
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 (a • f) p = ⨆ (_ : a ≠ 0), map f p

case neg
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 (a • f) p = ⨆ (_ : a ≠ 0), map f p
Module: Mathlib.RingTheory.NonUnitalSubsemiring.Basic

Goal state before:
pp: R : Type u
inst✝ : NonUnitalNonAssocSemiring R
s : Set R
x : R
hx : x ∈ closure ↑(AddSubmonoid.closure s)
H : NonUnitalSubsemiring R
J : H ∈ {S | s ⊆ ↑S}
y : R
hy : y ∈ ↑(Subsemigroup.closure ↑(AddSubmonoid.closure s))
z : R
hz : z ∈ ↑(AddSubmonoid.closure s)
⊢ z ∈ ↑H.toSubsemigroup

Tactic:
exact (AddSubmonoid.mem_closure.mp hz) H.toAddSubmonoid fun w hw => J hw

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

Goal state before:
pp: R : Type u
inst✝ : NonAssocSemiring R
s : Set R
x : R
hx : x ∈ closure ↑(AddSubmonoid.closure s)
H : Subsemiring R
J : H ∈ {S | s ⊆ ↑S}
y : R
hy : y ∈ ↑(Submonoid.closure ↑(AddSubmonoid.closure s))
z : R
hz : z ∈ ↑(AddSubmonoid.closure s)
⊢ z ∈ ↑H.toSubmonoid

Tactic:
exact (AddSubmonoid.mem_closure.mp hz) H.toAddSubmonoid fun w hw => J hw

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

Goal state before:
pp: case succ.inl
M : Type u_1
inst✝ : CommMonoidWithZero M
p : M
hp : Prime p
a : M
n : ℕ
ih : p ∣ a ^ n → p ∣ a
h : p ∣ a * a ^ n
dvd_a : p ∣ a
⊢ p ∣ a

pp: case succ.inr
M : Type u_1
inst✝ : CommMonoidWithZero M
p : M
hp : Prime p
a : M
n : ℕ
ih : p ∣ a ^ n → p ∣ a
h : p ∣ a * a ^ n
dvd_pow : p ∣ a ^ n
⊢ p ∣ a

Tactic:
· assumption

Goal state after:
case succ.inr
M : Type u_1
inst✝ : CommMonoidWithZero M
p : M
hp : Prime p
a : M
n : ℕ
ih : p ∣ a ^ n → p ∣ a
h : p ∣ a * a ^ n
dvd_pow : p ∣ a ^ n
⊢ p ∣ a
Module: Mathlib.Algebra.Group.Irreducible.Lemmas

Goal state before:
pp: M : Type u_2
inst✝ : Monoid M
x : M
n : ℕ
x✝ : n + 2 ≠ 1
⊢ ¬Irreducible (x ^ (n + 2))

Tactic:
by
    intro ⟨h₁, h₂⟩
    have := h₂ (pow_succ _ _)
    rw [isUnit_pow_iff n.succ_ne_zero, or_self] at this
    exact h₁ (this.pow _)

Goal state after:
Module: Mathlib.Algebra.Group.Irreducible.Lemmas

Goal state before:
pp: F : Type u_1
M : Type u_2
N : Type u_3
inst✝³ : Monoid M
inst✝² : Monoid N
x : M
inst✝¹ : EquivLike F M N
inst✝ : MulEquivClass F M N
f : F
⊢ Irreducible (f x) ↔ Irreducible x

Tactic:
simp [_root_.irreducible_iff, (EquivLike.surjective f).forall, ← map_mul, -isUnit_map_iff]

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

Goal state before:
pp: M : Type u_1
inst✝¹ : CommMonoidWithZero M
inst✝ : IsCancelMulZero M
p a b : M
n : ℕ
hp : Prime p
hpow : p ^ n.succ ∣ a ^ n.succ * b ^ n
hb : ¬p ^ 2 ∣ b
⊢ p ∣ a

Tactic:
rcases hp.dvd_or_dvd ((dvd_pow_self p (Nat.succ_ne_zero n)).trans hpow) with H | hbdiv

Goal state after:
case inl
M : Type u_1
inst✝¹ : CommMonoidWithZero M
inst✝ : IsCancelMulZero M
p a b : M
n : ℕ
hp : Prime p
hpow : p ^ n.succ ∣ a ^ n.succ * b ^ n
hb : ¬p ^ 2 ∣ b
H : p ∣ a ^ n.succ
⊢ p ∣ a

case inr
M : Type u_1
inst✝¹ : CommMonoidWithZero M
inst✝ : IsCancelMulZero M
p a b : M
n : ℕ
hp : Prime p
hpow : p ^ n.succ ∣ a ^ n.succ * b ^ n
hb : ¬p ^ 2 ∣ b
hbdiv : p ∣ b ^ n
⊢ p ∣ a
Module: Mathlib.Algebra.Ring.Subring.Basic

Goal state before:
pp: R : Type u_1
inst✝ : Ring R
s : Set R
C : R → Prop
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)
h0 : C 0
hd : List R
HL : ∀ y ∈ hd, y ∈ s ∨ y = -1
⊢ ∃ L, (∀ x ∈ L, x ∈ s) ∧ (hd.prod = L.prod ∨ hd.prod = -L.prod)

Tactic:
induction hd with

Goal state after:
case cons
R : Type u_1
inst✝ : Ring R
s : Set R
C : R → Prop
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)
h0 : C 0
hd : R
tl : List R
ih : (∀ y ∈ tl, y ∈ s ∨ y = -1) → ∃ L, (∀ x ∈ L, x ∈ s) ∧ (tl.prod = L.prod ∨ tl.prod = -L.prod)
HL : ∀ y ∈ hd :: tl, y ∈ s ∨ y = -1
⊢ ∃ L, (∀ x ∈ L, x ∈ s) ∧ ((hd :: tl).prod = L.prod ∨ (hd :: tl).prod = -L.prod)
Module: Mathlib.Algebra.GroupWithZero.NonZeroDivisors

Goal state before:
pp: case mp.mk.refine_1
M₀ : Type u_1
inst✝ : CommMonoidWithZero M₀
a : M₀
w✝ : Associates M₀
x : M₀
hx₁ : Quot.mk (⇑(Associated.setoid M₀)) x * Associates.mk a = 0
hx₂ : Quot.mk (⇑(Associated.setoid M₀)) x ≠ 0
⊢ Associates.mk (x * a) = 0

Tactic:
← Associates.mk_mul_mk,

Goal state after:
case mp.mk.refine_1
M₀ : Type u_1
inst✝ : CommMonoidWithZero M₀
a : M₀
w✝ : Associates M₀
x : M₀
hx₁ : Quot.mk (⇑(Associated.setoid M₀)) x * Associates.mk a = 0
hx₂ : Quot.mk (⇑(Associated.setoid M₀)) x ≠ 0
⊢ Associates.mk x * Associates.mk a = 0
Module: Mathlib.Algebra.Module.Submodule.Range

Goal state before:
pp: case mpr
R : Type u_1
R₂ : Type u_2
M : Type u_5
M₂ : Type u_6
inst✝⁶ : Ring R
inst✝⁵ : Ring R₂
inst✝⁴ : AddCommGroup M
inst✝³ : AddCommGroup M₂
inst✝² : Module R M
inst✝¹ : Module R₂ M₂
τ₁₂ : R →+* R₂
f : M →ₛₗ[τ₁₂] M₂
inst✝ : RingHomSurjective τ₁₂
p : Submodule R M
y : M₂
h₁ : y ∈ Set.range ⇑f
h₂ : ⇑f ⁻¹' {y} ⊆ ↑p
z : M
hz : f z = 0
⊢ z ∈ p

Tactic:
Set.mem_range

Goal state after:
case mpr
R : Type u_1
R₂ : Type u_2
M : Type u_5
M₂ : Type u_6
inst✝⁶ : Ring R
inst✝⁵ : Ring R₂
inst✝⁴ : AddCommGroup M
inst✝³ : AddCommGroup M₂
inst✝² : Module R M
inst✝¹ : Module R₂ M₂
τ₁₂ : R →+* R₂
f : M →ₛₗ[τ₁₂] M₂
inst✝ : RingHomSurjective τ₁₂
p : Submodule R M
y : M₂
h₁ : ∃ y_1, f y_1 = y
h₂ : ⇑f ⁻¹' {y} ⊆ ↑p
z : M
hz : f z = 0
⊢ z ∈ p
Module: Mathlib.Order.Atoms

Goal state before:
pp: α : Type u_4
inst✝¹ : Preorder α
inst✝ : IsStronglyAtomic α
s : Set α
h : s.OrdConnected
c : α
hc : c ∈ s
d : α
hd : d ∈ s
hcd : ⟨c, hc⟩ < ⟨d, hd⟩
x : α
hcx : c ⋖ x
hxd : x ≤ d
y : ↑s
hy : ⟨c, hc⟩ < y
hy' : y < ⟨x, ⋯⟩
⊢ ↑y < x

Tactic:
simpa using! hy'

Goal state after:
Module: Mathlib.Order.Atoms

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

Tactic:
by
  constructor <;> intro i
  · exact
      { eq_bot_or_eq_top := fun a => Or.symm (eq_bot_or_eq_top (OrderDual.ofDual a) : _ ∨ _) }
  · exact
      { exists_pair_ne := @exists_pair_ne αᵒᵈ _
        eq_bot_or_eq_top := fun a => Or.symm (eq_bot_or_eq_top (OrderDual.toDual a)) }

Goal state after:
Module: Mathlib.Order.Atoms

Goal state before:
pp: α : Type u_2
inst✝³ : Lattice α
inst✝² : OrderBot α
inst✝¹ : IsUpperModularLattice α
inst✝ : IsAtomistic α
a b : α
hab : a < b
⊢ ∃ x, a ⋖ x ∧ x ≤ b

Tactic:
obtain ⟨s, hsb, h⟩ := isLUB_atoms b

Goal state after:
α : Type u_2
inst✝³ : Lattice α
inst✝² : OrderBot α
inst✝¹ : IsUpperModularLattice α
inst✝ : IsAtomistic α
a b : α
hab : a < b
s : Set α
hsb : IsLUB s b
h : ∀ a ∈ s, IsAtom a
⊢ ∃ x, a ⋖ x ∧ x ≤ b
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 (⋯.IicOrderIsoIci ⟨a, ay⟩)

Tactic:
OrderIso.isAtom_iff

Goal state after:
α : 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⟩
Module: Mathlib.Algebra.BigOperators.GroupWithZero.Finset

Goal state before:
pp: ι : Type u_1
M₀ : Type u_4
inst✝² : Fintype ι
inst✝¹ : CommMonoidWithZero M₀
p : ι → Prop
inst✝ : DecidablePred p
⊢ (∏ i, if p i then 1 else 0) = if ∀ (i : ι), p i then 1 else 0

Tactic:
by simp [Finset.prod_boole]

Goal state after:
Module: Mathlib.LinearAlgebra.Span.Basic

Goal state before:
pp: case mpr
R : Type u_1
M : Type u_4
inst✝⁴ : Semiring R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
N : Type u_8
inst✝¹ : AddCommMonoid N
inst✝ : Module R N
S : Set M
f g : ↥(span R S) →ₗ[R] N
h : ∀ (s : ↑S), f ⟨↑s, ⋯⟩ = g ⟨↑s, ⋯⟩
⊢ f = g

Tactic:
suffices ∀ (x : M) (hx : x ∈ span R S), f ⟨x, hx⟩ = g ⟨x, hx⟩ by
      ext ⟨x, hx⟩
      exact this x hx

Goal state after:
case mpr
R : Type u_1
M : Type u_4
inst✝⁴ : Semiring R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
N : Type u_8
inst✝¹ : AddCommMonoid N
inst✝ : Module R N
S : Set M
f g : ↥(span R S) →ₗ[R] N
h : ∀ (s : ↑S), f ⟨↑s, ⋯⟩ = g ⟨↑s, ⋯⟩
⊢ ∀ (x : M) (hx : x ∈ span R S), f ⟨x, hx⟩ = g ⟨x, hx⟩