mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Algebra.MonoidAlgebra.Support

Goal state before:
pp: k : Type u₁
G : Type u₂
inst✝² : Semiring k
inst✝¹ : Mul G
inst✝ : DecidableEq G
f : k[G]
r : k
hr : ∀ (y : k), y * r = 0 ↔ y = 0
x : G
rx : IsRightRegular x
⊢ (f * single x r).coeff.support = image (fun x_1 ↦ x_1 * x) f.coeff.support

Tactic:
refine subset_antisymm (support_coeff_mul_single_subset f _ _) fun y hy => ?_

Goal state after:
k : Type u₁
G : Type u₂
inst✝² : Semiring k
inst✝¹ : Mul G
inst✝ : DecidableEq G
f : k[G]
r : k
hr : ∀ (y : k), y * r = 0 ↔ y = 0
x : G
rx : IsRightRegular x
y : G
hy : y ∈ image (fun x_1 ↦ x_1 * x) f.coeff.support
⊢ y ∈ (f * single x r).coeff.support
Module: Mathlib.LinearAlgebra.LinearPMap

Goal state before:
pp: case h
R : Type u_1
S : Type u_2
inst✝⁵ : Ring R
inst✝⁴ : Ring S
σ : R →+* S
E : Type u_4
inst✝³ : AddCommGroup E
inst✝² : Module R E
F : Type u_5
inst✝¹ : AddCommGroup F
inst✝ : Module S F
c : Set (E →ₛₗ.[σ] F)
hc : DirectedOn (fun x1 x2 ↦ x1 ≤ x2) c
cne : c.Nonempty
hdir : DirectedOn (fun x1 x2 ↦ x1 ≤ x2) (domain '' c)
P : (x : ↥(sSup (domain '' c))) → { p // ↑x ∈ (↑p).domain }
f : ↥(sSup (domain '' c)) → F := fun x ↦ ↑↑↑(P x) ⟨↑x, ⋯⟩
f_eq : ∀ (p : ↑c) (x : ↥(sSup (domain '' c))) (y : ↥(↑p).domain), ↑x = ↑y → f x = ↑↑p y
⊢ { domain := sSup (domain '' c), toFun := { toFun := f, map_add' := ⋯, map_smul' := ⋯ } } ∈ upperBounds c

Tactic:
·

Goal state after:
case h
R : Type u_1
S : Type u_2
inst✝⁵ : Ring R
inst✝⁴ : Ring S
σ : R →+* S
E : Type u_4
inst✝³ : AddCommGroup E
inst✝² : Module R E
F : Type u_5
inst✝¹ : AddCommGroup F
inst✝ : Module S F
c : Set (E →ₛₗ.[σ] F)
hc : DirectedOn (fun x1 x2 ↦ x1 ≤ x2) c
cne : c.Nonempty
hdir : DirectedOn (fun x1 x2 ↦ x1 ≤ x2) (domain '' c)
P : (x : ↥(sSup (domain '' c))) → { p // ↑x ∈ (↑p).domain }
f : ↥(sSup (domain '' c)) → F := fun x ↦ ↑↑↑(P x) ⟨↑x, ⋯⟩
f_eq : ∀ (p : ↑c) (x : ↥(sSup (domain '' c))) (y : ↥(↑p).domain), ↑x = ↑y → f x = ↑↑p y
⊢ { domain := sSup (domain '' c), toFun := { toFun := f, map_add' := ⋯, map_smul' := ⋯ } } ∈ upperBounds c
Module: Mathlib.Algebra.Polynomial.Eval.Defs

Goal state before:
pp: R : Type u
a : R
inst✝ : CommSemiring R
p q : R[X]
H : q.IsRoot a
⊢ (p * q).IsRoot a

Tactic:
rw [IsRoot, eval_mul, IsRoot.def.1 H, mul_zero]

Goal state after:
Module: Mathlib.Data.Nat.Prime.Defs

Goal state before:
pp: case zero
p : ℕ
p2 : 2 ≤ p
h : 2 ≤ 0 → 0 < p → ¬0 ∣ p
l : 0 < p
d : 0 ∣ p
⊢ 0 = 1

pp: case succ.zero
p : ℕ
p2 : 2 ≤ p
h : 2 ≤ 0 + 1 → 0 + 1 < p → ¬0 + 1 ∣ p
l : 0 + 1 < p
d : 0 + 1 ∣ p
⊢ 0 + 1 = 1

pp: case succ.succ
p : ℕ
p2 : 2 ≤ p
m : ℕ
h : 2 ≤ m + 1 + 1 → m + 1 + 1 < p → ¬m + 1 + 1 ∣ p
l : m + 1 + 1 < p
d : m + 1 + 1 ∣ p
⊢ m + 1 + 1 = 1

Tactic:
·

Goal state after:
case zero
p : ℕ
p2 : 2 ≤ p
h : 2 ≤ 0 → 0 < p → ¬0 ∣ p
l : 0 < p
d : 0 ∣ p
⊢ 0 = 1
Module: Mathlib.Data.Nat.Prime.Defs

Goal state before:
pp: case succ.zero
p : ℕ
p2 : 2 ≤ p
h : 2 ≤ 0 + 1 → 0 + 1 < p → ¬0 + 1 ∣ p
l : 0 + 1 < p
d : 0 + 1 ∣ p
⊢ 0 + 1 = 1

pp: case succ.succ
p : ℕ
p2 : 2 ≤ p
m : ℕ
h : 2 ≤ m + 1 + 1 → m + 1 + 1 < p → ¬m + 1 + 1 ∣ p
l : m + 1 + 1 < p
d : m + 1 + 1 ∣ p
⊢ m + 1 + 1 = 1

Tactic:
·

Goal state after:
case succ.zero
p : ℕ
p2 : 2 ≤ p
h : 2 ≤ 0 + 1 → 0 + 1 < p → ¬0 + 1 ∣ p
l : 0 + 1 < p
d : 0 + 1 ∣ p
⊢ 0 + 1 = 1
Module: Mathlib.Data.Nat.Prime.Defs

Goal state before:
pp: case succ.succ
p : ℕ
p2 : 2 ≤ p
m : ℕ
h : 2 ≤ m + 1 + 1 → m + 1 + 1 < p → ¬m + 1 + 1 ∣ p
l : m + 1 + 1 < p
d : m + 1 + 1 ∣ p
⊢ m + 1 + 1 = 1

Tactic:
·

Goal state after:
case succ.succ
p : ℕ
p2 : 2 ≤ p
m : ℕ
h : 2 ≤ m + 1 + 1 → m + 1 + 1 < p → ¬m + 1 + 1 ∣ p
l : m + 1 + 1 < p
d : m + 1 + 1 ∣ p
⊢ m + 1 + 1 = 1
Module: Mathlib.Data.Nat.Prime.Defs

Goal state before:
pp: case inl
p : ℕ
p2 : 2 ≤ p
a : ∀ (m : ℕ), 2 ≤ m → m ≤ p.sqrt → ¬m ∣ p
m : ℕ
m2 : 2 ≤ m
l : m < p
x✝ mdvd : m ∣ p
k : ℕ
e : p = m * k
h✝ : mdvd = ⋯
hm : m ≤ p.sqrt
⊢ False

pp: case inr
p : ℕ
p2 : 2 ≤ p
a : ∀ (m : ℕ), 2 ≤ m → m ≤ p.sqrt → ¬m ∣ p
m : ℕ
m2 : 2 ≤ m
l : m < p
x✝ mdvd : m ∣ p
k : ℕ
e : p = m * k
h✝ : mdvd = ⋯
hk : k ≤ p.sqrt
⊢ False

Tactic:
·

Goal state after:
case inl
p : ℕ
p2 : 2 ≤ p
a : ∀ (m : ℕ), 2 ≤ m → m ≤ p.sqrt → ¬m ∣ p
m : ℕ
m2 : 2 ≤ m
l : m < p
x✝ mdvd : m ∣ p
k : ℕ
e : p = m * k
h✝ : mdvd = ⋯
hm : m ≤ p.sqrt
⊢ False
Module: Mathlib.Data.Nat.Prime.Defs

Goal state before:
pp: case inr
p : ℕ
p2 : 2 ≤ p
a : ∀ (m : ℕ), 2 ≤ m → m ≤ p.sqrt → ¬m ∣ p
m : ℕ
m2 : 2 ≤ m
l : m < p
x✝ mdvd : m ∣ p
k : ℕ
e : p = m * k
h✝ : mdvd = ⋯
hk : k ≤ p.sqrt
⊢ False

Tactic:
·

Goal state after:
case inr
p : ℕ
p2 : 2 ≤ p
a : ∀ (m : ℕ), 2 ≤ m → m ≤ p.sqrt → ¬m ∣ p
m : ℕ
m2 : 2 ≤ m
l : m < p
x✝ mdvd : m ∣ p
k : ℕ
e : p = m * k
h✝ : mdvd = ⋯
hk : k ≤ p.sqrt
⊢ False
Module: Mathlib.Data.Nat.Prime.Defs

Goal state before:
pp: p : ℕ
hp✝ : 2 ≤ p
m : ℕ
h : m < p
n : ℕ
hp : p = m * n
hpn : p ≤ n
this : m ≠ 0 ∧ n ≠ 0
⊢ n ≠ 0

Tactic:
by lia

Goal state after:
Module: Mathlib.Data.Nat.Prime.Defs

Goal state before:
pp: p : ℕ
hp✝ : 2 ≤ p
m : ℕ
h : m < p
n : ℕ
hp : p = m * n
hpn : p ≤ n
this : m ≠ 0 ∧ n ≠ 0
⊢ 0 < m

Tactic:
by lia

Goal state after:
Module: Mathlib.Data.Nat.Prime.Defs

Goal state before:
pp: case pos
n : ℕ
n2 : 2 ≤ n
x✝ : ℕ
k : ℕ := x✝
i : ℕ
e : x✝ = 2 * i + 3
a : ∀ (m : ℕ), 2 ≤ m → m ∣ n → x✝ ≤ m
h : n < k * k
⊢ n.minFacProp (if n < x✝ * x✝ then n else if x✝ ∣ n then x✝ else n.minFacAux (x✝ + 2))

pp: case neg
n : ℕ
n2 : 2 ≤ n
x✝ : ℕ
k : ℕ := x✝
i : ℕ
e : x✝ = 2 * i + 3
a : ∀ (m : ℕ), 2 ≤ m → m ∣ n → x✝ ≤ m
h : ¬n < k * k
⊢ n.minFacProp (if n < x✝ * x✝ then n else if x✝ ∣ n then x✝ else n.minFacAux (x✝ + 2))

Tactic:
·

Goal state after:
case pos
n : ℕ
n2 : 2 ≤ n
x✝ : ℕ
k : ℕ := x✝
i : ℕ
e : x✝ = 2 * i + 3
a : ∀ (m : ℕ), 2 ≤ m → m ∣ n → x✝ ≤ m
h : n < k * k
⊢ n.minFacProp (if n < x✝ * x✝ then n else if x✝ ∣ n then x✝ else n.minFacAux (x✝ + 2))
Module: Mathlib.Data.Nat.Prime.Defs

Goal state before:
pp: case pos
n : ℕ
n2 : 2 ≤ n
x✝ : ℕ
k : ℕ := x✝
i : ℕ
e : x✝ = 2 * i + 3
a : ∀ (m : ℕ), 2 ≤ m → m ∣ n → x✝ ≤ m
h : ¬n < k * k
k2 : 2 ≤ k
dk : k ∣ n
⊢ n.minFacProp x✝

pp: case neg
n : ℕ
n2 : 2 ≤ n
x✝ : ℕ
k : ℕ := x✝
i : ℕ
e : x✝ = 2 * i + 3
a : ∀ (m : ℕ), 2 ≤ m → m ∣ n → x✝ ≤ m
h : ¬n < k * k
k2 : 2 ≤ k
dk : ¬k ∣ n
⊢ n.minFacProp (n.minFacAux (x✝ + 2))

Tactic:
·

Goal state after:
case pos
n : ℕ
n2 : 2 ≤ n
x✝ : ℕ
k : ℕ := x✝
i : ℕ
e : x✝ = 2 * i + 3
a : ∀ (m : ℕ), 2 ≤ m → m ∣ n → x✝ ≤ m
h : ¬n < k * k
k2 : 2 ≤ k
dk : k ∣ n
⊢ n.minFacProp x✝
Module: Mathlib.Data.Nat.Prime.Defs

Goal state before:
pp: case neg
n : ℕ
n2 : 2 ≤ n
x✝ : ℕ
k : ℕ := x✝
i : ℕ
e : x✝ = 2 * i + 3
a : ∀ (m : ℕ), 2 ≤ m → m ∣ n → x✝ ≤ m
h : ¬n < k * k
k2 : 2 ≤ k
dk : ¬k ∣ n
⊢ n.minFacProp (n.minFacAux (x✝ + 2))

Tactic:
·

Goal state after:
case neg
n : ℕ
n2 : 2 ≤ n
x✝ : ℕ
k : ℕ := x✝
i : ℕ
e : x✝ = 2 * i + 3
a : ∀ (m : ℕ), 2 ≤ m → m ∣ n → x✝ ≤ m
h : ¬n < k * k
k2 : 2 ≤ k
dk : ¬k ∣ n
⊢ n.minFacProp (n.minFacAux (x✝ + 2))
Module: Mathlib.LinearAlgebra.LinearPMap

Goal state before:
pp: case mp
R : Type u_1
inst✝⁴ : Ring R
E : Type u_4
inst✝³ : AddCommGroup E
inst✝² : Module R E
F : Type u_5
inst✝¹ : AddCommGroup F
inst✝ : Module R F
f : E →ₗ.[R] F
x : E
h : ∃ x_1, ∃ (h : x ∈ f.domain), ↑f ⟨x, ⋯⟩ = x_1
⊢ x ∈ f.domain

pp: case mpr
R : Type u_1
inst✝⁴ : Ring R
E : Type u_4
inst✝³ : AddCommGroup E
inst✝² : Module R E
F : Type u_5
inst✝¹ : AddCommGroup F
inst✝ : Module R F
f : E →ₗ.[R] F
x : E
h : x ∈ f.domain
⊢ ∃ x_1, ∃ (h : x ∈ f.domain), ↑f ⟨x, ⋯⟩ = x_1

Tactic:
·

Goal state after:
case mp
R : Type u_1
inst✝⁴ : Ring R
E : Type u_4
inst✝³ : AddCommGroup E
inst✝² : Module R E
F : Type u_5
inst✝¹ : AddCommGroup F
inst✝ : Module R F
f : E →ₗ.[R] F
x : E
h : ∃ x_1, ∃ (h : x ∈ f.domain), ↑f ⟨x, ⋯⟩ = x_1
⊢ x ∈ f.domain
Module: Mathlib.LinearAlgebra.LinearPMap

Goal state before:
pp: case mpr
R : Type u_1
inst✝⁴ : Ring R
E : Type u_4
inst✝³ : AddCommGroup E
inst✝² : Module R E
F : Type u_5
inst✝¹ : AddCommGroup F
inst✝ : Module R F
f : E →ₗ.[R] F
x : E
h : x ∈ f.domain
⊢ ∃ x_1, ∃ (h : x ∈ f.domain), ↑f ⟨x, ⋯⟩ = x_1

Tactic:
·

Goal state after:
case mpr
R : Type u_1
inst✝⁴ : Ring R
E : Type u_4
inst✝³ : AddCommGroup E
inst✝² : Module R E
F : Type u_5
inst✝¹ : AddCommGroup F
inst✝ : Module R F
f : E →ₗ.[R] F
x : E
h : x ∈ f.domain
⊢ ∃ x_1, ∃ (h : x ∈ f.domain), ↑f ⟨x, ⋯⟩ = x_1
Module: Mathlib.Data.Nat.Prime.Defs

Goal state before:
pp: case neg.inl
n : ℕ
n2 : 2 ≤ n
x✝ : ℕ
k : ℕ := x✝
i : ℕ
e : x✝ = 2 * i + 3
a : ∀ (m : ℕ), 2 ≤ m → m ∣ n → x✝ ≤ m
h : ¬n < k * k
k2 : 2 ≤ k
dk : ¬k ∣ n
this : n.sqrt - k < n.sqrt + 2 - k
m2 : 2 ≤ x✝
d : x✝ ∣ n
⊢ k + 2 ≤ x✝

pp: case neg.inr
n : ℕ
n2 : 2 ≤ n
x✝ : ℕ
k : ℕ := x✝
i : ℕ
e : x✝ = 2 * i + 3
a : ∀ (m : ℕ), 2 ≤ m → m ∣ n → x✝ ≤ m
h : ¬n < k * k
k2 : 2 ≤ k
dk : ¬k ∣ n
this : n.sqrt - k < n.sqrt + 2 - k
m : ℕ
m2 : 2 ≤ m
d : m ∣ n
ml : x✝ < m
⊢ k + 2 ≤ m

Tactic:
·

Goal state after:
case neg.inl
n : ℕ
n2 : 2 ≤ n
x✝ : ℕ
k : ℕ := x✝
i : ℕ
e : x✝ = 2 * i + 3
a : ∀ (m : ℕ), 2 ≤ m → m ∣ n → x✝ ≤ m
h : ¬n < k * k
k2 : 2 ≤ k
dk : ¬k ∣ n
this : n.sqrt - k < n.sqrt + 2 - k
m2 : 2 ≤ x✝
d : x✝ ∣ n
⊢ k + 2 ≤ x✝
Module: Mathlib.Algebra.CharP.Defs

Goal state before:
pp: case inr
R : Type u_1
inst✝² : AddMonoidWithOne R
p : ℕ
inst✝¹ : CharP R p
a b : ℕ
inst✝ : IsLeftCancelAdd R
this :
  ∀ (R : Type u_1) [inst : AddMonoidWithOne R] (p : ℕ) [CharP R p] {a b : ℕ} [IsLeftCancelAdd R],
    a ≤ b → (↑a = ↑b ↔ a % p = b % p)
hle : b < a
⊢ ↑a = ↑b ↔ a % p = b % p

pp: R✝ : Type u_1
inst✝³ : AddMonoidWithOne R✝
p✝ a✝ b✝ : ℕ
R : Type u_1
inst✝² : AddMonoidWithOne R
p : ℕ
inst✝¹ : CharP R p
a b : ℕ
inst✝ : IsLeftCancelAdd R
hle : a ≤ b
⊢ ↑a = ↑b ↔ a % p = b % p

Tactic:
·

Goal state after:
case inr
R : Type u_1
inst✝² : AddMonoidWithOne R
p : ℕ
inst✝¹ : CharP R p
a b : ℕ
inst✝ : IsLeftCancelAdd R
this :
  ∀ (R : Type u_1) [inst : AddMonoidWithOne R] (p : ℕ) [CharP R p] {a b : ℕ} [IsLeftCancelAdd R],
    a ≤ b → (↑a = ↑b ↔ a % p = b % p)
hle : b < a
⊢ ↑a = ↑b ↔ a % p = b % p
Module: Mathlib.Algebra.CharP.Defs

Goal state before:
pp: case mp
R✝ : Type u_1
inst✝³ : AddMonoidWithOne R✝
p✝ a✝ b : ℕ
R : Type u_1
inst✝² : AddMonoidWithOne R
p : ℕ
inst✝¹ : CharP R p
a : ℕ
inst✝ : IsLeftCancelAdd R
c : ℕ
hle : a ≤ a + c
⊢ p ∣ c → a % p = (a + c) % p

pp: case mpr
R✝ : Type u_1
inst✝³ : AddMonoidWithOne R✝
p✝ a✝ b : ℕ
R : Type u_1
inst✝² : AddMonoidWithOne R
p : ℕ
inst✝¹ : CharP R p
a : ℕ
inst✝ : IsLeftCancelAdd R
c : ℕ
hle : a ≤ a + c
⊢ a % p = (a + c) % p → p ∣ c

Tactic:
·

Goal state after:
case mp
R✝ : Type u_1
inst✝³ : AddMonoidWithOne R✝
p✝ a✝ b : ℕ
R : Type u_1
inst✝² : AddMonoidWithOne R
p : ℕ
inst✝¹ : CharP R p
a : ℕ
inst✝ : IsLeftCancelAdd R
c : ℕ
hle : a ≤ a + c
⊢ p ∣ c → a % p = (a + c) % p
Module: Mathlib.LinearAlgebra.LinearPMap

Goal state before:
pp: case mp
R : Type u_1
inst✝⁷ : Ring R
E : Type u_4
inst✝⁶ : AddCommGroup E
inst✝⁵ : Module R E
F : Type u_5
inst✝⁴ : AddCommGroup F
M : Type u_7
inst✝³ : Monoid M
inst✝² : DistribMulAction M F
inst✝¹ : Module R F
inst✝ : SMulCommClass R M F
f : E →ₗ.[R] F
z : M
x_fst : E
x_snd : F
h : (x_fst, x_snd) ∈ (z • f).graph
⊢ (x_fst, x_snd) ∈ Submodule.map (LinearMap.id.prodMap (z • LinearMap.id)) f.graph

pp: case mpr
R : Type u_1
inst✝⁷ : Ring R
E : Type u_4
inst✝⁶ : AddCommGroup E
inst✝⁵ : Module R E
F : Type u_5
inst✝⁴ : AddCommGroup F
M : Type u_7
inst✝³ : Monoid M
inst✝² : DistribMulAction M F
inst✝¹ : Module R F
inst✝ : SMulCommClass R M F
f : E →ₗ.[R] F
z : M
x_fst : E
x_snd : F
h : (x_fst, x_snd) ∈ Submodule.map (LinearMap.id.prodMap (z • LinearMap.id)) f.graph
⊢ (x_fst, x_snd) ∈ (z • f).graph

Tactic:
·

Goal state after:
case mp
R : Type u_1
inst✝⁷ : Ring R
E : Type u_4
inst✝⁶ : AddCommGroup E
inst✝⁵ : Module R E
F : Type u_5
inst✝⁴ : AddCommGroup F
M : Type u_7
inst✝³ : Monoid M
inst✝² : DistribMulAction M F
inst✝¹ : Module R F
inst✝ : SMulCommClass R M F
f : E →ₗ.[R] F
z : M
x_fst : E
x_snd : F
h : (x_fst, x_snd) ∈ (z • f).graph
⊢ (x_fst, x_snd) ∈ Submodule.map (LinearMap.id.prodMap (z • LinearMap.id)) f.graph
Module: Mathlib.Algebra.CharP.Defs

Goal state before:
pp: case inl
R : Type u_1
inst✝¹ : AddGroupWithOne R
p : ℕ
inst✝ : CharP R p
a : ℤ
h : a < 0
⊢ ↑a = 0 ↔ ↑p ∣ a

pp: case inr.inl
R : Type u_1
inst✝¹ : AddGroupWithOne R
p : ℕ
inst✝ : CharP R p
⊢ ↑0 = 0 ↔ ↑p ∣ 0

pp: case inr.inr
R : Type u_1
inst✝¹ : AddGroupWithOne R
p : ℕ
inst✝ : CharP R p
a : ℤ
h : 0 < a
⊢ ↑a = 0 ↔ ↑p ∣ a

Tactic:
·

Goal state after:
case inl
R : Type u_1
inst✝¹ : AddGroupWithOne R
p : ℕ
inst✝ : CharP R p
a : ℤ
h : a < 0
⊢ ↑a = 0 ↔ ↑p ∣ a
Module: Mathlib.Algebra.CharP.Defs

Goal state before:
pp: case inr.inl
R : Type u_1
inst✝¹ : AddGroupWithOne R
p : ℕ
inst✝ : CharP R p
⊢ ↑0 = 0 ↔ ↑p ∣ 0

pp: case inr.inr
R : Type u_1
inst✝¹ : AddGroupWithOne R
p : ℕ
inst✝ : CharP R p
a : ℤ
h : 0 < a
⊢ ↑a = 0 ↔ ↑p ∣ a

Tactic:
·

Goal state after:
case inr.inl
R : Type u_1
inst✝¹ : AddGroupWithOne R
p : ℕ
inst✝ : CharP R p
⊢ ↑0 = 0 ↔ ↑p ∣ 0
Module: Mathlib.Algebra.CharP.Defs

Goal state before:
pp: case inr.inr
R : Type u_1
inst✝¹ : AddGroupWithOne R
p : ℕ
inst✝ : CharP R p
a : ℤ
h : 0 < a
⊢ ↑a = 0 ↔ ↑p ∣ a

Tactic:
·

Goal state after:
case inr.inr
R : Type u_1
inst✝¹ : AddGroupWithOne R
p : ℕ
inst✝ : CharP R p
a : ℤ
h : 0 < a
⊢ ↑a = 0 ↔ ↑p ∣ a
Module: Mathlib.Data.Nat.Prime.Defs

Goal state before:
pp: case pos
n : ℕ
n1 : n ≠ 1
n0 : n = 0
⊢ n.minFacProp n.minFac

pp: case neg
n : ℕ
n1 : n ≠ 1
n0 : ¬n = 0
⊢ n.minFacProp n.minFac

Tactic:
·

Goal state after:
case pos
n : ℕ
n1 : n ≠ 1
n0 : n = 0
⊢ n.minFacProp n.minFac
Module: Mathlib.Data.Nat.Prime.Defs

Goal state before:
pp: case pos
n : ℕ
n1 : n ≠ 1
n0 : ¬n = 0
n2 : 2 ≤ n
d2 : 2 ∣ n
⊢ n.minFacProp 2

pp: case neg
n : ℕ
n1 : n ≠ 1
n0 : ¬n = 0
n2 : 2 ≤ n
d2 : ¬2 ∣ n
⊢ n.minFacProp (n.minFacAux 3)

Tactic:
·

Goal state after:
case pos
n : ℕ
n1 : n ≠ 1
n0 : ¬n = 0
n2 : 2 ≤ n
d2 : 2 ∣ n
⊢ n.minFacProp 2
Module: Mathlib.Data.Nat.Prime.Defs

Goal state before:
pp: case neg
n : ℕ
n1 : n ≠ 1
n0 : ¬n = 0
n2 : 2 ≤ n
d2 : ¬2 ∣ n
⊢ n.minFacProp (n.minFacAux 3)

Tactic:
·

Goal state after:
case neg
n : ℕ
n1 : n ≠ 1
n0 : ¬n = 0
n2 : 2 ≤ n
d2 : ¬2 ∣ n
⊢ n.minFacProp (n.minFacAux 3)
Module: Mathlib.Data.Nat.Prime.Defs

Goal state before:
pp: case pos
n m✝ : ℕ
n1 : n = 1
⊢ 2 ≤ m✝ → m✝ ∣ n → n.minFac ≤ m✝

pp: case neg
n m✝ : ℕ
n1 : ¬n = 1
⊢ 2 ≤ m✝ → m✝ ∣ n → n.minFac ≤ m✝

Tactic:
·

Goal state after:
case pos
n m✝ : ℕ
n1 : n = 1
⊢ 2 ≤ m✝ → m✝ ∣ n → n.minFac ≤ m✝
Module: Mathlib.Data.Nat.Prime.Defs

Goal state before:
pp: case neg
n m✝ : ℕ
n1 : ¬n = 1
⊢ 2 ≤ m✝ → m✝ ∣ n → n.minFac ≤ m✝

Tactic:
·

Goal state after:
case neg
n m✝ : ℕ
n1 : ¬n = 1
⊢ 2 ≤ m✝ → m✝ ∣ n → n.minFac ≤ m✝
Module: Mathlib.Data.Nat.Prime.Defs

Goal state before:
pp: case pos
n : ℕ
n1 : n = 1
⊢ 0 < n.minFac

pp: case neg
n : ℕ
n1 : ¬n = 1
⊢ 0 < n.minFac

Tactic:
·

Goal state after:
case pos
n : ℕ
n1 : n = 1
⊢ 0 < n.minFac
Module: Mathlib.Data.Nat.Prime.Defs

Goal state before:
pp: case neg
n : ℕ
n1 : ¬n = 1
⊢ 0 < n.minFac

Tactic:
·

Goal state after:
case neg
n : ℕ
n1 : ¬n = 1
⊢ 0 < n.minFac
Module: Mathlib.LinearAlgebra.LinearPMap

Goal state before:
pp: case mp
R : Type u_1
inst✝⁴ : Ring R
E : Type u_4
inst✝³ : AddCommGroup E
inst✝² : Module R E
F : Type u_5
inst✝¹ : AddCommGroup F
inst✝ : Module R F
f : E →ₗ.[R] F
x_fst : E
x_snd : F
h : (x_fst, x_snd) ∈ (-f).graph
⊢ (x_fst, x_snd) ∈ Submodule.map (LinearMap.id.prodMap (-LinearMap.id)) f.graph

pp: case mpr
R : Type u_1
inst✝⁴ : Ring R
E : Type u_4
inst✝³ : AddCommGroup E
inst✝² : Module R E
F : Type u_5
inst✝¹ : AddCommGroup F
inst✝ : Module R F
f : E →ₗ.[R] F
x_fst : E
x_snd : F
h : (x_fst, x_snd) ∈ Submodule.map (LinearMap.id.prodMap (-LinearMap.id)) f.graph
⊢ (x_fst, x_snd) ∈ (-f).graph

Tactic:
·

Goal state after:
case mp
R : Type u_1
inst✝⁴ : Ring R
E : Type u_4
inst✝³ : AddCommGroup E
inst✝² : Module R E
F : Type u_5
inst✝¹ : AddCommGroup F
inst✝ : Module R F
f : E →ₗ.[R] F
x_fst : E
x_snd : F
h : (x_fst, x_snd) ∈ (-f).graph
⊢ (x_fst, x_snd) ∈ Submodule.map (LinearMap.id.prodMap (-LinearMap.id)) f.graph
Module: Mathlib.Data.Nat.Prime.Defs

Goal state before:
pp: n : ℕ
pos : 0 < n
np : ¬Prime n
x : ℕ
hx : n = n.minFac * (x + 2)
⊢ n.minFac ≤ n.minFac * (x + 2) / n.minFac

Tactic:
rw [Nat.mul_div_cancel_left _ (minFac_pos _)]

Goal state after:
n : ℕ
pos : 0 < n
np : ¬Prime n
x : ℕ
hx : n = n.minFac * (x + 2)
⊢ n.minFac ≤ x + 2
Module: Mathlib.Data.Nat.Prime.Defs

Goal state before:
pp: case mp
n : ℕ
⊢ n.minFac = 1 → n = 1

pp: case mpr
n : ℕ
⊢ n = 1 → n.minFac = 1

Tactic:
·

Goal state after:
case mp
n : ℕ
⊢ n.minFac = 1 → n = 1
Module: Mathlib.Data.Nat.Prime.Defs

Goal state before:
pp: case mpr
n : ℕ
⊢ n = 1 → n.minFac = 1

Tactic:
·

Goal state after:
case mpr
n : ℕ
⊢ n = 1 → n.minFac = 1
Module: Mathlib.Data.Nat.Prime.Defs

Goal state before:
pp: case mp
n : ℕ
⊢ n.minFac = 2 → 2 ∣ n

pp: case mpr
n : ℕ
⊢ 2 ∣ n → n.minFac = 2

Tactic:
·

Goal state after:
case mp
n : ℕ
⊢ n.minFac = 2 → 2 ∣ n
Module: Mathlib.Data.Nat.Prime.Defs

Goal state before:
pp: case mpr
n : ℕ
⊢ 2 ∣ n → n.minFac = 2

Tactic:
·

Goal state after:
case mpr
n : ℕ
⊢ 2 ∣ n → n.minFac = 2
Module: Mathlib.Algebra.CharP.Defs

Goal state before:
pp: case zero
R : Type u_1
inst✝¹ : AddMonoidWithOne R
inst✝ : CharZero R
⊢ 1 ≠ 0

pp: case prime
R : Type u_1
inst✝ : AddMonoidWithOne R
p : ℕ
hprime✝ : Nat.Prime p
hchar✝ : CharP R p
⊢ p ≠ 0

Tactic:
·

Goal state after:
case zero
R : Type u_1
inst✝¹ : AddMonoidWithOne R
inst✝ : CharZero R
⊢ 1 ≠ 0
Module: Mathlib.Algebra.CharP.Defs

Goal state before:
pp: case prime
R : Type u_1
inst✝ : AddMonoidWithOne R
p : ℕ
hprime✝ : Nat.Prime p
hchar✝ : CharP R p
⊢ p ≠ 0

Tactic:
·

Goal state after:
case prime
R : Type u_1
inst✝ : AddMonoidWithOne R
p : ℕ
hprime✝ : Nat.Prime p
hchar✝ : CharP R p
⊢ p ≠ 0
Module: Mathlib.LinearAlgebra.LinearPMap

Goal state before:
pp: case mp
R : Type u_1
inst✝⁴ : Ring R
E : Type u_4
inst✝³ : AddCommGroup E
inst✝² : Module R E
F : Type u_5
inst✝¹ : AddCommGroup F
inst✝ : Module R F
f : E →ₗ.[R] F
x : E
h : x ∈ f.domain
⊢ ∃ y, (x, y) ∈ f.graph

pp: case mpr
R : Type u_1
inst✝⁴ : Ring R
E : Type u_4
inst✝³ : AddCommGroup E
inst✝² : Module R E
F : Type u_5
inst✝¹ : AddCommGroup F
inst✝ : Module R F
f : E →ₗ.[R] F
x : E
h : ∃ y, (x, y) ∈ f.graph
⊢ x ∈ f.domain

Tactic:
·

Goal state after:
case mp
R : Type u_1
inst✝⁴ : Ring R
E : Type u_4
inst✝³ : AddCommGroup E
inst✝² : Module R E
F : Type u_5
inst✝¹ : AddCommGroup F
inst✝ : Module R F
f : E →ₗ.[R] F
x : E
h : x ∈ f.domain
⊢ ∃ y, (x, y) ∈ f.graph
Module: Mathlib.Algebra.CharP.Defs

Goal state before:
pp: case zero
R : Type u_1
inst✝¹ : AddMonoidWithOne R
q : ℕ
hq : ExpChar R q
inst✝ : CharZero R
⊢ 1 = q

pp: case prime
R : Type u_1
inst✝ : AddMonoidWithOne R
p q : ℕ
hq : ExpChar R q
hp' : Nat.Prime p
hchar✝ : CharP R p
⊢ p = q

Tactic:
·

Goal state after:
case zero
R : Type u_1
inst✝¹ : AddMonoidWithOne R
q : ℕ
hq : ExpChar R q
inst✝ : CharZero R
⊢ 1 = q
Module: Mathlib.Algebra.CharP.Defs

Goal state before:
pp: case prime
R : Type u_1
inst✝ : AddMonoidWithOne R
p q : ℕ
hq : ExpChar R q
hp' : Nat.Prime p
hchar✝ : CharP R p
⊢ p = q

Tactic:
·

Goal state after:
case prime
R : Type u_1
inst✝ : AddMonoidWithOne R
p q : ℕ
hq : ExpChar R q
hp' : Nat.Prime p
hchar✝ : CharP R p
⊢ p = q
Module: Mathlib.Data.Nat.Prime.Defs

Goal state before:
pp: case a
m n : ℕ
H : ∀ (k : ℕ), Prime k → k ∣ m → ¬k ∣ n
g2 : ¬m.gcd n = 1
p : ℕ
hp : Prime p
hpdvd : p ∣ m.gcd n
⊢ m.gcd n ∣ m

pp: case a
m n : ℕ
H : ∀ (k : ℕ), Prime k → k ∣ m → ¬k ∣ n
g2 : ¬m.gcd n = 1
p : ℕ
hp : Prime p
hpdvd : p ∣ m.gcd n
⊢ m.gcd n ∣ n

Tactic:
·

Goal state after:
case a
m n : ℕ
H : ∀ (k : ℕ), Prime k → k ∣ m → ¬k ∣ n
g2 : ¬m.gcd n = 1
p : ℕ
hp : Prime p
hpdvd : p ∣ m.gcd n
⊢ m.gcd n ∣ m
Module: Mathlib.Algebra.CharP.Defs

Goal state before:
pp: case zero
R : Type u_1
inst✝¹ : AddMonoidWithOne R
hp : CharP R 0
inst✝ : CharZero R
⊢ 1 = 1

pp: case prime
R : Type u_1
inst✝ : AddMonoidWithOne R
q : ℕ
hp : CharP R 0
hq_prime : Nat.Prime q
hchar✝ : CharP R q
⊢ q = 1

Tactic:
·

Goal state after:
case zero
R : Type u_1
inst✝¹ : AddMonoidWithOne R
hp : CharP R 0
inst✝ : CharZero R
⊢ 1 = 1
Module: Mathlib.Algebra.CharP.Defs

Goal state before:
pp: case prime
R : Type u_1
inst✝ : AddMonoidWithOne R
q : ℕ
hp : CharP R 0
hq_prime : Nat.Prime q
hchar✝ : CharP R q
⊢ q = 1

Tactic:
·

Goal state after:
case prime
R : Type u_1
inst✝ : AddMonoidWithOne R
q : ℕ
hp : CharP R 0
hq_prime : Nat.Prime q
hchar✝ : CharP R q
⊢ q = 1
Module: Mathlib.Data.Nat.Prime.Defs

Goal state before:
pp: case a
m n : ℕ
H : ∀ (k : ℕ), Prime k → k ∣ m → ¬k ∣ n
g2 : ¬m.gcd n = 1
p : ℕ
hp : Prime p
hpdvd : p ∣ m.gcd n
⊢ m.gcd n ∣ n

Tactic:
·

Goal state after:
case a
m n : ℕ
H : ∀ (k : ℕ), Prime k → k ∣ m → ¬k ∣ n
g2 : ¬m.gcd n = 1
p : ℕ
hp : Prime p
hpdvd : p ∣ m.gcd n
⊢ m.gcd n ∣ n
Module: Mathlib.LinearAlgebra.LinearPMap

Goal state before:
pp: case mp
R : Type u_1
inst✝⁴ : Ring R
E : Type u_4
inst✝³ : AddCommGroup E
inst✝² : Module R E
F : Type u_5
inst✝¹ : AddCommGroup F
inst✝ : Module R F
f : E →ₗ.[R] F
y : F
h : y ∈ Set.range ↑f
⊢ ∃ x, (x, y) ∈ f.graph

pp: case mpr
R : Type u_1
inst✝⁴ : Ring R
E : Type u_4
inst✝³ : AddCommGroup E
inst✝² : Module R E
F : Type u_5
inst✝¹ : AddCommGroup F
inst✝ : Module R F
f : E →ₗ.[R] F
y : F
h : ∃ x, (x, y) ∈ f.graph
⊢ y ∈ Set.range ↑f

Tactic:
·

Goal state after:
case mp
R : Type u_1
inst✝⁴ : Ring R
E : Type u_4
inst✝³ : AddCommGroup E
inst✝² : Module R E
F : Type u_5
inst✝¹ : AddCommGroup F
inst✝ : Module R F
f : E →ₗ.[R] F
y : F
h : y ∈ Set.range ↑f
⊢ ∃ x, (x, y) ∈ f.graph
Module: Mathlib.Data.Nat.Prime.Defs

Goal state before:
pp: p n : ℕ
pp : Prime p
co : p.Coprime n
d : p ∣ n
⊢ p ∣ n * 1

Tactic:
simp [d]

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

Goal state before:
pp: case zero
R : Type u_1
inst✝¹ : AddMonoidWithOne R
p : ℕ
hp : CharP R p
inst✝ : CharZero R
⊢ p = 1 ↔ Nat.Prime p

pp: case prime
R : Type u_1
inst✝ : AddMonoidWithOne R
p q : ℕ
hp : CharP R p
hq_prime : Nat.Prime q
hchar✝ : CharP R q
⊢ p = q ↔ Nat.Prime p

Tactic:
·

Goal state after:
case zero
R : Type u_1
inst✝¹ : AddMonoidWithOne R
p : ℕ
hp : CharP R p
inst✝ : CharZero R
⊢ p = 1 ↔ Nat.Prime p
Module: Mathlib.Algebra.CharP.Defs

Goal state before:
pp: case prime
R : Type u_1
inst✝ : AddMonoidWithOne R
p q : ℕ
hp : CharP R p
hq_prime : Nat.Prime q
hchar✝ : CharP R q
⊢ p = q ↔ Nat.Prime p

Tactic:
·

Goal state after:
case prime
R : Type u_1
inst✝ : AddMonoidWithOne R
p q : ℕ
hp : CharP R p
hq_prime : Nat.Prime q
hchar✝ : CharP R q
⊢ p = q ↔ Nat.Prime p
Module: Mathlib.LinearAlgebra.LinearPMap

Goal state before:
pp: case left
R : Type u_1
inst✝⁴ : Ring R
E : Type u_4
inst✝³ : AddCommGroup E
inst✝² : Module R E
F : Type u_5
inst✝¹ : AddCommGroup F
inst✝ : Module R F
f g : E →ₗ.[R] F
h : f.graph ≤ g.graph
⊢ f.domain ≤ g.domain

pp: case right
R : Type u_1
inst✝⁴ : Ring R
E : Type u_4
inst✝³ : AddCommGroup E
inst✝² : Module R E
F : Type u_5
inst✝¹ : AddCommGroup F
inst✝ : Module R F
f g : E →ₗ.[R] F
h : f.graph ≤ g.graph
⊢ ∀ ⦃x : ↥f.domain⦄ ⦃y : ↥g.domain⦄, ↑x = ↑y → ↑f x = ↑g y

Tactic:
·

Goal state after:
case left
R : Type u_1
inst✝⁴ : Ring R
E : Type u_4
inst✝³ : AddCommGroup E
inst✝² : Module R E
F : Type u_5
inst✝¹ : AddCommGroup F
inst✝ : Module R F
f g : E →ₗ.[R] F
h : f.graph ≤ g.graph
⊢ f.domain ≤ g.domain
Module: Mathlib.Algebra.CharP.Defs

Goal state before:
pp: case zero
R : Type u_1
inst✝¹ : NonAssocSemiring R
inst✝ : CharZero R
⊢ ringExpChar R = 1

pp: case prime
R : Type u_1
inst✝ : NonAssocSemiring R
q : ℕ
h : Nat.Prime q
hchar✝ : CharP R q
⊢ ringExpChar R = q

Tactic:
·

Goal state after:
case zero
R : Type u_1
inst✝¹ : NonAssocSemiring R
inst✝ : CharZero R
⊢ ringExpChar R = 1
Module: Mathlib.Algebra.CharP.Defs

Goal state before:
pp: case zero
R : Type u_1
inst✝² : NonAssocSemiring R
inst✝¹ : Nontrivial R
p : ℕ
hp : CharP R p
inst✝ : CharZero R
⊢ p = 0

pp: case prime
R : Type u_1
inst✝¹ : NonAssocSemiring R
inst✝ : Nontrivial R
p : ℕ
hp : CharP R p
hprime✝ : Nat.Prime 1
hchar✝ : CharP R 1
⊢ p = 0

Tactic:
·

Goal state after:
case zero
R : Type u_1
inst✝² : NonAssocSemiring R
inst✝¹ : Nontrivial R
p : ℕ
hp : CharP R p
inst✝ : CharZero R
⊢ p = 0
Module: Mathlib.Algebra.CharP.Defs

Goal state before:
pp: case prime
R : Type u_1
inst✝¹ : NonAssocSemiring R
inst✝ : Nontrivial R
p : ℕ
hp : CharP R p
hprime✝ : Nat.Prime 1
hchar✝ : CharP R 1
⊢ p = 0

Tactic:
·

Goal state after:
case prime
R : Type u_1
inst✝¹ : NonAssocSemiring R
inst✝ : Nontrivial R
p : ℕ
hp : CharP R p
hprime✝ : Nat.Prime 1
hchar✝ : CharP R 1
⊢ p = 0