mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.LinearAlgebra.Dimension.Constructions

Goal state before:
pp: R : Type u
M : Type v
ι : Type w
inst✝² : Ring R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
s t : Set ι
f : ι → M
hs : LinearIndepOn R f s
hst : Disjoint s t
⊢ LinearIndepOn R (⇑(span R (f '' s)).mkQ ∘ f) t ↔ LinearIndepOn R f (s ∪ t)

Tactic:
by
  rw [linearIndepOn_union_iff_quotient hst, and_iff_right hs]

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

Goal state before:
pp: R : Type u_1
M : Type u_2
inst✝⁴ : Ring R
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : IsDomain R
inst✝ : IsTorsionFree R M
⊢ (∀ (x : M), ∃ a, a ≠ 0 ∧ x = 0) ↔ ∀ (x : M), x = 0

Tactic:
exists_and_right,

Goal state after:
R : Type u_1
M : Type u_2
inst✝⁴ : Ring R
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : IsDomain R
inst✝ : IsTorsionFree R M
⊢ (∀ (x : M), (∃ x, x ≠ 0) ∧ x = 0) ↔ ∀ (x : M), x = 0
Module: Mathlib.LinearAlgebra.Dimension.Finite

Goal state before:
pp: R : Type u_1
M : Type u_2
inst✝⁴ : Ring R
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : IsDomain R
inst✝ : IsTorsionFree R M
h : Module.rank R M = 0
⊢ Module.Finite R M

Tactic:
by
  nontriviality R
  rw [rank_zero_iff] at h
  infer_instance

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

Goal state before:
pp: R : Type u_1
M : Type u_2
inst✝³ : Ring R
inst✝² : AddCommGroup M
inst✝¹ : Module R M
inst✝ : Nontrivial R
s : Submodule R M
h : 0 < Module.rank R ↥s
eq : s = ⊥
⊢ False

Tactic:
eq,

Goal state after:
R : Type u_1
M : Type u_2
inst✝³ : Ring R
inst✝² : AddCommGroup M
inst✝¹ : Module R M
inst✝ : Nontrivial R
s : Submodule R M
h : 0 < Module.rank R ↥⊥
eq : s = ⊥
⊢ False
Module: Mathlib.LinearAlgebra.Dimension.Constructions

Goal state before:
pp: R : Type u
ι : Type w
inst✝³ : Semiring R
inst✝² : StrongRankCondition R
inst✝¹ : Finite ι
inst✝ : Nontrivial R
s : Set ι
this : Fintype ι
⊢ Fintype.card ↑(⇑(basisFun R ι) '' s) = s.ncard

Tactic:
Fintype.card_eq_nat_card,

Goal state after:
R : Type u
ι : Type w
inst✝³ : Semiring R
inst✝² : StrongRankCondition R
inst✝¹ : Finite ι
inst✝ : Nontrivial R
s : Set ι
this : Fintype ι
⊢ Nat.card ↑(⇑(basisFun R ι) '' s) = s.ncard
Module: Mathlib.Algebra.Star.NonUnitalSubalgebra

Goal state before:
pp: F : Type v'
R' : Type u'
R : Type u
A : Type v
B : Type w
C : Type w'
inst✝⁷ : CommSemiring R
inst✝⁶ : StarRing R
inst✝⁵ : NonUnitalSemiring A
inst✝⁴ : StarRing A
inst✝³ : Module R A
inst✝² : StarModule R A
inst✝¹ : IsScalarTower R A A
inst✝ : SMulCommClass R A A
S : NonUnitalSubalgebra R A
a : A
ha : a ∈ (S ⊔ star S).carrier
⊢ star a ∈ (S ⊔ star S).carrier

Tactic:
by
    simpa [← mem_star_iff _ a, ← (@NonUnitalAlgebra.gi R A _ _ _ _ _).l_sup_u _ _, star_adjoin_comm,
      Set.union_comm] using ha

Goal state after:
Module: Mathlib.LinearAlgebra.Basis.VectorSpace

Goal state before:
pp: case refine_2
K : Type u_3
V : Type u_4
V' : Type u_5
inst✝⁴ : DivisionRing K
inst✝³ : AddCommGroup V
inst✝² : AddCommGroup V'
inst✝¹ : Module K V
inst✝ : Module K V'
p : Submodule K V
v : V
f : ↥p →ₗ[K] V'
hv : v ∉ p
y : V'
g : V →ₗ[K] V'
hg :
  g ∘ₗ ({ domain := p, toFun := f }.supSpanSingleton v y hv).domain.subtype =
    ({ domain := p, toFun := f }.supSpanSingleton v y hv).toFun
⊢ g v = y

Tactic:
· have := LinearPMap.supSpanSingleton_apply_self ⟨p, f⟩ y hv
    simpa using! congr($hg _).trans this

Goal state after:
Module: Mathlib.LinearAlgebra.Basis.VectorSpace

Goal state before:
pp: K : Type u_6
V : Type u_7
inst✝² : Field K
inst✝¹ : AddCommGroup V
inst✝ : Module K V
f : V →ₗ[K] K
v : V
hfv : f v ≠ 0
⊢ ∃ n b i, v = b i ∧ f = f v • b.coord i

Tactic:
set b₁ := Basis.ofVectorSpace K (ker f)

Goal state after:
K : Type u_6
V : Type u_7
inst✝² : Field K
inst✝¹ : AddCommGroup V
inst✝ : Module K V
f : V →ₗ[K] K
v : V
hfv : f v ≠ 0
b₁ : Basis (↑(Basis.ofVectorSpaceIndex K ↥f.ker)) K ↥f.ker := Basis.ofVectorSpace K ↥f.ker
⊢ ∃ n b i, v = b i ∧ f = f v • b.coord i
Module: Mathlib.LinearAlgebra.Dimension.Finite

Goal state before:
pp: R : Type u_1
M : Type u_2
inst✝⁴ : Ring R
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : StrongRankCondition R
inst✝ : Module.Finite R M
N : Submodule R M
this✝ : Nontrivial R
this : Module.rank R (M ⧸ N) + Module.rank R ↥N ≤ Module.rank R M
⊢ finrank R (M ⧸ N) + finrank R ↥N ≤ finrank R M

Tactic:
← finrank_eq_rank R M,

Goal state after:
R : Type u_1
M : Type u_2
inst✝⁴ : Ring R
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : StrongRankCondition R
inst✝ : Module.Finite R M
N : Submodule R M
this✝ : Nontrivial R
this : Module.rank R (M ⧸ N) + Module.rank R ↥N ≤ ↑(finrank R M)
⊢ finrank R (M ⧸ N) + finrank R ↥N ≤ finrank R M
Module: Mathlib.LinearAlgebra.LinearPMap

Goal state before:
pp: 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
f g : E →ₛₗ.[σ] F
h : ∀ (x : ↥f.domain) (y : ↥g.domain), ↑x = ↑y → ↑f x = ↑g y
x : ↥(f.domain ⊔ g.domain) → E
hx : ∀ (z : ↥(f.domain ⊔ g.domain)), x z ∈ f.domain
y : ↥(f.domain ⊔ g.domain) → E
hy : ∀ (z : ↥(f.domain ⊔ g.domain)), y z ∈ g.domain
hxy : ∀ (z : ↥(f.domain ⊔ g.domain)), x z + y z = ↑z
fg : ↥(f.domain ⊔ g.domain) → F := fun z ↦ ↑f ⟨x z, ⋯⟩ + ↑g ⟨y z, ⋯⟩
x' : ↥f.domain
y' : ↥g.domain
⊢ ∀ (z' : ↥(f.domain ⊔ g.domain)), ↑x' + ↑y' = ↑z' → fg z' = ↑f x' + ↑g y'

Tactic:
z'

Goal state after:
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
f g : E →ₛₗ.[σ] F
h : ∀ (x : ↥f.domain) (y : ↥g.domain), ↑x = ↑y → ↑f x = ↑g y
x : ↥(f.domain ⊔ g.domain) → E
hx : ∀ (z : ↥(f.domain ⊔ g.domain)), x z ∈ f.domain
y : ↥(f.domain ⊔ g.domain) → E
hy : ∀ (z : ↥(f.domain ⊔ g.domain)), y z ∈ g.domain
hxy : ∀ (z : ↥(f.domain ⊔ g.domain)), x z + y z = ↑z
fg : ↥(f.domain ⊔ g.domain) → F := fun z ↦ ↑f ⟨x z, ⋯⟩ + ↑g ⟨y z, ⋯⟩
x' : ↥f.domain
y' : ↥g.domain
z' : ↥(f.domain ⊔ g.domain)
⊢ ↑x' + ↑y' = ↑z' → fg z' = ↑f x' + ↑g y'
Module: Mathlib.LinearAlgebra.FiniteDimensional.Basic

Goal state before:
pp: K : Type u
V : Type v
inst✝³ : DivisionRing K
inst✝² : AddCommGroup V
inst✝¹ : Module K V
inst✝ : FiniteDimensional K V
f : V →ₗ[K] V
⊢ f.ker = ⊥ ↔ f.range = ⊤

Tactic:
range_eq_top,

Goal state after:
K : Type u
V : Type v
inst✝³ : DivisionRing K
inst✝² : AddCommGroup V
inst✝¹ : Module K V
inst✝ : FiniteDimensional K V
f : V →ₗ[K] V
⊢ f.ker = ⊥ ↔ Surjective ⇑f
Module: Mathlib.LinearAlgebra.Dimension.FreeAndStrongRankCondition

Goal state before:
pp: case refine_2
K : Type u
V : Type v
inst✝⁴ : Ring K
inst✝³ : StrongRankCondition K
inst✝² : AddCommGroup V
inst✝¹ : Module K V
inst✝ : Free K V
this : Nontrivial K
x✝ : ∃ v₀, v₀ ≠ 0 ∧ ∀ (v : V), ∃ r, r • v₀ = v
v₀ : V
h : v₀ ≠ 0
hv : ∀ (v : V), ∃ r, r • v₀ = v
H : ¬1 ≤ Module.rank K V
⊢ False

Tactic:
not_le,

Goal state after:
case refine_2
K : Type u
V : Type v
inst✝⁴ : Ring K
inst✝³ : StrongRankCondition K
inst✝² : AddCommGroup V
inst✝¹ : Module K V
inst✝ : Free K V
this : Nontrivial K
x✝ : ∃ v₀, v₀ ≠ 0 ∧ ∀ (v : V), ∃ r, r • v₀ = v
v₀ : V
h : v₀ ≠ 0
hv : ∀ (v : V), ∃ r, r • v₀ = v
H : Module.rank K V < 1
⊢ False
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
s : Submodule K V
inst✝ : Free K ↥s
⊢ Module.rank K ↥s = 1 ↔ ∃ v₀ ∈ s, v₀ ≠ 0 ∧ s ≤ K ∙ v₀

Tactic:
by
  simp_rw [rank_eq_one_iff, le_span_singleton_iff]
  refine ⟨fun ⟨⟨v₀, hv₀⟩, H, h⟩ ↦ ⟨v₀, hv₀, fun h' ↦ by
    simp only [h', ne_eq] at H; exact H rfl, fun v hv ↦ ?_⟩,
    fun ⟨v₀, hv₀, H, h⟩ ↦ ⟨⟨v₀, hv₀⟩,
      fun h' ↦ H (by rwa [AddSubmonoid.mk_eq_zero] at h'), fun ⟨v, hv⟩ ↦ ?_⟩⟩
  · obtain ⟨r, hr⟩ := h ⟨v, hv⟩
    exact ⟨r, by rwa [Subtype.ext_iff, coe_smul] at hr⟩
  · obtain ⟨r, hr⟩ := h v hv
    exact ⟨r, by rwa [Subtype.ext_iff, coe_smul]⟩

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

Goal state before:
pp: case mpr
K : Type u
V : Type v
inst✝³ : DivisionRing K
inst✝² : AddCommGroup V
inst✝¹ : Module K V
inst✝ : FiniteDimensional K V
f : V →ₗ[K] V
⊢ f.ker = ⊥ → IsUnit f

Tactic:
intro h_inj
    rw [ker_eq_bot] at h_inj
    exact ⟨⟨f, (LinearEquiv.ofInjectiveEndo f h_inj).symm.toLinearMap,
      LinearEquiv.ofInjectiveEndo_right_inv f h_inj, LinearEquiv.ofInjectiveEndo_left_inv f h_inj⟩,
      rfl⟩

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

Goal state before:
pp: case refine_2
F : Type u_1
E : Type u_2
inst✝⁵ : CommRing F
inst✝⁴ : StrongRankCondition F
inst✝³ : Ring E
inst✝² : Algebra F E
inst✝¹ : Nontrivial E
inst✝ : Free F ↥⊥
κ : Type u_2
b : Basis κ F ↥⊥
H : ¬1 ≤ Module.rank F ↥⊥
⊢ False

Tactic:
not_le,

Goal state after:
case refine_2
F : Type u_1
E : Type u_2
inst✝⁵ : CommRing F
inst✝⁴ : StrongRankCondition F
inst✝³ : Ring E
inst✝² : Algebra F E
inst✝¹ : Nontrivial E
inst✝ : Free F ↥⊥
κ : Type u_2
b : Basis κ F ↥⊥
H : Module.rank F ↥⊥ < 1
⊢ False
Module: Mathlib.LinearAlgebra.Dimension.FreeAndStrongRankCondition

Goal state before:
pp: F : Type u_1
E : Type u_2
inst✝⁵ : CommRing F
inst✝⁴ : StrongRankCondition F
inst✝³ : Ring E
inst✝² : Algebra F E
S : Subalgebra F E
inst✝¹ : Nontrivial E
inst✝ : Free F ↥S
⊢ finrank F ↥S = 1 ↔ S = ⊥

Tactic:
rw [← Subalgebra.rank_eq_one_iff]
  exact toNat_eq_iff one_ne_zero

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

Goal state before:
pp: case refine_2
K : Type u
V : Type v
inst✝² : DivisionRing K
inst✝¹ : AddCommGroup V
inst✝ : Module K V
S : Submodule K V
hS : finrank K ↥S = 1
T : Submodule K V
hT : T < S
this✝ : FiniteDimensional K ↥S
this : FiniteDimensional K ↥T
⊢ T = ⊥

Tactic:
← finrank_eq_zero (R := K)

Goal state after:
case refine_2
K : Type u
V : Type v
inst✝² : DivisionRing K
inst✝¹ : AddCommGroup V
inst✝ : Module K V
S : Submodule K V
hS : finrank K ↥S = 1
T : Submodule K V
hT : T < S
this✝ : FiniteDimensional K ↥S
this : FiniteDimensional K ↥T
⊢ finrank K ↥T = 0
Module: Mathlib.LinearAlgebra.LinearPMap

Goal state before:
pp: 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
f g : E →ₛₗ.[σ] F
h : ∀ (x : ↥f.domain) (y : ↥g.domain), ↑x = ↑y → ↑f x = ↑g y
z₁ : ↥f.domain
z₂ : ↥(f.sup g h).domain
hz : ↑z₁ = ↑z₂
⊢ ↑f z₁ = ↑(f.sup g h) z₂

Tactic:
← add_zero (f _),

Goal state after:
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
f g : E →ₛₗ.[σ] F
h : ∀ (x : ↥f.domain) (y : ↥g.domain), ↑x = ↑y → ↑f x = ↑g y
z₁ : ↥f.domain
z₂ : ↥(f.sup g h).domain
hz : ↑z₁ = ↑z₂
⊢ ↑f z₁ + 0 = ↑(f.sup g h) z₂
Module: Mathlib.Algebra.Polynomial.Eval.Defs

Goal state before:
pp: R : Type u
S : Type v
inst✝¹ : Semiring R
inst✝ : Semiring S
f : R →+* S
x : S
n : ℕ
⊢ eval₂ f x ↑n = ↑n

Tactic:
by
  induction n with
  | zero => simp only [eval₂_zero, Nat.cast_zero]
  | succ n ih => rw [n.cast_succ, eval₂_add, ih, eval₂_one, n.cast_succ]

Goal state after:
Module: Mathlib.LinearAlgebra.LinearPMap

Goal state before:
pp: 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)
x : ↥(sSup (domain '' c))
⊢ { p // ↑x ∈ (↑p).domain }

Tactic:
apply Classical.indefiniteDescription

Goal state after:
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)
x : ↥(sSup (domain '' c))
⊢ ∃ x_1, ↑x ∈ (↑x_1).domain
Module: Mathlib.Algebra.Polynomial.Eval.Defs

Goal state before:
pp: R : Type u
inst✝ : Semiring R
p : R[X]
n : ℕ
⊢ (C ↑n).comp p = C ↑n

Tactic:
C_comp

Goal state after:
R : Type u
inst✝ : Semiring R
p : R[X]
n : ℕ
⊢ C ↑n = C ↑n
Module: Mathlib.Algebra.Polynomial.Eval.Defs

Goal state before:
pp: R : Type u
inst✝ : Semiring R
p : R[X]
⊢ (C 0).comp p = C 0

Tactic:
C_comp

Goal state after:
R : Type u
inst✝ : Semiring R
p : R[X]
⊢ C 0 = C 0
Module: Mathlib.Algebra.Polynomial.Eval.Defs

Goal state before:
pp: R : Type u
inst✝ : Semiring R
p : R[X]
⊢ (C 1).comp p = C 1

Tactic:
C_comp

Goal state after:
R : Type u
inst✝ : Semiring R
p : R[X]
⊢ C 1 = C 1
Module: Mathlib.Algebra.FreeAlgebra

Goal state before:
pp: R : Type u_1
X : Type u_2
inst✝ : CommSemiring R
motive : FreeAlgebra R X → Prop
grade0 : ∀ (r : R), motive ((algebraMap R (FreeAlgebra R X)) r)
grade1 : ∀ (x : X), motive (ι R x)
mul : ∀ (a b : FreeAlgebra R X), motive a → motive b → motive (a * b)
add : ∀ (a b : FreeAlgebra R X), motive a → motive b → motive (a + b)
a : FreeAlgebra R X
s : Subalgebra R (FreeAlgebra R X) :=
  { carrier := {x | motive x}, mul_mem' := ⋯, one_mem' := ⋯, add_mem' := ⋯, zero_mem' := ⋯, algebraMap_mem' := grade0 }
of : X → ↥s := Subtype.coind (ι R) grade1
of_id : AlgHom.id R (FreeAlgebra R X) = s.val.comp ((lift R) of)
this : a = ↑(((lift R) of) a)
⊢ motive a

Tactic:
by
    rw [this]
    exact Subtype.prop (lift R of a)

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:
· rw [(CharP.eq R hp (.ofCharZero R) : p = 0)]
    decide

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: R : Type u_1
S : Type u_2
T : Type u_3
inst✝⁹ : Ring R
inst✝⁸ : Ring S
inst✝⁷ : Ring T
σ : R →+* S
τ : S →+* T
E : Type u_4
inst✝⁶ : AddCommGroup E
inst✝⁵ : Module R E
F : Type u_5
inst✝⁴ : AddCommGroup F
inst✝³ : Module S F
G : Type u_6
inst✝² : AddCommGroup G
inst✝¹ : Module T G
inst✝ : Module R F
g : Submodule R (E × F)
hg : ∀ x ∈ g, x.1 = 0 → x.2 = 0
v w : ↥(map (LinearMap.fst R E F) g)
hadd : ↑v + ↑w ∈ map (LinearMap.fst R E F) g
⊢ valFromGraph hg ⋯ = valFromGraph hg ⋯ + valFromGraph hg ⋯

Tactic:
have hvw := valFromGraph_mem hg hadd

Goal state after:
R : Type u_1
S : Type u_2
T : Type u_3
inst✝⁹ : Ring R
inst✝⁸ : Ring S
inst✝⁷ : Ring T
σ : R →+* S
τ : S →+* T
E : Type u_4
inst✝⁶ : AddCommGroup E
inst✝⁵ : Module R E
F : Type u_5
inst✝⁴ : AddCommGroup F
inst✝³ : Module S F
G : Type u_6
inst✝² : AddCommGroup G
inst✝¹ : Module T G
inst✝ : Module R F
g : Submodule R (E × F)
hg : ∀ x ∈ g, x.1 = 0 → x.2 = 0
v w : ↥(map (LinearMap.fst R E F) g)
hadd : ↑v + ↑w ∈ map (LinearMap.fst R E F) g
hvw : (↑v + ↑w, valFromGraph hg hadd) ∈ g
⊢ valFromGraph hg ⋯ = valFromGraph hg ⋯ + valFromGraph hg ⋯
Module: Mathlib.Order.Filter.Extr

Goal state before:
pp: α : Type u
β : Type v
inst✝² : AddCommGroup β
inst✝¹ : PartialOrder β
inst✝ : IsOrderedAddMonoid β
f g : α → β
a : α
l : Filter α
hf : IsMinFilter f l a
hg : IsMaxFilter g l a
⊢ IsMinFilter (fun x ↦ f x - g x) l a

Tactic:
by simpa only [sub_eq_add_neg] using hf.add hg.neg

Goal state after:
Module: Mathlib.Order.Filter.Extr

Goal state before:
pp: α : Type u
β : Type v
inst✝² : AddCommGroup β
inst✝¹ : PartialOrder β
inst✝ : IsOrderedAddMonoid β
f g : α → β
a : α
l : Filter α
hf : IsMaxFilter f l a
hg : IsMinFilter g l a
⊢ IsMaxFilter (fun x ↦ f x - g x) l a

Tactic:
by simpa only [sub_eq_add_neg] using hf.add hg.neg

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
g : Submodule R (E × F)
hg : ∀ x ∈ g, x.1 = 0 → x.2 = 0
⊢ g.toLinearPMap.toFun.range = map (LinearMap.snd R E F) g

Tactic:
← LinearPMap.graph_map_snd_eq_range,

Goal state after:
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
⊢ map (LinearMap.snd R E F) g.toLinearPMap.graph = map (LinearMap.snd R E F) g
Module: Mathlib.Algebra.MonoidAlgebra.Basic

Goal state before:
pp: R : Type u_1
S : Type u_2
T : Type u_3
A : Type u_4
B : Type u_5
C : Type u_6
M : Type u_7
N : Type u_8
O : Type u_9
inst✝⁷ : CommSemiring R
inst✝⁶ : Semiring A
inst✝⁵ : Semiring B
inst✝⁴ : Algebra R A
inst✝³ : Algebra R B
inst✝² : Monoid M
inst✝¹ : Monoid N
inst✝ : Monoid O
⊢ domCongr R A (MulEquiv.refl M) = AlgEquiv.refl

Tactic:
domCongr_refl

Goal state after:
R : Type u_1
S : Type u_2
T : Type u_3
A : Type u_4
B : Type u_5
C : Type u_6
M : Type u_7
N : Type u_8
O : Type u_9
inst✝⁷ : CommSemiring R
inst✝⁶ : Semiring A
inst✝⁵ : Semiring B
inst✝⁴ : Algebra R A
inst✝³ : Algebra R B
inst✝² : Monoid M
inst✝¹ : Monoid N
inst✝ : Monoid O
⊢ AlgEquiv.refl = AlgEquiv.refl
Module: Mathlib.Algebra.Polynomial.Degree.Defs

Goal state before:
pp: case pos
R : Type u
a : R
inst✝ : Semiring R
h : a = 0
⊢ (C a).degree ≤ 0

pp: case neg
R : Type u
a : R
inst✝ : Semiring R
h : ¬a = 0
⊢ (C a).degree ≤ 0

Tactic:
· rw [h, C_0]
    exact bot_le

Goal state after:
case neg
R : Type u
a : R
inst✝ : Semiring R
h : ¬a = 0
⊢ (C a).degree ≤ 0
Module: Mathlib.Algebra.Polynomial.Degree.Operations

Goal state before:
pp: R : Type u
inst✝ : Semiring R
p q : R[X]
H : (p + q).natDegree = 0
⊢ p.natDegree = q.natDegree

Tactic:
by_cases h₁ : natDegree p = 0; on_goal 1 => by_cases h₂ : natDegree q = 0
  · exact h₁.trans h₂.symm
  · apply natDegree_eq_of_natDegree_add_lt_right; rwa [H, Nat.pos_iff_ne_zero]
  · apply natDegree_eq_of_natDegree_add_lt_left; rwa [H, Nat.pos_iff_ne_zero]

Goal state after:
Module: Mathlib.Algebra.Polynomial.Degree.SmallDegree

Goal state before:
pp: R : Type u
a b c d : R
inst✝ : Semiring R
ha : a ≠ 0
⊢ (C b * X ^ 2 + C c * X + C d).degree < (C a * X ^ 3).degree

Tactic:
by
  simpa only [degree_C_mul_X_pow 3 ha] using! degree_quadratic_lt

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

Goal state before:
pp: R : Type u_1
A : Type u_3
T : Type u_4
inst✝² : Semiring R
inst✝¹ : SemilatticeInf T
inst✝ : OrderTop T
D : A → T
s : R[A]
hs : s.coeff.support.Nonempty
⊢ s.coeff.support.inf (WithTop.some ∘ D) = ↑(s.coeff.support.inf D)

Tactic:
rw [← Finset.coe_inf' hs, Finset.inf'_eq_inf]

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

Goal state before:
pp: R : Type u
σ : Type u_1
a : R
e : ℕ
n : σ
s : σ →₀ ℕ
inst✝ : CommSemiring R
⊢ (monomial (s + Finsupp.single n e)) a = (monomial s) a * (monomial (Finsupp.single n e)) 1

Tactic:
monomial_mul,

Goal state after:
R : Type u
σ : Type u_1
a : R
e : ℕ
n : σ
s : σ →₀ ℕ
inst✝ : CommSemiring R
⊢ (monomial (s + Finsupp.single n e)) a = (monomial (s + Finsupp.single n e)) (a * 1)
Module: Mathlib.Algebra.MvPolynomial.Basic

Goal state before:
pp: R : Type u
σ : Type u_1
a : R
e : ℕ
n : σ
s : σ →₀ ℕ
inst✝ : CommSemiring R
⊢ (monomial (Finsupp.single n e + s)) a = (monomial (Finsupp.single n e)) 1 * (monomial s) a

Tactic:
monomial_mul,

Goal state after:
R : Type u
σ : Type u_1
a : R
e : ℕ
n : σ
s : σ →₀ ℕ
inst✝ : CommSemiring R
⊢ (monomial (Finsupp.single n e + s)) a = (monomial (Finsupp.single n e + s)) (1 * a)
Module: Mathlib.Algebra.MvPolynomial.Eval

Goal state before:
pp: R : Type u
S₁ : Type v
σ : Type u_1
inst✝¹ : CommSemiring R
inst✝ : CommSemiring S₁
p : MvPolynomial σ R
f : R →+* S₁
g : σ → S₁
⊢ ∀ {s : σ →₀ ℕ} {a : R}, eval₂ f g (p * (monomial s) a) = eval₂ f g p * f a * s.prod fun n e ↦ g n ^ e

Tactic:
classical
  apply MvPolynomial.induction_on p
  · intro a' s a
    simp [C_mul_monomial, eval₂_monomial, f.map_mul]
  · intro p q ih_p ih_q
    simp [add_mul, eval₂_add, ih_p, ih_q]
  · intro p n ih s a
    exact
      calc (p * X n * monomial s a).eval₂ f g
        _ = (p * monomial (Finsupp.single n 1 + s) a).eval₂ f g := by
          rw [monomial_single_add, pow_one, mul_assoc]
        _ = (p * monomial (Finsupp.single n 1) 1).eval₂ f g * f a * s.prod fun n e => g n ^ e := by
          simp [ih, prod_single_index, prod_add_index, pow_one, pow_add, mul_assoc, mul_left_comm,
            f.map_one]

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

Goal state before:
pp: R : Type u
σ : Type u_1
inst✝ : CommSemiring R
m : σ →₀ ℕ
a : R
p : MvPolynomial σ R
⊢ coeff m (C a * p) = a * coeff m p

Tactic:
rw [mul_def, sum_C]
  · simp +contextual [sum_def, coeff_sum]
  simp

Goal state after:
Module: Mathlib.Algebra.MvPolynomial.Rename

Goal state before:
pp: σ : Type u_1
τ : Type u_2
R : Type u_4
inst✝ : CommSemiring R
f : σ → τ
hf : Injective f
i : σ
⊢ X ((Equiv.ofInjective f hf).symm ⟨f i, ⋯⟩) = X i

Tactic:
Equiv.ofInjective_symm_apply

Goal state after:
σ : Type u_1
τ : Type u_2
R : Type u_4
inst✝ : CommSemiring R
f : σ → τ
hf : Injective f
i : σ
⊢ X i = X i
Module: Mathlib.Algebra.MvPolynomial.Rename

Goal state before:
pp: case neg
σ : Type u_1
τ : Type u_2
R : Type u_4
inst✝¹ : CommSemiring R
f : σ → τ
hf : Injective f
s : τ →₀ ℕ
c : R
inst✝ : Decidable (↑s.support ⊆ range f)
h : ¬↑s.support ⊆ range f
⊢ (killCompl hf) ((monomial s) c) = 0

Tactic:
· exact killCompl_monomial_eq_zero_of_not_subset hf c h

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

Goal state before:
pp: R : Type u
σ : Type u_1
inst✝¹ : CommSemiring R
inst✝ : DecidableEq R
p q : MvPolynomial σ R
h : Disjoint p.support q.support
⊢ (p + q).coeffs = p.coeffs ∪ q.coeffs

Tactic:
by
  ext r
  simp only [mem_coeffs_iff, mem_support_iff, coeff_add, ne_eq, Finset.mem_union]
  have hl (n : σ →₀ ℕ) (hne : p.coeff n ≠ 0) : q.coeff n = 0 :=
    notMem_support_iff.mp <| h.notMem_of_mem_left_finset (mem_support_iff.mpr hne)
  have hr (n : σ →₀ ℕ) (hne : q.coeff n ≠ 0) : p.coeff n = 0 :=
    notMem_support_iff.mp <| h.notMem_of_mem_right_finset (mem_support_iff.mpr hne)
  have hor (n) (h : ¬coeff n p + coeff n q = 0) : coeff n p ≠ 0 ∨ coeff n q ≠ 0 := by
    by_cases hp : coeff n p = 0 <;> simp_all
  refine ⟨fun ⟨n, hn1, hn2⟩ ↦ ?_, ?_⟩
  · obtain (h | h) := hor n hn1
    · exact Or.inl ⟨n, by simp [h, hn2, hl n h]⟩
    · exact Or.inr ⟨n, by simp [h, hn2, hr n h]⟩
  · rintro (⟨n, hn, rfl⟩ | ⟨n, hn, rfl⟩)
    · exact ⟨n, by simp [hl n hn, hn]⟩
    · exact ⟨n, by simp [hr n hn, hn]⟩

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

Goal state before:
pp: case refine_1
R : Type u_2
S : Type u_3
σ : Type u_4
inst✝² : CommSemiring R
inst✝¹ : CommSemiring S
inst✝ : Module R S
M : Submodule R S
⊢ coeffsIn σ M ≤ Submodule.span R {x | ∃ m ∈ M, ∃ i, (monomial i) m = x}

pp: case refine_2
R : Type u_2
S : Type u_3
σ : Type u_4
inst✝² : CommSemiring R
inst✝¹ : CommSemiring S
inst✝ : Module R S
M : Submodule R S
⊢ {x | ∃ m ∈ M, ∃ i, (monomial i) m = x} ⊆ ↑(coeffsIn σ M)

Tactic:
· rintro p hp
    rw [p.as_sum]
    exact sum_mem fun i hi ↦ Submodule.subset_span ⟨_, hp i, _, rfl⟩

Goal state after:
case refine_2
R : Type u_2
S : Type u_3
σ : Type u_4
inst✝² : CommSemiring R
inst✝¹ : CommSemiring S
inst✝ : Module R S
M : Submodule R S
⊢ {x | ∃ m ∈ M, ∃ i, (monomial i) m = x} ⊆ ↑(coeffsIn σ M)
Module: Mathlib.Algebra.MvPolynomial.Basic

Goal state before:
pp: case refine_2
R : Type u_2
S : Type u_3
σ : Type u_4
inst✝² : CommSemiring R
inst✝¹ : CommSemiring S
inst✝ : Module R S
M : Submodule R S
⊢ {x | ∃ m ∈ M, ∃ i, (monomial i) m = x} ⊆ ↑(coeffsIn σ M)

Tactic:
rintro _ ⟨m, hm, s, n, rfl⟩ i
    simp
    split <;> simp [hm]

Goal state after:
Module: Mathlib.Algebra.MvPolynomial.Variables

Goal state before:
pp: R : Type u
σ : Type u_1
r : R
s : σ →₀ ℕ
inst✝ : CommSemiring R
h : r ≠ 0
⊢ ((monomial s) r).vars = s.support

Tactic:
by
  classical rw [vars_def, degrees_monomial_eq _ _ h, Finsupp.toFinset_toMultiset]

Goal state after: