mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Algebra.Order.Star.Basic

Goal state before:
pp: R : Type u_1
inst✝³ : NonUnitalSemiring R
inst✝² : PartialOrder R
inst✝¹ : StarRing R
inst✝ : StarOrderedRing R
x✝ y x d : R
hd : d ∈ AddSubmonoid.closure (range fun s ↦ star s * s)
⊢ starAddEquiv d ∈ AddSubmonoid.closure (range fun s ↦ star s * s)

Tactic:
refine AddMonoidHom.mclosure_preimage_le _ _ <| AddSubmonoid.closure_mono ?_ hd

Goal state after:
R : Type u_1
inst✝³ : NonUnitalSemiring R
inst✝² : PartialOrder R
inst✝¹ : StarRing R
inst✝ : StarOrderedRing R
x✝ y x d : R
hd : d ∈ AddSubmonoid.closure (range fun s ↦ star s * s)
⊢ (range fun s ↦ star s * s) ⊆ ⇑starAddEquiv ⁻¹' range fun s ↦ star s * s
Module: Mathlib.LinearAlgebra.Dimension.Constructions

Goal state before:
pp: R : Type u
inst✝³ : Semiring R
inst✝² : StrongRankCondition R
m : Type v
n : Type w
inst✝¹ : Finite m
inst✝ : Finite n
⊢ Module.rank R (Matrix m n R) = lift.{max v w u, v} #m * lift.{max v w u, w} #n

Tactic:
rw [rank_matrix_module, rank_self, lift_one, mul_one, ← lift_lift.{v, max u w}, lift_id,
    ← lift_lift.{w, max u v}, lift_id]

Goal state after:
Module: Mathlib.LinearAlgebra.Dimension.Constructions

Goal state before:
pp: R : Type u
M : Type v
inst✝⁴ : Semiring R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
inst✝¹ : StrongRankCondition R
ι : Type u_2
inst✝ : Fintype ι
v : ι → M
hv : span R (range v) = ⊤
⊢ finrank R M ≤ Fintype.card ι

Tactic:
rw [← finrank_top, ← hv]
  exact (finrank_span_le_card _).trans (by convert! Fintype.card_range_le v; rw [Set.toFinset_card])

Goal state after:
Module: Mathlib.LinearAlgebra.Dimension.Constructions

Goal state before:
pp: case refine_1
R : Type u_2
V : Type u_3
inst✝² : CommRing R
inst✝¹ : AddCommGroup V
inst✝ : Module R V
W : Submodule R V
m : Type u_4
n : Type u_5
bW : Basis m R ↥W
bQ : Basis n R (V ⧸ W)
w : ↥W
i : m
⊢ ∀ (x y : ↥W),
    (fun i ↦ ((bW.sumQuot bQ).repr (W.subtype (x + y))) (Sum.inl i)) =
      (fun i ↦ ((bW.sumQuot bQ).repr (W.subtype x)) (Sum.inl i)) + fun i ↦
        ((bW.sumQuot bQ).repr (W.subtype y)) (Sum.inl i)

pp: case refine_2
R : Type u_2
V : Type u_3
inst✝² : CommRing R
inst✝¹ : AddCommGroup V
inst✝ : Module R V
W : Submodule R V
m : Type u_4
n : Type u_5
bW : Basis m R ↥W
bQ : Basis n R (V ⧸ W)
w : ↥W
i : m
⊢ ∀ (c : R) (x : ↥W),
    (fun i ↦ ((bW.sumQuot bQ).repr (W.subtype (c • x))) (Sum.inl i)) =
      c • fun i ↦ ((bW.sumQuot bQ).repr (W.subtype x)) (Sum.inl i)

pp: case refine_3
R : Type u_2
V : Type u_3
inst✝² : CommRing R
inst✝¹ : AddCommGroup V
inst✝ : Module R V
W : Submodule R V
m : Type u_4
n : Type u_5
bW : Basis m R ↥W
bQ : Basis n R (V ⧸ W)
w : ↥W
i : m
⊢ ∀ (i : m), (fun i_1 ↦ ((bW.sumQuot bQ).repr (W.subtype (bW i))) (Sum.inl i_1)) = ⇑(Finsupp.single i 1)

Tactic:
<;>

Goal state after:
case refine_1
R : Type u_2
V : Type u_3
inst✝² : CommRing R
inst✝¹ : AddCommGroup V
inst✝ : Module R V
W : Submodule R V
m : Type u_4
n : Type u_5
bW : Basis m R ↥W
bQ : Basis n R (V ⧸ W)
w : ↥W
i : m
⊢ ∀ (x y : ↥W),
    (fun i ↦ ((bW.sumQuot bQ).repr (W.subtype (x + y))) (Sum.inl i)) =
      (fun i ↦ ((bW.sumQuot bQ).repr (W.subtype x)) (Sum.inl i)) + fun i ↦
        ((bW.sumQuot bQ).repr (W.subtype y)) (Sum.inl i)

case refine_2
R : Type u_2
V : Type u_3
inst✝² : CommRing R
inst✝¹ : AddCommGroup V
inst✝ : Module R V
W : Submodule R V
m : Type u_4
n : Type u_5
bW : Basis m R ↥W
bQ : Basis n R (V ⧸ W)
w : ↥W
i : m
⊢ ∀ (c : R) (x : ↥W),
    (fun i ↦ ((bW.sumQuot bQ).repr (W.subtype (c • x))) (Sum.inl i)) =
      c • fun i ↦ ((bW.sumQuot bQ).repr (W.subtype x)) (Sum.inl i)

case refine_3
R : Type u_2
V : Type u_3
inst✝² : CommRing R
inst✝¹ : AddCommGroup V
inst✝ : Module R V
W : Submodule R V
m : Type u_4
n : Type u_5
bW : Basis m R ↥W
bQ : Basis n R (V ⧸ W)
w : ↥W
i : m
⊢ ∀ (i : m), (fun i_1 ↦ ((bW.sumQuot bQ).repr (W.subtype (bW i))) (Sum.inl i_1)) = ⇑(Finsupp.single i 1)
Module: Mathlib.LinearAlgebra.Dimension.Finite

Goal state before:
pp: case e'_1
R : Type u
M : Type v
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
n : ℕ
hn : n ≤ finrank R M
h : finrank R M = 0
⊢ (fun x ↦ x ∈ ∅) = fun x ↦ x ∈ ∅

pp: case e'_4
R : Type u
M : Type v
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
n : ℕ
hn : n ≤ finrank R M
h : finrank R M = 0
e_1✝ : ↥∅ = ↑∅
⊢ (fun x ↦ x ∈ ∅) = fun x ↦ x ∈ ∅

Tactic:
<;>

Goal state after:
case e'_1
R : Type u
M : Type v
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
n : ℕ
hn : n ≤ finrank R M
h : finrank R M = 0
⊢ (fun x ↦ x ∈ ∅) = fun x ↦ x ∈ ∅

case e'_4
R : Type u
M : Type v
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
n : ℕ
hn : n ≤ finrank R M
h : finrank R M = 0
e_1✝ : ↥∅ = ↑∅
⊢ (fun x ↦ x ∈ ∅) = fun x ↦ x ∈ ∅
Module: Mathlib.LinearAlgebra.Basis.VectorSpace

Goal state before:
pp: K : Type u_3
V : Type u_4
inst✝² : DivisionRing K
inst✝¹ : AddCommGroup V
inst✝ : Module K V
⊢ LinearIndependent K Subtype.val

Tactic:
convert! (ofVectorSpace K V).linearIndependent
  ext x
  rw [ofVectorSpace_apply_self]

Goal state after:
Module: Mathlib.Algebra.Star.NonUnitalSubalgebra

Goal state before:
pp: R : Type u
A : Type v
inst✝⁷ : CommSemiring R
inst✝⁶ : StarRing R
inst✝⁵ : NonUnitalSemiring A
inst✝⁴ : StarRing A
inst✝³ : Module R A
inst✝² : IsScalarTower R A A
inst✝¹ : SMulCommClass R A A
inst✝ : StarModule R A
s : Set A
⊢ (adjoin R s).toNonUnitalSubalgebra ≤ NonUnitalSubalgebra.centralizer R (↑(centralizer R s) ∪ star ↑(centralizer R s))

Tactic:
adjoin_toNonUnitalSubalgebra

Goal state after:
R : Type u
A : Type v
inst✝⁷ : CommSemiring R
inst✝⁶ : StarRing R
inst✝⁵ : NonUnitalSemiring A
inst✝⁴ : StarRing A
inst✝³ : Module R A
inst✝² : IsScalarTower R A A
inst✝¹ : SMulCommClass R A A
inst✝ : StarModule R A
s : Set A
⊢ NonUnitalAlgebra.adjoin R (s ∪ star s) ≤
    NonUnitalSubalgebra.centralizer R (↑(centralizer R s) ∪ star ↑(centralizer R s))
Module: Mathlib.LinearAlgebra.Dimension.FreeAndStrongRankCondition

Goal state before:
pp: K : Type u
V : Type v
inst✝⁴ : Ring K
inst✝³ : StrongRankCondition K
inst✝² : AddCommGroup V
inst✝¹ : Module K V
inst✝ : Free K V
n : ℕ
⊢ ↑n ≤ Module.rank K V ↔ ∃ s, s.card = n ∧ LinearIndependent K Subtype.val

Tactic:
simp only [le_rank_iff_exists_linearIndependent, mk_set_eq_nat_iff_finset]

Goal state after:
K : Type u
V : Type v
inst✝⁴ : Ring K
inst✝³ : StrongRankCondition K
inst✝² : AddCommGroup V
inst✝¹ : Module K V
inst✝ : Free K V
n : ℕ
⊢ (∃ s, (∃ t, ↑t = s ∧ t.card = n) ∧ LinearIndepOn K id s) ↔ ∃ s, s.card = n ∧ LinearIndependent K Subtype.val
Module: Mathlib.LinearAlgebra.Dimension.FreeAndStrongRankCondition

Goal state before:
pp: case mpr
K : Type u
V : Type v
inst✝⁴ : Ring K
inst✝³ : StrongRankCondition K
inst✝² : AddCommGroup V
inst✝¹ : Module K V
inst✝ : Free K V
n : ℕ
⊢ (∃ s, s.card = n ∧ LinearIndependent K Subtype.val) → ∃ s, (∃ t, ↑t = s ∧ t.card = n) ∧ LinearIndepOn K id s

Tactic:
rintro ⟨s, rfl, si⟩
    exact ⟨s, ⟨s, rfl, rfl⟩, si⟩

Goal state after:
Module: Mathlib.LinearAlgebra.Dimension.FreeAndStrongRankCondition

Goal state before:
pp: case mpr
K : Type u
V : Type v
inst✝⁴ : Ring K
inst✝³ : StrongRankCondition K
inst✝² : AddCommGroup V
inst✝¹ : Module K V
inst✝ : Free K V
κ : Type v
b : Basis κ K V
⊢ (∃ v₀, ∀ (v : V), ∃ r, r • v₀ = v) → Module.rank K V ≤ 1

Tactic:
· rintro ⟨v₀, hv₀⟩
    have h : K ∙ v₀ = ⊤ := by
      ext
      simp [mem_span_singleton, hv₀]
    rw [← rank_top, ← h]
    refine (rank_span_le _).trans_eq ?_
    simp

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

Goal state before:
pp: case hf
R : Type u
S : Type v
inst✝¹ : Semiring R
p q : R[X]
inst✝ : Semiring S
f : R →+* S
x : S
⊢ ∀ (i : ℕ), f 0 * x ^ i = 0

pp: case h_add
R : Type u
S : Type v
inst✝¹ : Semiring R
p q : R[X]
inst✝ : Semiring S
f : R →+* S
x : S
⊢ ∀ (a : ℕ) (b₁ b₂ : R), f (b₁ + b₂) * x ^ a = f b₁ * x ^ a + f b₂ * x ^ a

Tactic:
<;>

Goal state after:
case hf
R : Type u
S : Type v
inst✝¹ : Semiring R
p q : R[X]
inst✝ : Semiring S
f : R →+* S
x : S
⊢ ∀ (i : ℕ), f 0 * x ^ i = 0

case h_add
R : Type u
S : Type v
inst✝¹ : Semiring R
p q : R[X]
inst✝ : Semiring S
f : R →+* S
x : S
⊢ ∀ (a : ℕ) (b₁ b₂ : R), f (b₁ + b₂) * x ^ a = f b₁ * x ^ a + f b₂ * x ^ a
Module: Mathlib.Algebra.Polynomial.Eval.Defs

Goal state before:
pp: R : Type u
a : R
inst✝ : Semiring R
p : R[X]
x : R
h : Commute a x
⊢ eval₂ (RingHom.id R) x p * (RingHom.id R) a = eval x p * a

pp: case h
R : Type u
a : R
inst✝ : Semiring R
p : R[X]
x : R
h : Commute a x
⊢ Commute ((RingHom.id R) a) x

Tactic:
<;>

Goal state after:
R : Type u
a : R
inst✝ : Semiring R
p : R[X]
x : R
h : Commute a x
⊢ eval₂ (RingHom.id R) x p * (RingHom.id R) a = eval x p * a

case h
R : Type u
a : R
inst✝ : Semiring R
p : R[X]
x : R
h : Commute a x
⊢ Commute ((RingHom.id R) a) x
Module: Mathlib.Algebra.Polynomial.Eval.Defs

Goal state before:
pp: case refine_1
R : Type u_1
inst✝ : CommSemiring R
φ ψ χ : R[X]
⊢ ∀ (a : R), ((C a).comp ψ).comp χ = (C a).comp (ψ.comp χ)

pp: case refine_2
R : Type u_1
inst✝ : CommSemiring R
φ ψ χ : R[X]
⊢ ∀ (p q : R[X]),
    (p.comp ψ).comp χ = p.comp (ψ.comp χ) →
      (q.comp ψ).comp χ = q.comp (ψ.comp χ) → ((p + q).comp ψ).comp χ = (p + q).comp (ψ.comp χ)

pp: case refine_3
R : Type u_1
inst✝ : CommSemiring R
φ ψ χ : R[X]
⊢ ∀ (n : ℕ) (a : R),
    ((C a * X ^ n).comp ψ).comp χ = (C a * X ^ n).comp (ψ.comp χ) →
      ((C a * X ^ (n + 1)).comp ψ).comp χ = (C a * X ^ (n + 1)).comp (ψ.comp χ)

Tactic:
<;>

Goal state after:
case refine_1
R : Type u_1
inst✝ : CommSemiring R
φ ψ χ : R[X]
⊢ ∀ (a : R), ((C a).comp ψ).comp χ = (C a).comp (ψ.comp χ)

case refine_2
R : Type u_1
inst✝ : CommSemiring R
φ ψ χ : R[X]
⊢ ∀ (p q : R[X]),
    (p.comp ψ).comp χ = p.comp (ψ.comp χ) →
      (q.comp ψ).comp χ = q.comp (ψ.comp χ) → ((p + q).comp ψ).comp χ = (p + q).comp (ψ.comp χ)

case refine_3
R : Type u_1
inst✝ : CommSemiring R
φ ψ χ : R[X]
⊢ ∀ (n : ℕ) (a : R),
    ((C a * X ^ n).comp ψ).comp χ = (C a * X ^ n).comp (ψ.comp χ) →
      ((C a * X ^ (n + 1)).comp ψ).comp χ = (C a * X ^ (n + 1)).comp (ψ.comp χ)
Module: Mathlib.Data.Nat.Prime.Defs

Goal state before:
pp: p : ℕ
⊢ Prime p ↔ 2 ≤ p ∧ ∀ (m : ℕ), m ∣ p → m = 1 ∨ m = p

Tactic:
refine ⟨fun h => ⟨h.two_le, h.eq_one_or_self_of_dvd⟩, fun h => ?_⟩

Goal state after:
p : ℕ
h : 2 ≤ p ∧ ∀ (m : ℕ), m ∣ p → m = 1 ∨ m = p
⊢ Prime p
Module: Mathlib.Algebra.Polynomial.Eval.Defs

Goal state before:
pp: case ofNat
R : Type u
inst✝ : Ring R
p : R[X]
a✝ : ℕ
⊢ (↑(Int.ofNat a✝)).comp p = ↑(Int.ofNat a✝)

pp: case negSucc
R : Type u
inst✝ : Ring R
p : R[X]
a✝ : ℕ
⊢ (↑(Int.negSucc a✝)).comp p = ↑(Int.negSucc a✝)

Tactic:
<;>

Goal state after:
case ofNat
R : Type u
inst✝ : Ring R
p : R[X]
a✝ : ℕ
⊢ (↑(Int.ofNat a✝)).comp p = ↑(Int.ofNat a✝)

case negSucc
R : Type u
inst✝ : Ring R
p : R[X]
a✝ : ℕ
⊢ (↑(Int.negSucc a✝)).comp p = ↑(Int.negSucc a✝)
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
⊢ (∃ 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
⊢ 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
⊢ (∃ x_1, ∃ (h : x ∈ f.domain), ↑f ⟨x, ⋯⟩ = x_1) → x ∈ f.domain

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
⊢ x ∈ f.domain → ∃ x_1, ∃ (h : x ∈ f.domain), ↑f ⟨x, ⋯⟩ = x_1
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 (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
k2 : 2 ≤ k
dk : ¬k ∣ n
⊢ n.minFacProp (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
k2 : 2 ≤ k
dk : k ∣ n
⊢ n.minFacProp (if x✝ ∣ n then x✝ else n.minFacAux (x✝ + 2))

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 (if x✝ ∣ n then x✝ else 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
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
⊢ (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
⊢ (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
⊢ (x_fst, x_snd) ∈ (z • f).graph → (x_fst, x_snd) ∈ Submodule.map (LinearMap.id.prodMap (z • LinearMap.id)) f.graph

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
⊢ (x_fst, x_snd) ∈ Submodule.map (LinearMap.id.prodMap (z • LinearMap.id)) f.graph → (x_fst, x_snd) ∈ (z • f).graph
Module: Mathlib.Data.Nat.Prime.Defs

Goal state before:
pp: case zero
⊢ 0 ≠ 1 → ¬0 = 0 → 2 ≤ 0

pp: case succ.zero
⊢ 0 + 1 ≠ 1 → ¬0 + 1 = 0 → 2 ≤ 0 + 1

pp: case succ.succ
n✝ : ℕ
⊢ n✝ + 1 + 1 ≠ 1 → ¬n✝ + 1 + 1 = 0 → 2 ≤ n✝ + 1 + 1

Tactic:
<;>

Goal state after:
case zero
⊢ 0 ≠ 1 → ¬0 = 0 → 2 ≤ 0

case succ.zero
⊢ 0 + 1 ≠ 1 → ¬0 + 1 = 0 → 2 ≤ 0 + 1

case succ.succ
n✝ : ℕ
⊢ n✝ + 1 + 1 ≠ 1 → ¬n✝ + 1 + 1 = 0 → 2 ≤ n✝ + 1 + 1
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 (if 2 ∣ n then 2 else n.minFacAux 3)

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

Tactic:
<;>

Goal state after:
case pos
n : ℕ
n1 : n ≠ 1
n0 : ¬n = 0
n2 : 2 ≤ n
d2 : 2 ∣ n
⊢ n.minFacProp (if 2 ∣ n then 2 else n.minFacAux 3)

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

Goal state before:
pp: n : ℕ
pos : 0 < n
np : ¬Prime n
h0 : n = n.minFac * 0
⊢ ¬0 < n

Tactic:
h0,

Goal state after:
n : ℕ
pos : 0 < n
np : ¬Prime n
h0 : n = n.minFac * 0
⊢ ¬0 < n.minFac * 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_fst : E
x_snd : F
⊢ (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
⊢ (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
⊢ (x_fst, x_snd) ∈ (-f).graph → (x_fst, x_snd) ∈ Submodule.map (LinearMap.id.prodMap (-LinearMap.id)) f.graph

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
⊢ (x_fst, x_snd) ∈ Submodule.map (LinearMap.id.prodMap (-LinearMap.id)) f.graph → (x_fst, x_snd) ∈ (-f).graph
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
⊢ 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
⊢ (∃ 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
⊢ x ∈ f.domain → ∃ y, (x, y) ∈ f.graph

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
⊢ (∃ y, (x, y) ∈ f.graph) → x ∈ f.domain
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
⊢ p ∣ 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
⊢ p ∣ 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
⊢ p ∣ m

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
⊢ p ∣ 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
⊢ 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
⊢ (∃ 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
⊢ y ∈ Set.range ↑f → ∃ x, (x, y) ∈ f.graph

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
⊢ (∃ x, (x, y) ∈ f.graph) → y ∈ Set.range ↑f
Module: Mathlib.LinearAlgebra.LinearPMap

Goal state before:
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 : E
hx✝ : x ∈ f.domain
y : E
hx : y ∈ f.domain
hy : y ∈ g.domain
hxy : x = y
⊢ (y, ↑f ⟨x, hx✝⟩) ∈ f.graph

Tactic:
rw [← image_iff hx]

Goal state after:
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 : E
hx✝ : x ∈ f.domain
y : E
hx : y ∈ f.domain
hy : y ∈ g.domain
hxy : x = y
⊢ ↑f ⟨x, hx✝⟩ = ↑f ⟨y, hx⟩
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
g : Submodule R (E × F)
hg : ∀ x ∈ g, x.1 = 0 → x.2 = 0
x_fst : E
x_snd : F
⊢ (x_fst, x_snd) ∈ g.toLinearPMap.graph → (x_fst, x_snd) ∈ g

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
g : Submodule R (E × F)
hg : ∀ x ∈ g, x.1 = 0 → x.2 = 0
x_fst : E
x_snd : F
⊢ (x_fst, x_snd) ∈ g → (x_fst, x_snd) ∈ g.toLinearPMap.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
g : Submodule R (E × F)
hg : ∀ x ∈ g, x.1 = 0 → x.2 = 0
x_fst : E
x_snd : F
⊢ (x_fst, x_snd) ∈ g.toLinearPMap.graph → (x_fst, x_snd) ∈ g

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
g : Submodule R (E × F)
hg : ∀ x ∈ g, x.1 = 0 → x.2 = 0
x_fst : E
x_snd : F
⊢ (x_fst, x_snd) ∈ g → (x_fst, x_snd) ∈ g.toLinearPMap.graph
Module: Mathlib.Order.Filter.Extr

Goal state before:
pp: α : Type u
β : Type v
inst✝ : Preorder β
f : α → β
s : Set α
a : α
ha : a ∈ s
hfsa : IsMinOn f s a
⊢ IsGLB {x | ∃ x_1 ∈ s, f x_1 = x} (f a)

Tactic:
rw [isGLB_iff_le_iff]
  intro b
  simp only [mem_lowerBounds, mem_ofPred_eq, forall_exists_index, and_imp, forall_apply_eq_imp_iff₂]
  exact ⟨fun hba x hx ↦ le_trans hba (hfsa hx), fun hb ↦ hb a ha⟩

Goal state after:
Module: Mathlib.LinearAlgebra.LinearPMap

Goal state before:
pp: 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
hf : f.toFun.ker = ⊥
⊢ f.inverse.graph = Submodule.map (↑(LinearEquiv.prodComm R E F)) f.graph

Tactic:
by
  rw [inverse, Submodule.toLinearPMap_graph_eq _ (mem_inverse_graph_snd_eq_zero hf)]

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

Goal state before:
pp: case single_one_right
R : Type u_1
A : Type u_4
M : Type u_7
inst✝³ : CommSemiring R
inst✝² : Semiring A
inst✝¹ : Algebra R A
inst✝ : Monoid M
m✝ a✝ : M
⊢ ((mapDomainAlgHom R A (MonoidHom.id M)) (single m✝ 1)).coeff a✝ = ((AlgHom.id R A[M]) (single m✝ 1)).coeff a✝

pp: case single_one_left
R : Type u_1
A : Type u_4
M : Type u_7
inst✝³ : CommSemiring R
inst✝² : Semiring A
inst✝¹ : Algebra R A
inst✝ : Monoid M
x✝ : A
a✝ : M
⊢ (((mapDomainAlgHom R A (MonoidHom.id M)).comp singleOneAlgHom) x✝).coeff a✝ =
    (((AlgHom.id R A[M]).comp singleOneAlgHom) x✝).coeff a✝

Tactic:
<;>

Goal state after:
case single_one_right
R : Type u_1
A : Type u_4
M : Type u_7
inst✝³ : CommSemiring R
inst✝² : Semiring A
inst✝¹ : Algebra R A
inst✝ : Monoid M
m✝ a✝ : M
⊢ ((mapDomainAlgHom R A (MonoidHom.id M)) (single m✝ 1)).coeff a✝ = ((AlgHom.id R A[M]) (single m✝ 1)).coeff a✝

case single_one_left
R : Type u_1
A : Type u_4
M : Type u_7
inst✝³ : CommSemiring R
inst✝² : Semiring A
inst✝¹ : Algebra R A
inst✝ : Monoid M
x✝ : A
a✝ : M
⊢ (((mapDomainAlgHom R A (MonoidHom.id M)).comp singleOneAlgHom) x✝).coeff a✝ =
    (((AlgHom.id R A[M]).comp singleOneAlgHom) x✝).coeff a✝