mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.RingTheory.Localization.Basic

Goal state before:
pp: R : Type u_1
inst✝⁸ : CommSemiring R
M N : Submonoid R
S : Type u_2
inst✝⁷ : CommSemiring S
inst✝⁶ : Algebra R S
P : Type u_3
inst✝⁵ : CommSemiring P
Rₘ : Type u_4
Sₘ : Type u_5
inst✝⁴ : CommSemiring Rₘ
inst✝³ : CommSemiring Sₘ
inst✝² : Algebra R Rₘ
inst✝¹ : IsLocalization M Rₘ
inst✝ : Algebra S Sₘ
i : IsLocalization (Algebra.algebraMapSubmonoid S M) Sₘ
⊢ IsLocalization (Algebra.algebraMapSubmonoid R M) Rₘ

Tactic:
by
  simpa

Goal state after:
Module: Mathlib.Algebra.Algebra.Epi

Goal state before:
pp: case add
R : Type u_1
A : Type u_2
inst✝² : CommSemiring R
inst✝¹ : Semiring A
inst✝ : Algebra R A
h : ∀ (a : A), 1 ⊗ₜ[R] a = a ⊗ₜ[R] 1
x y : A ⊗[R] A
hxy : (lift (LinearMap.mul R A)) x = (lift (LinearMap.mul R A)) y
u v : A ⊗[R] A
hu : ∃ a, u = a ⊗ₜ[R] 1
hv : ∃ a, v = a ⊗ₜ[R] 1
⊢ ∃ a, u + v = a ⊗ₜ[R] 1

Tactic:
obtain ⟨u, rfl⟩ := hu

Goal state after:
case add
R : Type u_1
A : Type u_2
inst✝² : CommSemiring R
inst✝¹ : Semiring A
inst✝ : Algebra R A
h : ∀ (a : A), 1 ⊗ₜ[R] a = a ⊗ₜ[R] 1
x y : A ⊗[R] A
hxy : (lift (LinearMap.mul R A)) x = (lift (LinearMap.mul R A)) y
v : A ⊗[R] A
hv : ∃ a, v = a ⊗ₜ[R] 1
u : A
⊢ ∃ a, u ⊗ₜ[R] 1 + v = a ⊗ₜ[R] 1
Module: Mathlib.Algebra.Algebra.Epi

Goal state before:
pp: R : Type u_1
A : Type u_2
inst✝² : CommSemiring R
inst✝¹ : Semiring A
inst✝ : Algebra R A
h : ∀ (a : A), 1 ⊗ₜ[R] a = a ⊗ₜ[R] 1
x y : A ⊗[R] A
hxy : (lift (LinearMap.mul R A)) x = (lift (LinearMap.mul R A)) y
h' : ∀ (x : A ⊗[R] A), ∃ a, x = a ⊗ₜ[R] 1
⊢ x = y

Tactic:
obtain ⟨a, rfl⟩ := h' x

Goal state after:
R : Type u_1
A : Type u_2
inst✝² : CommSemiring R
inst✝¹ : Semiring A
inst✝ : Algebra R A
h : ∀ (a : A), 1 ⊗ₜ[R] a = a ⊗ₜ[R] 1
y : A ⊗[R] A
h' : ∀ (x : A ⊗[R] A), ∃ a, x = a ⊗ₜ[R] 1
a : A
hxy : (lift (LinearMap.mul R A)) (a ⊗ₜ[R] 1) = (lift (LinearMap.mul R A)) y
⊢ a ⊗ₜ[R] 1 = y
Module: Mathlib.Algebra.Algebra.Epi

Goal state before:
pp: R : Type u_1
A : Type u_2
inst✝² : CommSemiring R
inst✝¹ : Semiring A
inst✝ : Algebra R A
h : Surjective ⇑(algebraMap R A)
r : R
⊢ 1 ⊗ₜ[R] (algebraMap R A) r = (algebraMap R A) r ⊗ₜ[R] 1

Tactic:
rw [algebraMap_eq_smul_one, smul_tmul]

Goal state after:
Module: Mathlib.Algebra.Algebra.TransferInstance

Goal state before:
pp: R : Type u_1
α : Type u_2
β : Type u_3
inst✝² : CommSemiring R
e✝ e : α ≃ β
inst✝¹ : Semiring β
inst✝ : Algebra R β
b : β
this✝ : Semiring α := e.semiring
this : Algebra R α := Equiv.algebra R e
⊢ Sort ?u.18

Tactic:
exact (algEquiv R e).symm b = e.symm b

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

Goal state before:
pp: α : Type u_1
inst✝¹ : Group α
inst✝ : StarMul α
s : Set α
⊢ s⁻¹⋆ = s⋆⁻¹

Tactic:
ext
  simp only [mem_star, mem_inv, star_inv]

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

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✝³ : AddCommGroupWithOne A
inst✝² : Module R A
inst✝¹ : AddCommMonoidWithOne B
inst✝ : Module R B
n : ℕ
⊢ ↑(Int.negSucc n) ⊗ₜ[R] 1 = -↑(n + 1)

Tactic:
simp [natCast_def, add_tmul, neg_tmul, one_def]

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

Goal state before:
pp: R✝ : Type u_1
A✝ : Type u_2
B✝ : Type u_3
inst✝¹⁷ : CommSemiring R✝
inst✝¹⁶ : NonUnitalNonAssocSemiring A✝
inst✝¹⁵ : NonUnitalNonAssocSemiring B✝
inst✝¹⁴ : Module R✝ A✝
inst✝¹³ : Module R✝ B✝
inst✝¹² : SMulCommClass R✝ A✝ A✝
inst✝¹¹ : SMulCommClass R✝ B✝ B✝
inst✝¹⁰ : IsScalarTower R✝ A✝ A✝
inst✝⁹ : IsScalarTower R✝ B✝ B✝
R : Type u_4
S : Type u_5
A : Type u_6
B : Type u_7
inst✝⁸ : CommSemiring R
inst✝⁷ : CommSemiring S
inst✝⁶ : Semiring A
inst✝⁵ : Semiring B
inst✝⁴ : Algebra R A
inst✝³ : Algebra S B
inst✝² : Algebra R S
inst✝¹ : Algebra R B
inst✝ : IsScalarTower R S B
f : A →ₐ[R] B
⊢ (LinearMap.liftBaseChange S ↑f) 1 = 1

Tactic:
simp [Algebra.TensorProduct.one_def]

Goal state after:
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✝²⁵ : CommSemiring S
inst✝²⁴ : Algebra R S
inst✝²³ : Semiring A
inst✝²² : Algebra R A
inst✝²¹ : Algebra S A
inst✝²⁰ : IsScalarTower R S A
inst✝¹⁹ : Semiring B
inst✝¹⁸ : Algebra R B
inst✝¹⁷ : Semiring C
inst✝¹⁶ : Algebra R C
inst✝¹⁵ : Algebra S C
inst✝¹⁴ : IsScalarTower R S C
inst✝¹³ : Semiring D
inst✝¹² : Algebra R D
inst✝¹¹ : Semiring E
inst✝¹⁰ : Algebra R E
inst✝⁹ : Algebra S E
inst✝⁸ : IsScalarTower R S E
inst✝⁷ : Semiring F
inst✝⁶ : Algebra R F
inst✝⁵ : CommSemiring T
inst✝⁴ : Algebra R T
inst✝³ : Algebra S T
inst✝² : Algebra T A
inst✝¹ : IsScalarTower R T A
inst✝ : IsScalarTower S T A
⊢ (AlgebraTensorModule.assoc R S T A C D) 1 = 1

Tactic:
simp [Algebra.TensorProduct.one_def]

Goal state after:
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✝³¹ : CommSemiring S
inst✝³⁰ : Algebra R S
inst✝²⁹ : Semiring A✝
inst✝²⁸ : Algebra R A✝
inst✝²⁷ : Algebra S A✝
inst✝²⁶ : IsScalarTower R S A✝
inst✝²⁵ : Semiring B✝
inst✝²⁴ : Algebra R B✝
inst✝²³ : Semiring C
inst✝²² : Algebra R C
inst✝²¹ : Algebra S C
inst✝²⁰ : IsScalarTower R S C
inst✝¹⁹ : Semiring D
inst✝¹⁸ : Algebra R D
inst✝¹⁷ : Semiring E
inst✝¹⁶ : Algebra R E
inst✝¹⁵ : Algebra S E
inst✝¹⁴ : IsScalarTower R S E
inst✝¹³ : Semiring F
inst✝¹² : Algebra R F
T : Type u_3
A : Type u_4
B : Type u_5
inst✝¹¹ : CommSemiring T
inst✝¹⁰ : CommSemiring A
inst✝⁹ : CommSemiring B
inst✝⁸ : Algebra R T
inst✝⁷ : Algebra R A
inst✝⁶ : Algebra R B
inst✝⁵ : Algebra T A
inst✝⁴ : IsScalarTower R T A
inst✝³ : Algebra S A
inst✝² : IsScalarTower R S A
inst✝¹ : Algebra S T
inst✝ : IsScalarTower S T A
⊢ (AlgebraTensorModule.cancelBaseChange R S T A B).symm 1 = 1

Tactic:
simp [Algebra.TensorProduct.one_def]

Goal state after:
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 : R
inst✝ : IsCancelAdd R
⊢ x < y ↔ ∃ p, p ≠ 0 ∧ p ∈ AddSubmonoid.closure (range fun s ↦ star s * s) ∧ y = x + p

Tactic:
lt_iff_le_and_ne,

Goal state after:
R : Type u_1
inst✝⁴ : NonUnitalSemiring R
inst✝³ : PartialOrder R
inst✝² : StarRing R
inst✝¹ : StarOrderedRing R
x y : R
inst✝ : IsCancelAdd R
⊢ x ≤ y ∧ x ≠ y ↔ ∃ p, p ≠ 0 ∧ p ∈ AddSubmonoid.closure (range fun s ↦ star s * s) ∧ y = x + p
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
⊢ ∀ (x y : ↥(iSup K)),
    Set.iUnionLift (fun i ↦ ↑(K i)) (fun i x ↦ (f i) x) compat ↑(iSup K) ⋯ (x * y) =
      Set.iUnionLift (fun i ↦ ↑(K i)) (fun i x ↦ (f i) x) compat ↑(iSup K) ⋯ x *
        Set.iUnionLift (fun i ↦ ↑(K i)) (fun i x ↦ (f i) x) compat ↑(iSup K) ⋯ y

Tactic:
by
        dsimp
        apply Set.iUnionLift_binary (coe_iSup_of_directed (K := K) dir) dir _ (fun _ => (· * ·))
        all_goals simp

Goal state after:
Module: Mathlib.Algebra.Order.Star.Basic

Goal state before:
pp: case pos
R : Type u_1
inst✝³ : NonUnitalSemiring R
inst✝² : PartialOrder R
inst✝¹ : StarRing R
inst✝ : StarOrderedRing R
x y : R
h : x = y
⊢ star x < star y ↔ x < y

Tactic:
simp [h]

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

Goal state before:
pp: R : Type u
M : Type v
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
n : ℕ
hn : ↑n ≤ Module.rank R M
h : ↑n = Module.rank R M
s : Set M
hs : LinearIndepOn R id s
hs' : #↑↑⟨s, hs⟩ = ↑n
this : Finite ↑s
val✝ : Fintype ↑s
⊢ s.toFinset.card = n

Tactic:
simpa using hs'

Goal state after:
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
x : ↑(ofVectorSpaceIndex K V)
⊢ (ofVectorSpace K V) x = ↑x

Tactic:
by
  unfold ofVectorSpace
  exact Basis.mk_apply _ _ _

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

Goal state before:
pp: case refine_2
K : Type u_3
V : Type u_4
inst✝² : DivisionRing K
inst✝¹ : AddCommGroup V
inst✝ : Module K V
v : V
hv : v ≠ 0
⊢ IsAtom (K ∙ v)

Tactic:
exact nonzero_span_atom v hv

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

Goal state before:
pp: case pos
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
⊢ f (b j) = (f (b i) • b.coord i) (b j)

Tactic:
simp [h]

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

Goal state before:
pp: R : Type u
M : Type v
inst✝³ : Semiring R
inst✝² : AddCommMonoid M
inst✝¹ : Module R M
inst✝ : Nontrivial R
⊢ finrank R ↥⊥ = 0

Tactic:
finrank_bot

Goal state after:
R : Type u
M : Type v
inst✝³ : Semiring R
inst✝² : AddCommMonoid M
inst✝¹ : Module R M
inst✝ : Nontrivial R
⊢ 0 = 0
Module: Mathlib.LinearAlgebra.Dimension.FreeAndStrongRankCondition

Goal state before:
pp: case mp
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

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

Goal state after:
case mp
K : Type u
V : Type v
inst✝⁴ : Ring K
inst✝³ : StrongRankCondition K
inst✝² : AddCommGroup V
inst✝¹ : Module K V
inst✝ : Free K V
t : Finset V
si : LinearIndepOn K id ↑t
⊢ ∃ s, s.card = t.card ∧ LinearIndependent K Subtype.val
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
h : finrank F ↥S = 1
inst✝ : Free F ↥S
⊢ Module.rank F ↥S ≤ 1

Tactic:
rw [finrank, toNat_eq_one] at h

Goal state after:
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
h : Module.rank F ↥S = 1
inst✝ : Free F ↥S
⊢ Module.rank F ↥S ≤ 1
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
inst✝ : Free F E
a✝ : Nontrivial E
h : finrank F E = 1
⊢ Function.Surjective ⇑(algebraMap F E)

Tactic:
rwa [Algebra.surjective_algebraMap_iff, eq_comm, Subalgebra.bot_eq_top_iff_finrank_eq_one]

Goal state after:
Module: Mathlib.Algebra.FreeAlgebra

Goal state before:
pp: R : Type u_1
X : Type u_2
inst✝ : CommSemiring R
⊢ ∀ (a b c : FreeAlgebra R X), (a + b) * c = a * c + b * c

Tactic:
by
    rintro ⟨⟩ ⟨⟩ ⟨⟩
    exact Quot.sound Rel.right_distrib

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

Goal state before:
pp: case a
K : Type u
V : Type v
inst✝² : DivisionRing K
inst✝¹ : AddCommGroup V
inst✝ : Module K V
f : End K V
k : ℕ
h : LinearMap.ker (f ^ k) = LinearMap.ker (f ^ k.succ)
m : ℕ
⊢ LinearMap.ker (f ^ (k + (m + 1))) ≤ LinearMap.ker (f ^ k)

Tactic:
· rw [ker_pow_constant h m, add_comm m 1, ← add_assoc, pow_add, pow_add f k m,
        Module.End.mul_eq_comp, Module.End.mul_eq_comp, LinearMap.ker_comp, LinearMap.ker_comp, h,
        Nat.add_one]

Goal state after:
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
h' : f + g = 0
x : E
this : f.domain = ⊤ ∧ g.domain = ⊤
⊢ x ∈ (-f).domain ↔ x ∈ g.domain

Tactic:
neg_domain,

Goal state after:
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
h' : f + g = 0
x : E
this : f.domain = ⊤ ∧ g.domain = ⊤
⊢ x ∈ f.domain ↔ x ∈ g.domain
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

Tactic:
simp [h]

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

Goal state before:
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:
simp [h]

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

Goal state before:
pp: k : Type u₁
G : Type u₂
inst✝² : Semiring k
inst✝¹ : Mul G
inst✝ : DecidableEq G
x : k[G]
r : k
a : G
⊢ image₂ (fun x1 x2 ↦ x1 * x2) x.coeff.support {a} ⊆ image (fun x ↦ x * a) x.coeff.support

Tactic:
image₂_singleton_right

Goal state after:
k : Type u₁
G : Type u₂
inst✝² : Semiring k
inst✝¹ : Mul G
inst✝ : DecidableEq G
x : k[G]
r : k
a : G
⊢ image (fun a_1 ↦ a_1 * a) x.coeff.support ⊆ image (fun x ↦ x * a) x.coeff.support
Module: Mathlib.LinearAlgebra.LinearPMap

Goal state before:
pp: case w.refine_2
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
c : R
x : ↥(sSup (domain '' c✝))
⊢ f (c • x) = σ c • f x

Tactic:
f_eq (P x).1 (c • x) (c • ⟨x, (P x).2⟩) rfl,

Goal state after:
case w.refine_2
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
c : R
x : ↥(sSup (domain '' c✝))
⊢ ↑↑↑(P x) (c • ⟨↑x, ⋯⟩) = σ c • f x
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 : E →ₛₗ.[σ] F
S : Submodule R E
x : ↥(S ⊓ f.domain)
y : ↥f.domain
h : ↑x = ↑y
⊢ ↑((Submodule.inclusion ⋯) x) = ↑y

Tactic:
simp [h]

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

Goal state before:
pp: p : ℕ
⊢ Prime p ↔ 2 ≤ p ∧ ¬∃ m n, m < p ∧ n < p ∧ m * n = p

Tactic:
push Not
  simp_rw [prime_def_lt, dvd_def, exists_imp]
  refine and_congr_right fun hp ↦ forall_congr' fun m ↦ (forall_congr' fun h ↦ ?_).trans forall_comm
  simp_rw [Ne, forall_comm (β := _ = _), eq_comm, imp_false, not_lt]
  refine forall₂_congr fun n hp ↦ ⟨by simp_all, fun hpn ↦ ?_⟩
  have := mul_ne_zero_iff.mp (hp ▸ show p ≠ 0 by lia)
  exact (Nat.mul_eq_right (by lia)).mp
    (hp.symm.trans (hpn.antisymm (hp ▸ Nat.le_mul_of_pos_left _ (by lia))))

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
x : E × F
⊢ x ∈ f.graph ↔ ∃ y, (↑y, ↑f y) = x

Tactic:
simp [graph]

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
h : fst✝ = x_fst ∧ z • snd✝ = x_snd
y : ↥f.domain
hy : ↑y = (fst✝, snd✝).1
hx' : ↑f y = (fst✝, snd✝).2
⊢ ∃ y, ↑y = (x_fst, x_snd).1 ∧ ↑(z • f) y = (x_fst, x_snd).2

Tactic:
use y

Goal state after:
case h
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
h : fst✝ = x_fst ∧ z • snd✝ = x_snd
y : ↥f.domain
hy : ↑y = (fst✝, snd✝).1
hx' : ↑f y = (fst✝, snd✝).2
⊢ ↑y = (x_fst, x_snd).1 ∧ ↑(z • f) y = (x_fst, x_snd).2
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
inst✝ : Module R F
f : E →ₗ.[R] F
x_fst : E
x_snd : F
fst✝ : E
snd✝ : F
h : fst✝ = x_fst ∧ -snd✝ = x_snd
y : ↥f.domain
hy : ↑y = (fst✝, snd✝).1
hx' : ↑f y = (fst✝, snd✝).2
⊢ ∃ y, ↑y = (x_fst, x_snd).1 ∧ ↑(-f) y = (x_fst, x_snd).2

Tactic:
use y

Goal state after:
case h
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
fst✝ : E
snd✝ : F
h : fst✝ = x_fst ∧ -snd✝ = x_snd
y : ↥f.domain
hy : ↑y = (fst✝, snd✝).1
hx' : ↑f y = (fst✝, snd✝).2
⊢ ↑y = (x_fst, x_snd).1 ∧ ↑(-f) y = (x_fst, x_snd).2
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
x : E
y : F
h : (x, y) ∈ f.graph
⊢ x ∈ f.domain

Tactic:
rw [mem_domain_iff]

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
f : E →ₗ.[R] F
x : E
y : F
h : (x, y) ∈ f.graph
⊢ ∃ y, (x, y) ∈ f.graph
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
x : E
y : F
hx : (x, y) ∈ f.graph
⊢ ∃ y, (x, y) ∈ g.graph

Tactic:
use y

Goal state after:
case h
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
y : F
hx : (x, y) ∈ f.graph
⊢ (x, y) ∈ g.graph
Module: Mathlib.Algebra.Polynomial.Coeff

Goal state before:
pp: case pos
R : Type u_1
inst✝ : Ring R
p : R[X]
n : ℕ
a : R
n✝ : ℕ
h : n✝ = n
⊢ a = p.coeff n✝ + (a - p.coeff n)

Tactic:
simp [h]

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

Goal state before:
pp: case neg
R : Type u_1
inst✝ : Ring R
p : R[X]
n : ℕ
a : R
n✝ : ℕ
h : ¬n✝ = n
⊢ p.coeff n✝ = p.coeff n✝ + 0

Tactic:
simp [h]

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

Goal state before:
pp: case inr
R : Type u
inst✝ : Semiring R
p : R[X]
h : p ≠ 0
⊢ AddMonoidAlgebra.supDegree id p.toFinsupp = p.natDegree

Tactic:
apply WithBot.coe_injective

Goal state after:
case inr
R : Type u
inst✝ : Semiring R
p : R[X]
h : p ≠ 0
⊢ ↑(AddMonoidAlgebra.supDegree id p.toFinsupp) = ↑p.natDegree
Module: Mathlib.Algebra.Polynomial.Degree.Operations

Goal state before:
pp: R : Type u
inst✝ : Semiring R
p : R[X]
n : ℕ
pn : p.natDegree ≤ n
p1 : p.coeff n = 1
⊢ p.Monic

Tactic:
unfold Monic
  nontriviality
  refine (congr_arg _ <| natDegree_eq_of_le_of_coeff_ne_zero pn ?_).trans p1
  exact ne_of_eq_of_ne p1 one_ne_zero

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

Goal state before:
pp: R : Type u
inst✝¹ : Semiring R
inst✝ : NoZeroDivisors R
p q : R[X]
h1 : p ∣ q
h2 : q ≠ 0
⊢ p.degree ≤ q.degree

Tactic:
by
  rcases h1 with ⟨q, rfl⟩; rw [mul_ne_zero_iff] at h2
  exact degree_le_mul_left p h2.2

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

Goal state before:
pp: R : Type u
a b c : R
inst✝ : Semiring R
⊢ (C a * X ^ 2 + C b * X + C c).degree ≤ 2

Tactic:
simpa only [add_assoc] using!
    degree_add_le_of_degree_le (degree_C_mul_X_pow_le 2 a)
      (le_trans degree_linear_le <| WithBot.coe_le_coe.mpr one_le_two)

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

Goal state before:
pp: R : Type u
inst✝ : Semiring R
p : R[X]
n : ℕ
⊢ (p ^ n).coeff (n * p.natDegree) = p.leadingCoeff ^ n

Tactic:
induction n with
  | zero => simp
  | succ i hi =>
    rw [pow_succ, pow_succ, Nat.succ_mul]
    by_cases hp1 : p.leadingCoeff ^ i = 0
    · rw [hp1, zero_mul]
      by_cases hp2 : p ^ i = 0
      · rw [hp2, zero_mul, coeff_zero]
      · apply coeff_eq_zero_of_natDegree_lt
        have h1 : (p ^ i).natDegree < i * p.natDegree := by
          refine lt_of_le_of_ne natDegree_pow_le fun h => hp2 ?_
          rw [← h, hp1] at hi
          exact leadingCoeff_eq_zero.mp hi
        calc
          (p ^ i * p).natDegree ≤ (p ^ i).natDegree + p.natDegree := natDegree_mul_le
          _ < i * p.natDegree + p.natDegree := by gcongr
    · rw [← natDegree_pow' hp1, ← leadingCoeff_pow' hp1]
      exact coeff_mul_degree_add_degree _ _

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

Goal state before:
pp: case mp.inr
α : Type u
inst✝ : DecidableEq α
a : α
n : ℕ
x y : α →₀ ℕ
i : α
h : x i + y i = if a = i then n else 0
hai : a ≠ i
⊢ (if a = i then x a else 0) = x i ∧ (if a = i then y a else 0) = y i

Tactic:
if_neg hai,

Goal state after:
case mp.inr
α : Type u
inst✝ : DecidableEq α
a : α
n : ℕ
x y : α →₀ ℕ
i : α
hai : a ≠ i
h : x i + y i = 0
⊢ 0 = x i ∧ 0 = y i
Module: Mathlib.Algebra.Polynomial.AlgebraMap

Goal state before:
pp: R : Type u_3
A : Type u_4
inst✝² : CommSemiring R
inst✝¹ : Semiring A
inst✝ : Algebra R A
p : R[X]
f : R[X] →ₐ[R] A
| f p

Tactic:
← Polynomial.sum_C_mul_X_pow_eq p

Goal state after:
R : Type u_3
A : Type u_4
inst✝² : CommSemiring R
inst✝¹ : Semiring A
inst✝ : Algebra R A
p : R[X]
f : R[X] →ₐ[R] A
| f (p.sum fun n a ↦ C a * X ^ n)
Module: Mathlib.Algebra.Polynomial.AlgebraMap

Goal state before:
pp: R : Type u
inst✝ : CommSemiring R
p q p' q' : R[X]
hpq : p.comp q = X
hqp : q.comp p = X
hpq' : p'.comp q' = X
hqp' : q'.comp p' = X
h : p = p'
a✝ : R[X]
⊢ (p.algEquivOfCompEqX q hpq hqp) a✝ = (p'.algEquivOfCompEqX q' hpq' hqp') a✝

Tactic:
simp [h]

Goal state after: