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

Goal state before:
pp: case inl_add_inr
S : Type u_1
R : Type u_2
A : Type u_3
inst✝¹² : CommSemiring S
inst✝¹¹ : CommSemiring R
inst✝¹⁰ : NonUnitalSemiring A
inst✝⁹ : Module R A
inst✝⁸ : SMulCommClass R A A
inst✝⁷ : IsScalarTower R A A
B : Type u_4
inst✝⁶ : Semiring B
inst✝⁵ : Algebra S B
inst✝⁴ : Algebra S R
inst✝³ : DistribMulAction S A
inst✝² : IsScalarTower S R A
F : Type u_6
inst✝¹ : FunLike F (Unitization R A) B
inst✝ : AlgHomClass F S (Unitization R A) B
φ ψ : F
h : ∀ (a : A), φ ↑a = ψ ↑a
h' : ∀ (r : R), φ ((algebraMap R (Unitization R A)) r) = ψ ((algebraMap R (Unitization R A)) r)
r✝ : R
a✝ : A
⊢ φ (inl r✝ + ↑a✝) = ψ (inl r✝ + ↑a✝)

Tactic:
simp only [map_add, ← algebraMap_eq_inl, h, h']

Goal state after:
Module: Mathlib.RingTheory.TensorProduct.Maps

Goal state before:
pp: R : Type uR
A : Type uA
B : Type uB
inst✝⁴ : CommSemiring R
inst✝³ : Semiring A
inst✝² : Algebra R A
inst✝¹ : Semiring B
inst✝ : Algebra R B
h : Function.Bijective ⇑(algebraMap R A)
⊢ Function.Bijective ⇑includeRight

Tactic:
rw [← Function.Bijective.of_comp_iff' (TensorProduct.comm R A B).bijective]

Goal state after:
R : Type uR
A : Type uA
B : Type uB
inst✝⁴ : CommSemiring R
inst✝³ : Semiring A
inst✝² : Algebra R A
inst✝¹ : Semiring B
inst✝ : Algebra R B
h : Function.Bijective ⇑(algebraMap R A)
⊢ Function.Bijective (⇑(TensorProduct.comm R A B) ∘ ⇑includeRight)
Module: Mathlib.RingTheory.TensorProduct.Maps

Goal state before:
pp: R : Type uR
R' : Type u_1
S : Type uS
T : Type u_2
A : Type uA
B : Type uB
C : Type uC
D : Type uD
E : Type uE
F : Type uF
inst✝⁷ : CommSemiring R
inst✝⁶ : Semiring A
inst✝⁵ : Semiring B
inst✝⁴ : CommSemiring S
inst✝³ : Algebra R A
inst✝² : Algebra R B
inst✝¹ : Algebra R S
f : A →ₐ[R] S
g : B →ₐ[R] S
inst✝ : CompatibleSMul R S S S
x✝ : S ⊗[R] S
x y : S
⊢ (x * y) ⊗ₜ[R] 1 = x ⊗ₜ[R] y

Tactic:
rw [mul_comm, ← smul_eq_mul, smul_tmul, smul_eq_mul, mul_one]

Goal state after:
Module: Mathlib.Algebra.Algebra.Subalgebra.Directed

Goal state before:
pp: R : Type u_1
A : Type u_2
B : Type u_3
inst✝⁵ : CommSemiring R
inst✝⁴ : Semiring A
inst✝³ : Algebra R A
inst✝² : Semiring B
inst✝¹ : Algebra R B
S : Subalgebra R A
ι : Type u_4
inst✝ : Nonempty ι
K : ι → Subalgebra R A
dir : Directed (fun x1 x2 ↦ x1 ≤ x2) K
f : (i : ι) → ↥(K i) →ₐ[R] B
hf : ∀ (i j : ι) (h : K i ≤ K j), f i = (f j).comp (inclusion h)
T : Subalgebra R A
hT : T ≤ iSup K
compat : ∀ (i j : ι) (x : A) (hxi : x ∈ ↑(K i)) (hxj : x ∈ ↑(K j)), (f i) ⟨x, hxi⟩ = (f j) ⟨x, hxj⟩ :=
  iSupLift._proof_2 K dir f hf
⊢ Set.iUnionLift (fun i ↦ ↑(K i)) (fun i x ↦ (f i) x) compat ↑(iSup K) ⋯ 0 = 0

Tactic:
dsimp
        exact Set.iUnionLift_const _ (fun i : ι => (0 : K i)) (fun _ => rfl) _ (by simp)

Goal state after:
Module: Mathlib.Algebra.Algebra.Subalgebra.Centralizer

Goal state before:
pp: case mpr
R : Type u_1
inst✝⁵ : CommSemiring R
A : Type u_2
inst✝⁴ : Semiring A
inst✝³ : Algebra R A
B : Type u_3
inst✝² : Semiring B
inst✝¹ : Algebra R B
S : Set A
inst✝ : Module.Free R B
w : ↥(centralizer R S) ⊗[R] B
x : A
hx : x ∈ S
⊢ includeLeft x * (Algebra.TensorProduct.map (centralizer R S).val (AlgHom.id R B)).toRingHom w =
    (Algebra.TensorProduct.map (centralizer R S).val (AlgHom.id R B)).toRingHom w * includeLeft x

Tactic:
induction w using TensorProduct.induction_on with

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

Goal state before:
pp: R : Type u
M : Type v
inst✝³ : Ring R
inst✝² : AddCommGroup M
inst✝¹ : Module R M
inst✝ : Nontrivial R
M' : Submodule R M
⊢ Module.rank R (M ⧸ M') + Module.rank R ↥M' ≤ Module.rank R M

Tactic:
conv_lhs => simp only [Module.rank_def]

Goal state after:
R : Type u
M : Type v
inst✝³ : Ring R
inst✝² : AddCommGroup M
inst✝¹ : Module R M
inst✝ : Nontrivial R
M' : Submodule R M
⊢ (⨆ ι, #↑↑ι) + ⨆ ι, #↑↑ι ≤ Module.rank R M
Module: Mathlib.Algebra.Order.Star.Basic

Goal state before:
pp: F : Type u_6
E : Type u_7
R : Type u_8
inst✝¹⁰ : AddCommGroup E
inst✝⁹ : PartialOrder E
inst✝⁸ : StarAddMonoid E
inst✝⁷ : NonUnitalRing R
inst✝⁶ : PartialOrder R
inst✝⁵ : StarRing R
inst✝⁴ : StarOrderedRing R
inst✝³ : SelfAdjointDecompose E
inst✝² : FunLike F E R
inst✝¹ : OrderHomClass F E R
inst✝ : AddMonoidHomClass F E R
a : E
ha : IsSelfAdjoint a
f : F
⊢ IsSelfAdjoint (f a)

Tactic:
obtain ⟨b, c, hb, hc, rfl⟩ := ha.exists_nonneg_sub_nonneg
  have h₁ := OrderHomClass.mono f hb
  have h₂ := OrderHomClass.mono f hc
  cfc_tac

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

Goal state before:
pp: R : Type u
M M₁ : Type v
inst✝⁵ : Semiring R
inst✝⁴ : AddCommMonoid M
inst✝³ : AddCommMonoid M₁
inst✝² : Module R M
inst✝¹ : Module R M₁
inst✝ : Nontrivial R
⊢ Module.rank R M + Module.rank R M₁ ≤ Module.rank R (M × M₁)

Tactic:
conv_lhs => simp only [Module.rank_def]

Goal state after:
R : Type u
M M₁ : Type v
inst✝⁵ : Semiring R
inst✝⁴ : AddCommMonoid M
inst✝³ : AddCommMonoid M₁
inst✝² : Module R M
inst✝¹ : Module R M₁
inst✝ : Nontrivial R
⊢ (⨆ ι, #↑↑ι) + ⨆ ι, #↑↑ι ≤ Module.rank R (M × M₁)
Module: Mathlib.Algebra.Algebra.Subalgebra.Centralizer

Goal state before:
pp: R : Type u_1
inst✝⁵ : CommSemiring R
A : Type u_2
inst✝⁴ : Semiring A
inst✝³ : Algebra R A
B : Type u_3
inst✝² : Semiring B
inst✝¹ : Algebra R B
inst✝ : Module.Free R A
⊢ centralizer R ↑includeRight.range = (Algebra.TensorProduct.map (AlgHom.id R A) (centralizer R ↑⊤).val).range

Tactic:
← centralizer_coe_map_includeRight_eq_center_tensorProduct R A B ⊤

Goal state after:
R : Type u_1
inst✝⁵ : CommSemiring R
A : Type u_2
inst✝⁴ : Semiring A
inst✝³ : Algebra R A
B : Type u_3
inst✝² : Semiring B
inst✝¹ : Algebra R B
inst✝ : Module.Free R A
⊢ centralizer R ↑includeRight.range = centralizer R ↑(map includeRight ⊤)
Module: Mathlib.LinearAlgebra.Dimension.Finite

Goal state before:
pp: case hbc
R : Type u
M : Type v
inst✝⁴ : Semiring R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
inst✝¹ : StrongRankCondition R
ι : Type w
inst✝ : Module.Finite R M
v : ι → M
h : LinearIndependent R v
⊢ lift.{w, v} (Module.rank R M) < lift.{v, w} ℵ₀

Tactic:
← finrank_eq_rank,

Goal state after:
case hbc
R : Type u
M : Type v
inst✝⁴ : Semiring R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
inst✝¹ : StrongRankCondition R
ι : Type w
inst✝ : Module.Finite R M
v : ι → M
h : LinearIndependent R v
⊢ lift.{w, v} ↑(finrank R M) < lift.{v, w} ℵ₀
Module: Mathlib.LinearAlgebra.Basis.VectorSpace

Goal state before:
pp: case neg
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
s : Set V := ⇑f.ker.subtype '' Set.range ⇑b₁
hs : span K s = f.ker
n : Set V := insert v s
H₁ : LinearIndepOn K _root_.id n
H₂ : ⊤ ≤ span K n
b : Basis (↑n) K V := Basis.mk H₁ ⋯
i : ↑n := ⟨v, ⋯⟩
hi : b i = v
j : ↑n
h : ¬i = j
⊢ b j ∈ span K s

Tactic:
Basis.coe_mk

Goal state after:
case neg
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
s : Set V := ⇑f.ker.subtype '' Set.range ⇑b₁
hs : span K s = f.ker
n : Set V := insert v s
H₁ : LinearIndepOn K _root_.id n
H₂ : ⊤ ≤ span K n
b : Basis (↑n) K V := Basis.mk H₁ ⋯
i : ↑n := ⟨v, ⋯⟩
hi : b i = v
j : ↑n
h : ¬i = j
⊢ _root_.id ↑j ∈ span K s
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
⊢ ⊥ = ⊤

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

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
inst✝¹ : StrongRankCondition R
S : Submodule R M
inst✝ : Module.Finite R ↥S
⊢ finrank R ↥S = 0 ↔ Module.rank R ↥S = 0

Tactic:
← finrank_eq_rank,

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
inst✝¹ : StrongRankCondition R
S : Submodule R M
inst✝ : Module.Finite R ↥S
⊢ finrank R ↥S = 0 ↔ ↑(finrank R ↥S) = 0
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
ι : Type u_1
inst✝ : IsEmpty ι
hV : Module.rank K V = 0
⊢ Subsingleton V

Tactic:
obtain ⟨_, b⟩ := Module.Free.exists_basis (R := K) (M := V)
    have := mk_eq_zero_iff.1 (hV ▸ b.mk_eq_rank'')
    exact b.repr.toEquiv.subsingleton

Goal state after:
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
hinj : Injective ⇑f
h : Module.rank K ↥f.range = Module.rank K V
⊢ Surjective ⇑f

Tactic:
← finrank_eq_rank,

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
hinj : Injective ⇑f
h : ↑(finrank K ↥f.range) = Module.rank K V
⊢ Surjective ⇑f
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
hinj : Injective ⇑f
h : ↑(finrank K ↥f.range) = Module.rank K V
⊢ Surjective ⇑f

Tactic:
← finrank_eq_rank,

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
hinj : Injective ⇑f
h : ↑(finrank K ↥f.range) = ↑(finrank K V)
⊢ Surjective ⇑f
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 g : V →ₗ[K] V
h : Commute f g
h' : Disjoint f.ker g.ker
⊢ (f ∘ₗ g).ker = f.ker ⊔ g.ker

Tactic:
suffices ∀ x, f x = 0 → f (g x) = 0 by rw [ker_comp, comap_eq_sup_ker_of_disjoint _ h']; simpa
  intro x hx
  rw [← comp_apply, ← Module.End.mul_eq_comp, h.eq, Module.End.mul_apply, hx, map_zero]

Goal state after:
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
inst✝ : Module.Finite K V
⊢ finrank K V ≤ 1 ↔ Module.rank K V ≤ 1

Tactic:
← finrank_eq_rank,

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
inst✝ : Module.Finite K V
⊢ finrank K V ≤ 1 ↔ ↑(finrank K V) ≤ 1
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
W : Submodule K V
inst✝¹ : Free K ↥W
inst✝ : Module.Finite K ↥W
⊢ finrank K ↥W ≤ 1 ↔ Module.rank K ↥W ≤ 1

Tactic:
← finrank_eq_rank,

Goal state after:
K : Type u
V : Type v
inst✝⁵ : Ring K
inst✝⁴ : StrongRankCondition K
inst✝³ : AddCommGroup V
inst✝² : Module K V
W : Submodule K V
inst✝¹ : Free K ↥W
inst✝ : Module.Finite K ↥W
⊢ finrank K ↥W ≤ 1 ↔ ↑(finrank K ↥W) ≤ 1
Module: Mathlib.LinearAlgebra.LinearPMap

Goal state before:
pp: case h'
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
f g : E →ₛₗ.[σ] F
x : E
hf✝ : x ∈ (f - g).domain
h : x ∈ (f + -g).domain
⊢ ↑(f - g) ⟨x, hf✝⟩ = ↑(f + -g) ⟨x, h⟩

Tactic:
simp [sub_apply, add_apply, neg_apply, ← sub_eq_add_neg]

Goal state after:
Module: Mathlib.LinearAlgebra.LinearPMap

Goal state before:
pp: case mpr.mk
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
fst✝ : E
snd✝ : F
hx' : (fst✝, snd✝) ∈ f.graph
h : (LinearMap.id.prodMap (z • LinearMap.id)) (fst✝, snd✝) = (x_fst, x_snd)
⊢ (x_fst, x_snd) ∈ (z • f).graph

Tactic:
simp only [LinearMap.prodMap_apply, LinearMap.id_coe, id, LinearMap.smul_apply,
    Prod.mk_inj] at h

Goal state after:
case mpr.mk
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
fst✝ : E
snd✝ : F
hx' : (fst✝, snd✝) ∈ f.graph
h : fst✝ = x_fst ∧ z • snd✝ = x_snd
⊢ (x_fst, x_snd) ∈ (z • f).graph
Module: Mathlib.Algebra.CharP.Defs

Goal state before:
pp: R : Type u_1
inst✝¹ : Ring R
inst✝ : IsDomain R
q : ℕ
h✝ : ExpChar R q
⊢ ExpChar R (ringExpChar R)

Tactic:
ringExpChar.eq R q

Goal state after:
R : Type u_1
inst✝¹ : Ring R
inst✝ : IsDomain R
q : ℕ
h✝ : ExpChar R q
⊢ ExpChar R q
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
g : Submodule R (E × F)
hg : ∀ x ∈ g, x.1 = 0 → x.2 = 0
x_fst : E
x_snd : F
hx : (x_fst, x_snd) ∈ g
⊢ ∃ y, ↑y = (x_fst, x_snd).1 ∧ ↑g.toLinearPMap y = (x_fst, x_snd).2

Tactic:
have hx_fst : x_fst ∈ g.map (LinearMap.fst R E F) := by
    simp only [mem_map, LinearMap.fst_apply, Prod.exists, exists_and_right, exists_eq_right]
    exact ⟨x_snd, hx⟩

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
g : Submodule R (E × F)
hg : ∀ x ∈ g, x.1 = 0 → x.2 = 0
x_fst : E
x_snd : F
hx : (x_fst, x_snd) ∈ g
hx_fst : x_fst ∈ map (LinearMap.fst R E F) g
⊢ ∃ y, ↑y = (x_fst, x_snd).1 ∧ ↑g.toLinearPMap y = (x_fst, x_snd).2
Module: Mathlib.Order.Filter.Extr

Goal state before:
pp: α : Type u
β : Type u_1
inst✝¹ : LinearOrder α
inst✝ : Preorder β
a b c : α
f : α → β
h₀ : MonotoneOn f (Ioc a b)
h₁ : AntitoneOn f (Ico b c)
⊢ IsMaxOn f (Ioo a c) b

Tactic:
intro x hx
  by_cases! g₀ : x ≤ b
  · exact h₀ ⟨hx.1, g₀⟩ (right_mem_Ioc.2 (g₀.trans_lt' hx.1)) g₀
  · refine h₁ (left_mem_Ico.2 (g₀.trans hx.2)) ⟨g₀.le, hx.2⟩ g₀.le

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 = ⊥
y : ↥f.inverse.domain
x : ↥f.domain
hxy : ↑f x = ↑y
⊢ ↑f.inverse y = ↑x

Tactic:
have := mem_inverse_graph hf x
  grind

Goal state after:
Module: Mathlib.Algebra.Polynomial.Coeff

Goal state before:
pp: case h₀
R : Type u
inst✝ : Semiring R
r : R
n k : ℕ
⊢ ∀ b ∈ range (n + 1), b ≠ k → (X ^ b).coeff k * r ^ (n - b) * ↑(n.choose b) = 0

Tactic:
intro _ _ h

Goal state after:
case h₀
R : Type u
inst✝ : Semiring R
r : R
n k b✝ : ℕ
a✝ : b✝ ∈ range (n + 1)
h : b✝ ≠ k
⊢ (X ^ b✝).coeff k * r ^ (n - b✝) * ↑(n.choose b✝) = 0
Module: Mathlib.Algebra.Polynomial.Degree.Defs

Goal state before:
pp: case inr
R : Type u
inst✝ : Semiring R
p : R[X]
n : ℕ
hn : 0 < n
h : p ≠ 0
⊢ p.degree = ↑n ↔ p.natDegree = n

Tactic:
· exact degree_eq_iff_natDegree_eq h

Goal state after:
Module: Mathlib.Algebra.Polynomial.Coeff

Goal state before:
pp: S : Type u_1
inst✝ : CommRing S
d i : ℕ
⊢ (↑(d.choose i) - if i = d then 1 else 0) = if i < d then ↑(d.choose i) else 0

Tactic:
split_ifs

Goal state after:
case pos
S : Type u_1
inst✝ : CommRing S
d i : ℕ
h✝¹ : i = d
h✝ : i < d
⊢ ↑(d.choose i) - 1 = ↑(d.choose i)

case neg
S : Type u_1
inst✝ : CommRing S
d i : ℕ
h✝¹ : i = d
h✝ : ¬i < d
⊢ ↑(d.choose i) - 1 = 0

case pos
S : Type u_1
inst✝ : CommRing S
d i : ℕ
h✝¹ : ¬i = d
h✝ : i < d
⊢ ↑(d.choose i) - 0 = ↑(d.choose i)

case neg
S : Type u_1
inst✝ : CommRing S
d i : ℕ
h✝¹ : ¬i = d
h✝ : ¬i < d
⊢ ↑(d.choose i) - 0 = 0
Module: Mathlib.Algebra.Polynomial.Degree.Defs

Goal state before:
pp: R : Type u
inst✝ : Semiring R
a : R
m : ℕ
⊢ (if a = 0 then 0 else m) ≤ m

Tactic:
split_ifs

Goal state after:
case pos
R : Type u
inst✝ : Semiring R
a : R
m : ℕ
h✝ : a = 0
⊢ 0 ≤ m

case neg
R : Type u
inst✝ : Semiring R
a : R
m : ℕ
h✝ : ¬a = 0
⊢ m ≤ m
Module: Mathlib.Algebra.MonoidAlgebra.Degree

Goal state before:
pp: case refine_1
R : Type u_7
A : Type u_8
B : Type u_9
inst✝⁶ : CommSemiring R
inst✝⁵ : AddCommMonoid A
inst✝⁴ : AddCommMonoid B
inst✝³ : SemilatticeSup B
inst✝² : OrderBot B
inst✝¹ : AddLeftMono B
inst✝ : AddRightMono B
D : A → B
hzero : D 0 = 0
hadd : ∀ (a1 a2 : A), D (a1 + a2) = D a1 + D a2
ι : Type u_10
s : Finset ι
f : ι → R[A]
⊢ (if 1 = 0 then ⊥ else D 0) ≤ 0

Tactic:
split_ifs

Goal state after:
case pos
R : Type u_7
A : Type u_8
B : Type u_9
inst✝⁶ : CommSemiring R
inst✝⁵ : AddCommMonoid A
inst✝⁴ : AddCommMonoid B
inst✝³ : SemilatticeSup B
inst✝² : OrderBot B
inst✝¹ : AddLeftMono B
inst✝ : AddRightMono B
D : A → B
hzero : D 0 = 0
hadd : ∀ (a1 a2 : A), D (a1 + a2) = D a1 + D a2
ι : Type u_10
s : Finset ι
f : ι → R[A]
h✝ : 1 = 0
⊢ ⊥ ≤ 0

case neg
R : Type u_7
A : Type u_8
B : Type u_9
inst✝⁶ : CommSemiring R
inst✝⁵ : AddCommMonoid A
inst✝⁴ : AddCommMonoid B
inst✝³ : SemilatticeSup B
inst✝² : OrderBot B
inst✝¹ : AddLeftMono B
inst✝ : AddRightMono B
D : A → B
hzero : D 0 = 0
hadd : ∀ (a1 a2 : A), D (a1 + a2) = D a1 + D a2
ι : Type u_10
s : Finset ι
f : ι → R[A]
h✝ : ¬1 = 0
⊢ D 0 ≤ 0
Module: Mathlib.Algebra.Polynomial.Degree.Defs

Goal state before:
pp: R : Type u
inst✝ : Semiring R
p : R[X]
n : ℕ
a : R
⊢ (if a = 0 then p.support.erase n else insert n p.support).max ≤ max p.degree ↑n

Tactic:
split_ifs

Goal state after:
case pos
R : Type u
inst✝ : Semiring R
p : R[X]
n : ℕ
a : R
h✝ : a = 0
⊢ (p.support.erase n).max ≤ max p.degree ↑n

case neg
R : Type u
inst✝ : Semiring R
p : R[X]
n : ℕ
a : R
h✝ : ¬a = 0
⊢ (insert n p.support).max ≤ max p.degree ↑n
Module: Mathlib.Algebra.MonoidAlgebra.Degree

Goal state before:
pp: case refine_2
R : Type u_7
A : Type u_8
B : Type u_9
inst✝⁶ : CommSemiring R
inst✝⁵ : AddCommMonoid A
inst✝⁴ : AddCommMonoid B
inst✝³ : SemilatticeSup B
inst✝² : OrderBot B
inst✝¹ : AddLeftMono B
inst✝ : AddRightMono B
D : A → B
hzero : D 0 = 0
hadd : ∀ (a1 a2 : A), D (a1 + a2) = D a1 + D a2
ι : Type u_10
s✝ : Finset ι
f : ι → R[A]
i : ι
s : Finset ι
his : i ∉ s
ih : supDegree D (∏ i ∈ s, f i) ≤ ∑ i ∈ s, supDegree D (f i)
⊢ supDegree D (f i * ∏ x ∈ s, f x) ≤ supDegree D (f i) + ∑ x ∈ s, supDegree D (f x)

Tactic:
exact (supDegree_mul_le hadd).trans (by gcongr)

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

Goal state before:
pp: R : Type u
inst✝ : Semiring R
p q : R[X]
⊢ (p * q).degree ≤ p.degree + q.degree

Tactic:
simpa [degree, ← support_toFinsupp] using! AddMonoidAlgebra.sup_support_coeff_mul_le (by simp) ..

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

Goal state before:
pp: case hb
R : Type u_1
A : Type u_3
B : Type u_5
inst✝⁶ : Semiring R
inst✝⁵ : LinearOrder B
inst✝⁴ : OrderBot B
p q : R[A]
D : A → B
inst✝³ : AddZeroClass A
inst✝² : Add B
inst✝¹ : AddLeftStrictMono B
inst✝ : AddRightStrictMono B
hD : Function.Injective D
hadd : ∀ (a1 a2 : A), D (a1 + a2) = D a1 + D a2
hpq : leadingCoeff D p * leadingCoeff D q ≠ 0
hp : p ≠ 0
hq : q ≠ 0
⊢ supDegree D p + supDegree D q ∈ ↑{ carrier := Set.range D, add_mem' := ?hb✝ }

pp: case hb
R : Type u_1
A : Type u_3
B : Type u_5
inst✝⁶ : Semiring R
inst✝⁵ : LinearOrder B
inst✝⁴ : OrderBot B
p q : R[A]
D : A → B
inst✝³ : AddZeroClass A
inst✝² : Add B
inst✝¹ : AddLeftStrictMono B
inst✝ : AddRightStrictMono B
hD : Function.Injective D
hadd : ∀ (a1 a2 : A), D (a1 + a2) = D a1 + D a2
hpq : leadingCoeff D p * leadingCoeff D q ≠ 0
hp : p ≠ 0
hq : q ≠ 0
⊢ ∀ {a b : B}, a ∈ Set.range D → b ∈ Set.range D → a + b ∈ Set.range D

Tactic:
← AddHom.srange_mk _ hadd,

Goal state after:
case hb
R : Type u_1
A : Type u_3
B : Type u_5
inst✝⁶ : Semiring R
inst✝⁵ : LinearOrder B
inst✝⁴ : OrderBot B
p q : R[A]
D : A → B
inst✝³ : AddZeroClass A
inst✝² : Add B
inst✝¹ : AddLeftStrictMono B
inst✝ : AddRightStrictMono B
hD : Function.Injective D
hadd : ∀ (a1 a2 : A), D (a1 + a2) = D a1 + D a2
hpq : leadingCoeff D p * leadingCoeff D q ≠ 0
hp : p ≠ 0
hq : q ≠ 0
⊢ supDegree D p + supDegree D q ∈ ↑{ toFun := D, map_add' := hadd }.srange

case hb
R : Type u_1
A : Type u_3
B : Type u_5
inst✝⁶ : Semiring R
inst✝⁵ : LinearOrder B
inst✝⁴ : OrderBot B
p q : R[A]
D : A → B
inst✝³ : AddZeroClass A
inst✝² : Add B
inst✝¹ : AddLeftStrictMono B
inst✝ : AddRightStrictMono B
hD : Function.Injective D
hadd : ∀ (a1 a2 : A), D (a1 + a2) = D a1 + D a2
hpq : leadingCoeff D p * leadingCoeff D q ≠ 0
hp : p ≠ 0
hq : q ≠ 0
⊢ ∀ {a b : B}, a ∈ Set.range D → b ∈ Set.range D → a + b ∈ Set.range D
Module: Mathlib.Algebra.Polynomial.Degree.Operations

Goal state before:
pp: R : Type u_1
inst✝ : Semiring R
n : ℕ
a✝ : Nontrivial R
⊢ (X ^ n).natDegree ≤ n

Tactic:
rw [Polynomial.natDegree_X_pow]

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

Goal state before:
pp: R : Type u
a : R
inst✝ : Ring R
p : R[X]
hp : 0 < p.degree
⊢ (p + C (-a)).degree = p.degree

Tactic:
degree_add_C hp

Goal state after:
R : Type u
a : R
inst✝ : Ring R
p : R[X]
hp : 0 < p.degree
⊢ p.degree = p.degree
Module: Mathlib.Algebra.Polynomial.Eval.Degree

Goal state before:
pp: case h₀
R : Type u
inst✝ : Semiring R
p q : R[X]
hqd0 : q.natDegree ≠ 0
⊢ ∀ b ∈ p.support, b ≠ p.natDegree → (fun a b ↦ (C b * q ^ a).coeff (p.natDegree * q.natDegree)) b (p.coeff b) = 0

pp: case h₁
R : Type u
inst✝ : Semiring R
p q : R[X]
hqd0 : q.natDegree ≠ 0
⊢ p.natDegree ∉ p.support →
    (fun a b ↦ (C b * q ^ a).coeff (p.natDegree * q.natDegree)) p.natDegree (p.coeff p.natDegree) = 0

pp: case h₂
R : Type u
inst✝ : Semiring R
p q : R[X]
hqd0 : q.natDegree ≠ 0
⊢ (fun a b ↦ (C b * q ^ a).coeff (p.natDegree * q.natDegree)) p.natDegree (p.coeff p.natDegree) =
    p.leadingCoeff * q.leadingCoeff ^ p.natDegree

Tactic:
case h₂ =>
    simp only [coeff_natDegree, coeff_C_mul, coeff_pow_mul_natDegree]

Goal state after:
case h₀
R : Type u
inst✝ : Semiring R
p q : R[X]
hqd0 : q.natDegree ≠ 0
⊢ ∀ b ∈ p.support, b ≠ p.natDegree → (fun a b ↦ (C b * q ^ a).coeff (p.natDegree * q.natDegree)) b (p.coeff b) = 0

case h₁
R : Type u
inst✝ : Semiring R
p q : R[X]
hqd0 : q.natDegree ≠ 0
⊢ p.natDegree ∉ p.support →
    (fun a b ↦ (C b * q ^ a).coeff (p.natDegree * q.natDegree)) p.natDegree (p.coeff p.natDegree) = 0
Module: Mathlib.Data.Finsupp.Antidiagonal

Goal state before:
pp: α : Type u
inst✝ : DecidableEq α
a : α
n : ℕ
⊢ antidiagonal (single a n) =
    map ({ toFun := single a, inj' := ⋯ }.prodMap { toFun := single a, inj' := ⋯ }) (antidiagonal n)

Tactic:
ext ⟨x, y⟩
  simp only [mem_antidiagonal, mem_map, mem_antidiagonal, Function.Embedding.coe_prodMap,
    Function.Embedding.coeFn_mk, Prod.map_apply, Prod.mk.injEq, Prod.exists]
  constructor
  · intro h
    refine ⟨x a, y a, DFunLike.congr_fun h a |>.trans single_eq_same, ?_⟩
    simp_rw [DFunLike.ext_iff, ← forall_and]
    intro i
    replace h := DFunLike.congr_fun h i
    simp_rw [single_apply, Finsupp.add_apply] at h ⊢
    obtain rfl | hai := Decidable.eq_or_ne a i
    · exact ⟨if_pos rfl, if_pos rfl⟩
    · simp_rw [if_neg hai, add_eq_zero] at h ⊢
      exact h.imp Eq.symm Eq.symm
  · rintro ⟨a, b, rfl, rfl, rfl⟩
    exact (single_add _ _ _).symm

Goal state after:
Module: Mathlib.Data.Finsupp.Order

Goal state before:
pp: ι : Type u_1
κ : Type u_2
α : Type u_3
inst✝² : Zero α
inst✝¹ : LE α
inst✝ : Std.Refl fun x1 x2 ↦ x1 ≤ x2
f : ι ↪ κ
g₁ g₂ : ι →₀ α
⊢ embDomain f g₁ ≤ embDomain f g₂ ↔ g₁ ≤ g₂

Tactic:
by
  constructor
  · rw [Finsupp.le_def]
    intro h' x
    simpa [Finsupp.embDomain_apply] using h' (f x)
  intro h
  simp [Finsupp.le_def, embDomain_apply, apply_dite₂, Finsupp.le_def.mp h]

Goal state after: