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

Goal state before:
pp: ι : Type u_1
R : ι → Type u_2
inst✝ : (i : ι) → CommSemiring (R i)
i : ι
S : Submonoid (R i)
T : Submonoid ((i : ι) → R i) := Submonoid.comap (Pi.evalRingHom R i) S
⊢ Bijective ⇑(mapPiEvalRingHom S)

Tactic:
refine ⟨fun x₁ x₂ eq ↦ ?_, fun x ↦ ?_⟩

Goal state after:
case refine_1
ι : Type u_1
R : ι → Type u_2
inst✝ : (i : ι) → CommSemiring (R i)
i : ι
S : Submonoid (R i)
T : Submonoid ((i : ι) → R i) := Submonoid.comap (Pi.evalRingHom R i) S
x₁ x₂ : Localization (Submonoid.comap (Pi.evalRingHom R i) S)
eq : (mapPiEvalRingHom S) x₁ = (mapPiEvalRingHom S) x₂
⊢ x₁ = x₂

case refine_2
ι : Type u_1
R : ι → Type u_2
inst✝ : (i : ι) → CommSemiring (R i)
i : ι
S : Submonoid (R i)
T : Submonoid ((i : ι) → R i) := Submonoid.comap (Pi.evalRingHom R i) S
x : Localization S
⊢ ∃ a, (mapPiEvalRingHom S) a = x
Module: Mathlib.RingTheory.Adjoin.Basic

Goal state before:
pp: case a
R : Type uR
A : Type uA
B : Type uB
inst✝⁴ : CommSemiring R
inst✝³ : Semiring A
inst✝² : Semiring B
inst✝¹ : Algebra R A
inst✝ : Algebra R B
s : Set A
t : Set B
a : A
b : B
ha : (a, b).1 ∈ ↑(adjoin R s)
hb : (a, b).2 ∈ ↑(adjoin R t)
P : Subalgebra R (A × B) := adjoin R (⇑(LinearMap.inl R A B) '' (s ∪ {1}) ∪ ⇑(LinearMap.inr R A B) '' (t ∪ {1}))
Ha : (a, 0) ∈ adjoin R (⇑(LinearMap.inl R A B) '' (s ∪ {1}))
⊢ (a, b) ∈ adjoin R (⇑(LinearMap.inl R A B) '' (s ∪ {1}) ∪ ⇑(LinearMap.inr R A B) '' (t ∪ {1}))

Tactic:
have Hb : ((0 : A), b) ∈ adjoin R (LinearMap.inr R A B '' (t ∪ {1})) :=
      mem_adjoin_of_map_mul R LinearMap.inr_map_mul hb

Goal state after:
case a
R : Type uR
A : Type uA
B : Type uB
inst✝⁴ : CommSemiring R
inst✝³ : Semiring A
inst✝² : Semiring B
inst✝¹ : Algebra R A
inst✝ : Algebra R B
s : Set A
t : Set B
a : A
b : B
ha : (a, b).1 ∈ ↑(adjoin R s)
hb : (a, b).2 ∈ ↑(adjoin R t)
P : Subalgebra R (A × B) := adjoin R (⇑(LinearMap.inl R A B) '' (s ∪ {1}) ∪ ⇑(LinearMap.inr R A B) '' (t ∪ {1}))
Ha : (a, 0) ∈ adjoin R (⇑(LinearMap.inl R A B) '' (s ∪ {1}))
Hb : (0, b) ∈ adjoin R (⇑(LinearMap.inr R A B) '' (t ∪ {1}))
⊢ (a, b) ∈ adjoin R (⇑(LinearMap.inl R A B) '' (s ∪ {1}) ∪ ⇑(LinearMap.inr R A B) '' (t ∪ {1}))
Module: Mathlib.RingTheory.Adjoin.Basic

Goal state before:
pp: F : Type u_4
E : Type u_5
L : Type u_6
L' : Type u_7
inst✝¹⁰ : CommSemiring F
inst✝⁹ : CommSemiring L
inst✝⁸ : CommSemiring L'
inst✝⁷ : Semiring E
inst✝⁶ : Algebra F L
inst✝⁵ : Algebra L E
inst✝⁴ : Algebra F L'
inst✝³ : Algebra L' E
inst✝² : Algebra F E
inst✝¹ : IsScalarTower F L E
inst✝ : IsScalarTower F L' E
i : L ≃ₐ[F] L'
hi : ⇑(algebraMap L E) = ⇑(algebraMap L' E) ∘ ⇑i
S : Set E
K K' : Subalgebra F E
h : K.toSubsemiring = K'.toSubsemiring
⊢ K = K'

Tactic:
SetLike.ext'_iff

Goal state after:
F : Type u_4
E : Type u_5
L : Type u_6
L' : Type u_7
inst✝¹⁰ : CommSemiring F
inst✝⁹ : CommSemiring L
inst✝⁸ : CommSemiring L'
inst✝⁷ : Semiring E
inst✝⁶ : Algebra F L
inst✝⁵ : Algebra L E
inst✝⁴ : Algebra F L'
inst✝³ : Algebra L' E
inst✝² : Algebra F E
inst✝¹ : IsScalarTower F L E
inst✝ : IsScalarTower F L' E
i : L ≃ₐ[F] L'
hi : ⇑(algebraMap L E) = ⇑(algebraMap L' E) ∘ ⇑i
S : Set E
K K' : Subalgebra F E
h : ↑K.toSubsemiring = ↑K'.toSubsemiring
⊢ ↑K = ↑K'
Module: Mathlib.RingTheory.Localization.Basic

Goal state before:
pp: R : Type u_1
inst✝ : CommRing R
M : Submonoid R
hM : M ≤ nonZeroDivisors R
a c : R
b d : ↥M
x✝ : ∃ a_1 ∈ M, a_1 * (↑d * a) = a_1 * (↑b * c)
u : R
hu : u ∈ M
h : u * (↑d * a) = u * (↑b * c)
hu' : ∀ (x : R), u * x = 0 → x = 0
⊢ u * (a * ↑d - ↑b * c) = 0

Tactic:
rwa [mul_sub, sub_eq_zero, mul_comm a]

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

Goal state before:
pp: R : Type u_1
M : Type u_2
inst✝⁴ : CommRing R
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : Module.Finite R M
inst✝ : Nontrivial M
n : ℕ
f : Fin n → M
hf : Submodule.span R (Set.range f) = ⊤
s : Set ℕ := {m | Submodule.span R (f '' Fin.val ⁻¹' Set.Iio m) ≠ ⊤}
hns : ∀ x ∈ s, x < n
hs₁ : s.Nonempty
hs₂ : BddAbove s
hs : sSup s ∈ s
this : Submodule.span R (f '' Fin.val ⁻¹' Set.Iio (Order.succ (sSup s))) = ⊤
⊢ ⊤ = R ∙ (Submodule.span R (f '' Fin.val ⁻¹' Set.Iio (sSup s))).mkQ (f ⟨sSup s, ⋯⟩)

Tactic:
rw [← Set.image_singleton, ← Submodule.map_span,
    ← (Submodule.comap_injective_of_surjective (Submodule.mkQ_surjective _)).eq_iff,
    Submodule.comap_map_eq, Submodule.ker_mkQ, Submodule.comap_top, ← this, ← Submodule.span_union,
    Order.Iio_succ_eq_insert (sSup s), ← Set.union_singleton, Set.preimage_union, Set.image_union,
    ← @Set.image_singleton _ _ f, Set.union_comm]

Goal state after:
R : Type u_1
M : Type u_2
inst✝⁴ : CommRing R
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : Module.Finite R M
inst✝ : Nontrivial M
n : ℕ
f : Fin n → M
hf : Submodule.span R (Set.range f) = ⊤
s : Set ℕ := {m | Submodule.span R (f '' Fin.val ⁻¹' Set.Iio m) ≠ ⊤}
hns : ∀ x ∈ s, x < n
hs₁ : s.Nonempty
hs₂ : BddAbove s
hs : sSup s ∈ s
this : Submodule.span R (f '' Fin.val ⁻¹' Set.Iio (Order.succ (sSup s))) = ⊤
⊢ Submodule.span R (f '' Fin.val ⁻¹' {sSup s} ∪ f '' Fin.val ⁻¹' Set.Iio (sSup s)) =
    Submodule.span R (f '' {⟨sSup s, ⋯⟩} ∪ f '' Fin.val ⁻¹' Set.Iio (sSup s))
Module: Mathlib.Algebra.Ring.TransferInstance

Goal state before:
pp: α : Type u_1
β : Type u_2
e : α ≃ β
inst✝ : NonAssocSemiring β
mul : Mul α := e.mul
⊢ NonAssocSemiring α

Tactic:
let add_monoid_with_one := e.addMonoidWithOne

Goal state after:
α : Type u_1
β : Type u_2
e : α ≃ β
inst✝ : NonAssocSemiring β
mul : Mul α := e.mul
add_monoid_with_one : AddMonoidWithOne α := e.addMonoidWithOne
⊢ NonAssocSemiring α
Module: Mathlib.Algebra.Ring.TransferInstance

Goal state before:
pp: α : Type u_1
β : Type u_2
e : α ≃ β
inst✝ : Semiring β
mul : Mul α := e.mul
⊢ Semiring α

Tactic:
let add_monoid_with_one := e.addMonoidWithOne

Goal state after:
α : Type u_1
β : Type u_2
e : α ≃ β
inst✝ : Semiring β
mul : Mul α := e.mul
add_monoid_with_one : AddMonoidWithOne α := e.addMonoidWithOne
⊢ Semiring α
Module: Mathlib.Algebra.Ring.TransferInstance

Goal state before:
pp: α : Type u_1
β : Type u_2
e : α ≃ β
inst✝ : CommSemiring β
mul : Mul α := e.mul
⊢ CommSemiring α

Tactic:
let add_monoid_with_one := e.addMonoidWithOne

Goal state after:
α : Type u_1
β : Type u_2
e : α ≃ β
inst✝ : CommSemiring β
mul : Mul α := e.mul
add_monoid_with_one : AddMonoidWithOne α := e.addMonoidWithOne
⊢ CommSemiring α
Module: Mathlib.Algebra.Algebra.Spectrum.Basic

Goal state before:
pp: R : Type u
A : Type v
inst✝² : CommSemiring R
inst✝¹ : Ring A
inst✝ : Algebra R A
r : Rˣ
a : Aˣ
h : ↑r ∈ resolventSet R ↑a
⊢ ↑r⁻¹ ∈ resolventSet R ↑a⁻¹

Tactic:
mem_resolventSet_iff,

Goal state after:
R : Type u
A : Type v
inst✝² : CommSemiring R
inst✝¹ : Ring A
inst✝ : Algebra R A
r : Rˣ
a : Aˣ
h : IsUnit (↑ₐ ↑r - ↑a)
⊢ IsUnit (↑ₐ ↑r⁻¹ - ↑a⁻¹)
Module: Mathlib.Algebra.Algebra.Spectrum.Basic

Goal state before:
pp: R : Type u
A : Type v
inst✝² : CommSemiring R
inst✝¹ : Ring A
inst✝ : Algebra R A
r : Rˣ
a : Aˣ
h : IsUnit (r • 1 - ↑a)
h₁ : ↑a * (r • ↑a⁻¹ - 1) = r • 1 - ↑a
h₂ : (r • ↑a⁻¹ - 1) * ↑a = r • 1 - ↑a
⊢ Commute (↑a) (r • ↑a⁻¹ - 1)

Tactic:
← h₂

Goal state after:
R : Type u
A : Type v
inst✝² : CommSemiring R
inst✝¹ : Ring A
inst✝ : Algebra R A
r : Rˣ
a : Aˣ
h : IsUnit (r • 1 - ↑a)
h₁ : ↑a * (r • ↑a⁻¹ - 1) = (r • ↑a⁻¹ - 1) * ↑a
h₂ : (r • ↑a⁻¹ - 1) * ↑a = r • 1 - ↑a
⊢ Commute (↑a) (r • ↑a⁻¹ - 1)
Module: Mathlib.Algebra.Algebra.Spectrum.Basic

Goal state before:
pp: R : Type u
A : Type v
inst✝⁵ : CommSemiring R
inst✝⁴ : Ring A
inst✝³ : Algebra R A
inst✝² : InvolutiveStar R
inst✝¹ : StarRing A
inst✝ : StarModule R A
r : R
a : A
⊢ star r ∈ resolventSet R a ↔ r ∈ resolventSet R (star a)

Tactic:
by
  refine ⟨fun h => ?_, fun h => ?_⟩ <;>
    simpa only [mem_resolventSet_iff, Algebra.algebraMap_eq_smul_one, star_sub, star_smul,
      star_star, star_one] using IsUnit.star h

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

Goal state before:
pp: case refine_2.refine_3
R : Type u_1
A : Type u_2
B : Type u_3
M : Type u_4
inst✝¹¹ : CommSemiring R
inst✝¹⁰ : AddCommMonoid M
inst✝⁹ : Module R M
inst✝⁸ : Semiring A
inst✝⁷ : Semiring B
inst✝⁶ : Module A M
inst✝⁵ : Module B M
inst✝⁴ : Algebra R A
inst✝³ : Algebra R B
inst✝² : IsScalarTower R A M
inst✝¹ : IsScalarTower R B M
inst✝ : SMulCommClass A B M
x y : A ⊗[R] B
m : M
z w : A ⊗[R] B
hz : ∀ (x : A) (y : B), (x ⊗ₜ[R] y * z) • m = x ⊗ₜ[R] y • z • m
hw : ∀ (x : A) (y : B), (x ⊗ₜ[R] y * w) • m = x ⊗ₜ[R] y • w • m
a : A
b : B
⊢ (a ⊗ₜ[R] b * (z + w)) • m = a ⊗ₜ[R] b • (z + w) • m

Tactic:
simp only [(· • ·)] at hz hw ⊢

Goal state after:
case refine_2.refine_3
R : Type u_1
A : Type u_2
B : Type u_3
M : Type u_4
inst✝¹¹ : CommSemiring R
inst✝¹⁰ : AddCommMonoid M
inst✝⁹ : Module R M
inst✝⁸ : Semiring A
inst✝⁷ : Semiring B
inst✝⁶ : Module A M
inst✝⁵ : Module B M
inst✝⁴ : Algebra R A
inst✝³ : Algebra R B
inst✝² : IsScalarTower R A M
inst✝¹ : IsScalarTower R B M
inst✝ : SMulCommClass A B M
x y : A ⊗[R] B
m : M
z w : A ⊗[R] B
hz : ∀ (x : A) (y : B), (moduleAux (x ⊗ₜ[R] y * z)) m = (moduleAux (x ⊗ₜ[R] y)) ((moduleAux z) m)
hw : ∀ (x : A) (y : B), (moduleAux (x ⊗ₜ[R] y * w)) m = (moduleAux (x ⊗ₜ[R] y)) ((moduleAux w) m)
a : A
b : B
⊢ (moduleAux (a ⊗ₜ[R] b * (z + w))) m = (moduleAux (a ⊗ₜ[R] b)) ((moduleAux (z + w)) m)
Module: Mathlib.RingTheory.TensorProduct.Basic

Goal state before:
pp: case refine_3.refine_2
R : Type u_1
A : Type u_2
B : Type u_3
M : Type u_4
inst✝¹¹ : CommSemiring R
inst✝¹⁰ : AddCommMonoid M
inst✝⁹ : Module R M
inst✝⁸ : Semiring A
inst✝⁷ : Semiring B
inst✝⁶ : Module A M
inst✝⁵ : Module B M
inst✝⁴ : Algebra R A
inst✝³ : Algebra R B
inst✝² : IsScalarTower R A M
inst✝¹ : IsScalarTower R B M
inst✝ : SMulCommClass A B M
x y : A ⊗[R] B
m : M
a : A
b : B
z w : A ⊗[R] B
hz : (z * a ⊗ₜ[R] b) • m = z • a ⊗ₜ[R] b • m
hw : (w * a ⊗ₜ[R] b) • m = w • a ⊗ₜ[R] b • m
⊢ ((z + w) * a ⊗ₜ[R] b) • m = (z + w) • a ⊗ₜ[R] b • m

Tactic:
simp only [(· • ·)] at hz hw ⊢

Goal state after:
case refine_3.refine_2
R : Type u_1
A : Type u_2
B : Type u_3
M : Type u_4
inst✝¹¹ : CommSemiring R
inst✝¹⁰ : AddCommMonoid M
inst✝⁹ : Module R M
inst✝⁸ : Semiring A
inst✝⁷ : Semiring B
inst✝⁶ : Module A M
inst✝⁵ : Module B M
inst✝⁴ : Algebra R A
inst✝³ : Algebra R B
inst✝² : IsScalarTower R A M
inst✝¹ : IsScalarTower R B M
inst✝ : SMulCommClass A B M
x y : A ⊗[R] B
m : M
a : A
b : B
z w : A ⊗[R] B
hz : (moduleAux (z * a ⊗ₜ[R] b)) m = (moduleAux z) ((moduleAux (a ⊗ₜ[R] b)) m)
hw : (moduleAux (w * a ⊗ₜ[R] b)) m = (moduleAux w) ((moduleAux (a ⊗ₜ[R] b)) m)
⊢ (moduleAux ((z + w) * a ⊗ₜ[R] b)) m = (moduleAux (z + w)) ((moduleAux (a ⊗ₜ[R] b)) m)
Module: Mathlib.RingTheory.TensorProduct.Basic

Goal state before:
pp: case refine_3.refine_3
R : Type u_1
A : Type u_2
B : Type u_3
M : Type u_4
inst✝¹¹ : CommSemiring R
inst✝¹⁰ : AddCommMonoid M
inst✝⁹ : Module R M
inst✝⁸ : Semiring A
inst✝⁷ : Semiring B
inst✝⁶ : Module A M
inst✝⁵ : Module B M
inst✝⁴ : Algebra R A
inst✝³ : Algebra R B
inst✝² : IsScalarTower R A M
inst✝¹ : IsScalarTower R B M
inst✝ : SMulCommClass A B M
x y : A ⊗[R] B
m : M
u v : A ⊗[R] B
a✝¹ : ∀ (x y : A ⊗[R] B), (x * u) • m = x • u • m → (y * u) • m = y • u • m → ((x + y) * u) • m = (x + y) • u • m
a✝ : ∀ (x y : A ⊗[R] B), (x * v) • m = x • v • m → (y * v) • m = y • v • m → ((x + y) * v) • m = (x + y) • v • m
z w : A ⊗[R] B
hz : (z * (u + v)) • m = z • (u + v) • m
hw : (w * (u + v)) • m = w • (u + v) • m
⊢ ((z + w) * (u + v)) • m = (z + w) • (u + v) • m

Tactic:
simp only [(· • ·)] at hz hw ⊢

Goal state after:
case refine_3.refine_3
R : Type u_1
A : Type u_2
B : Type u_3
M : Type u_4
inst✝¹¹ : CommSemiring R
inst✝¹⁰ : AddCommMonoid M
inst✝⁹ : Module R M
inst✝⁸ : Semiring A
inst✝⁷ : Semiring B
inst✝⁶ : Module A M
inst✝⁵ : Module B M
inst✝⁴ : Algebra R A
inst✝³ : Algebra R B
inst✝² : IsScalarTower R A M
inst✝¹ : IsScalarTower R B M
inst✝ : SMulCommClass A B M
x y : A ⊗[R] B
m : M
u v : A ⊗[R] B
a✝¹ : ∀ (x y : A ⊗[R] B), (x * u) • m = x • u • m → (y * u) • m = y • u • m → ((x + y) * u) • m = (x + y) • u • m
a✝ : ∀ (x y : A ⊗[R] B), (x * v) • m = x • v • m → (y * v) • m = y • v • m → ((x + y) * v) • m = (x + y) • v • m
z w : A ⊗[R] B
hz : (moduleAux (z * (u + v))) m = (moduleAux z) ((moduleAux (u + v)) m)
hw : (moduleAux (w * (u + v))) m = (moduleAux w) ((moduleAux (u + v)) m)
⊢ (moduleAux ((z + w) * (u + v))) m = (moduleAux (z + w)) ((moduleAux (u + v)) m)
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) ⋯ 1 = 1

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

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

Goal state before:
pp: R : Type u
inst✝⁶ : Semiring R
inst✝⁵ : StrongRankCondition R
ι : Type v
inst✝⁴ : Fintype ι
M : ι → Type w
inst✝³ : (i : ι) → AddCommMonoid (M i)
inst✝² : (i : ι) → Module R (M i)
inst✝¹ : ∀ (i : ι), Free R (M i)
inst✝ : ∀ (i : ι), Module.Finite R (M i)
⊢ finrank R (⨁ (i : ι), M i) = ∑ i, finrank R (M i)

Tactic:
by
  simp only [finrank, fun i => rank_eq_card_chooseBasisIndex R (M i), rank_directSum, ← mk_sigma,
    mk_toNat_eq_card, card_sigma]

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

Goal state before:
pp: R : Type u
inst✝⁶ : Semiring R
inst✝⁵ : StrongRankCondition R
ι : Type v
inst✝⁴ : Fintype ι
M : ι → Type w
inst✝³ : (i : ι) → AddCommMonoid (M i)
inst✝² : (i : ι) → Module R (M i)
inst✝¹ : ∀ (i : ι), Free R (M i)
inst✝ : ∀ (i : ι), Module.Finite R (M i)
⊢ finrank R ((i : ι) → M i) = ∑ i, finrank R (M i)

Tactic:
by
  simp only [finrank, fun i => rank_eq_card_chooseBasisIndex R (M i), rank_pi, ← mk_sigma,
    mk_toNat_eq_card, Fintype.card_sigma]

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

Goal state before:
pp: case mpr
R : Type u_1
M : Type u_2
inst✝² : Ring R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
a✝ : Nontrivial R
h : ∀ (x : M), ∃ a, a ≠ 0 ∧ a • x = 0
s : Set M
hs : LinearIndepOn R id s
⊢ IsEmpty ↑↑⟨s, hs⟩

Tactic:
← not_nonempty_iff

Goal state after:
case mpr
R : Type u_1
M : Type u_2
inst✝² : Ring R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
a✝ : Nontrivial R
h : ∀ (x : M), ∃ a, a ≠ 0 ∧ a • x = 0
s : Set M
hs : LinearIndepOn R id s
⊢ ¬Nonempty ↑↑⟨s, hs⟩
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
f g : E →ₛₗ.[σ] F
c : R
x : E
x✝ : x ∈ {x | ∃ (hf : x ∈ f.domain) (hg : x ∈ g.domain), ↑f ⟨x, hf⟩ = ↑g ⟨x, hg⟩}
hfx : x ∈ f.domain
hgx : x ∈ g.domain
hx : ↑f ⟨x, hfx⟩ = ↑g ⟨x, hgx⟩
⊢ ↑f ⟨c • x, ⋯⟩ = ↑g ⟨c • x, ⋯⟩

Tactic:
have {f : E →ₛₗ.[σ] F} (hfx) : (⟨c • x, smul_mem _ c hfx⟩ : f.domain) = c • ⟨x, hfx⟩ := by
        simp
      rw [this hfx, this hgx, f.map_smulₛₗ, g.map_smulₛₗ, hx]

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

Goal state before:
pp: F : Type u_1
K : Type u_2
inst✝⁴ : Field F
inst✝³ : Ring K
inst✝² : IsDomain K
inst✝¹ : Algebra F K
inst✝ : FiniteDimensional F K
x : K
H : x ≠ 0
this : Surjective ⇑(LinearMap.mulLeft F x)
⊢ ∃ y, x * y = 1

Tactic:
exact this 1

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 + (b + c)

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

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
v : V
nz : v ≠ 0
⊢ finrank K V = 1 ↔ ∀ (w : V), ∃ c, c • v = w

Tactic:
rw [finrank_eq_one_iff_of_nonzero v nz]

Goal state after:
K : Type u
V : Type v
inst✝² : DivisionRing K
inst✝¹ : AddCommGroup V
inst✝ : Module K V
v : V
nz : v ≠ 0
⊢ K ∙ v = ⊤ ↔ ∀ (w : V), ∃ c, c • v = w
Module: Mathlib.Algebra.Polynomial.Eval.Defs

Goal state before:
pp: R : Type u
inst✝ : Semiring R
p : R[X]
x : R
⊢ eval x p = p.sum fun e a ↦ a * x ^ e

Tactic:
by
  rw [eval, eval₂_eq_sum]
  rfl

Goal state after:
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
p q : R[X]
⊢ ∀ (n : ℕ) (a : R),
    map f ((C a * X ^ n).comp q) = (map f (C a * X ^ n)).comp (map f q) →
      map f ((C a * X ^ (n + 1)).comp q) = (map f (C a * X ^ (n + 1))).comp (map f q)

Tactic:
simp +contextual only [pow_succ, ← mul_assoc, comp, forall_const,
        eval₂_mul_X, imp_true_iff, map_X, Polynomial.map_mul]

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

Goal state before:
pp: n : ℕ
pos : 0 < n
np : ¬(2 ≤ n ∧ n.minFac = n)
h1 : n = n.minFac
⊢ n.minFac ≤ n / n.minFac

Tactic:
not_and_or,

Goal state after:
n : ℕ
pos : 0 < n
np : ¬2 ≤ n ∨ ¬n.minFac = n
h1 : n = n.minFac
⊢ n.minFac ≤ n / n.minFac
Module: Mathlib.LinearAlgebra.LinearPMap

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

Tactic:
Set.mem_range

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

Goal state before:
pp: case zero
R : Type u_1
inst✝² : NonAssocSemiring R
inst✝¹ : Nontrivial R
inst✝ : CharZero R
⊢ CharZero R

pp: case prime
R : Type u_1
inst✝¹ : NonAssocSemiring R
inst✝ : Nontrivial R
hprime✝ : Nat.Prime 1
hchar✝ : CharP R 1
⊢ CharZero R

Tactic:
· assumption

Goal state after:
case prime
R : Type u_1
inst✝¹ : NonAssocSemiring R
inst✝ : Nontrivial R
hprime✝ : Nat.Prime 1
hchar✝ : CharP R 1
⊢ CharZero R
Module: Mathlib.Order.Filter.Extr

Goal state before:
pp: α : Type u
l : Filter α
a : α
β : Type u_1
inst✝ : PartialOrder β
f : α → β
h₁ : IsMinFilter f l a
h₂ : IsMaxFilter f l a
⊢ f =ᶠ[l] fun x ↦ f a

Tactic:
filter_upwards [h₁, h₂] using by grind

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

Goal state before:
pp: R : Type u_1
inst✝ : Semiring R
n k : ℕ
⊢ ((X + C 1) ^ n).coeff k = ↑(n.choose k)

Tactic:
coeff_X_add_C_pow,

Goal state after:
R : Type u_1
inst✝ : Semiring R
n k : ℕ
⊢ 1 ^ (n - k) * ↑(n.choose k) = ↑(n.choose k)
Module: Mathlib.Algebra.Polynomial.Degree.Defs

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

Tactic:
by_cases h : a = 0

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

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.degree = q.degree
hlc : p.leadingCoeff + q.leadingCoeff ≠ 0
⊢ (p + q).degree = p.degree

Tactic:
rw [degree_add_eq_of_leadingCoeff_add_ne_zero hlc, h, max_self]

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

Goal state before:
pp: R : Type u
inst✝ : Semiring R
p q : R[X]
h : p.leadingCoeff * q.leadingCoeff ≠ 0
hp : p ≠ 0
hq : q ≠ 0
⊢ (p * q).coeff (p.natDegree + q.natDegree) ≠ 0

Tactic:
coeff_mul_degree_add_degree

Goal state after:
R : Type u
inst✝ : Semiring R
p q : R[X]
h : p.leadingCoeff * q.leadingCoeff ≠ 0
hp : p ≠ 0
hq : q ≠ 0
⊢ p.leadingCoeff * q.leadingCoeff ≠ 0
Module: Mathlib.Algebra.MonoidAlgebra.Degree

Goal state before:
pp: R : Type u_1
A : Type u_3
B : Type u_5
inst✝² : Semiring R
inst✝¹ : LinearOrder B
inst✝ : OrderBot B
p : R[A]
D : A → B
hp : p ≠ 0
⊢ supDegree D p ∈ Set.range D

Tactic:
by
  obtain ⟨a, -, he⟩ := exists_supDegree_mem_support D hp; exact ⟨a, he.symm⟩

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

Goal state before:
pp: 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
inst✝ : NoZeroDivisors R
hD : Function.Injective D
hadd : ∀ (a1 a2 : A), D (a1 + a2) = D a1 + D a2
⊢ leadingCoeff D (p * q) = leadingCoeff D p * leadingCoeff D q

Tactic:
by
  obtain rfl | hp := eq_or_ne p 0
  · simp_rw [leadingCoeff_zero, zero_mul, leadingCoeff_zero]
  obtain rfl | hq := eq_or_ne q 0
  · simp_rw [leadingCoeff_zero, mul_zero, leadingCoeff_zero]
  rw [← coeff_supDegree_add_supDegree hD hadd, ← supDegree_mul hD hadd ?_ hp hq, leadingCoeff]
  apply mul_ne_zero <;> rwa [Ne, leadingCoeff_eq_zero hD]

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

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

Tactic:
simpa [Finsupp.embDomain_eq_mapDomain] using Finsupp.embDomain_le_embDomain_iff_le ⟨f, h⟩ g₁ g₂

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

Goal state before:
pp: ι : Type u_1
α : Type u_3
inst✝² : AddCommMonoid α
inst✝¹ : PartialOrder α
inst✝ : CanonicallyOrderedAdd α
f g : ι →₀ α
s : Finset ι
hf : f.support ⊆ s
⊢ f ≤ g ↔ ∀ i ∈ s, f i ≤ g i

Tactic:
by
  refine ⟨fun h s _ ↦ h s, fun h s ↦ ?_⟩
  by_cases H : s ∈ f.support
  · exact h s (hf H)
  · exact notMem_support_iff.1 H ▸ zero_le

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

Goal state before:
pp: case neg
ι : Type u_1
κ : Type u_2
α : Type u_3
inst✝⁴ : AddCommMonoid α
inst✝³ : PartialOrder α
inst✝² : CanonicallyOrderedAdd α
inst✝¹ : Sub α
inst✝ : OrderedSub α
f : ι → κ
h : Function.Injective f
f1 f2 : ι →₀ α
y : κ
hy : y ∈ Set.range f
⊢ (mapDomain f (f1 - f2)) y = (mapDomain f f1 - mapDomain f f2) y

Tactic:
obtain ⟨x, rfl⟩ := hy
    simp [mapDomain_apply h]

Goal state after:
Module: Mathlib.Order.PiLex

Goal state before:
pp: ι : Type u_1
β : ι → Type u_2
inst✝² : LinearOrder ι
x : (i : ι) → β i
i : ι
a : β i
inst✝¹ : (i : ι) → PartialOrder (β i)
inst✝ : WellFoundedLT ι
⊢ x i < a ∨ x = update x i a ↔ x i < a ∨ x i = a

Tactic:
eq_update_self_iff

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

Goal state before:
pp: R : Type u
σ : Type u_1
inst✝ : CommSemiring R
x : σ → ℕ
t : Finset σ
x✝ : σ
hi : x✝ ∈ t
⊢ X x✝ ^ x x✝ = X x✝ ^ (Finsupp.indicator t fun i x_1 ↦ x i) x✝

Tactic:
by simp [Finsupp.indicator, hi]

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

Goal state before:
pp: R : Type u
σ : Type u_1
inst✝ : CommSemiring R
φ : MvPolynomial σ R
d₀ : σ →₀ ℕ
h : ∀ d ∈ φ.support, d = d₀
d : σ →₀ ℕ
⊢ coeff d φ = coeff d ((monomial d₀) (coeff d₀ φ))

Tactic:
rcases eq_or_ne d d₀ with rfl | hd

Goal state after:
case inl
R : Type u
σ : Type u_1
inst✝ : CommSemiring R
φ : MvPolynomial σ R
d : σ →₀ ℕ
h : ∀ d_1 ∈ φ.support, d_1 = d
⊢ coeff d φ = coeff d ((monomial d) (coeff d φ))

case inr
R : Type u
σ : Type u_1
inst✝ : CommSemiring R
φ : MvPolynomial σ R
d₀ : σ →₀ ℕ
h : ∀ d ∈ φ.support, d = d₀
d : σ →₀ ℕ
hd : d ≠ d₀
⊢ coeff d φ = coeff d ((monomial d₀) (coeff d₀ φ))
Module: Mathlib.Algebra.MvPolynomial.Eval

Goal state before:
pp: case mul_X
R : Type u
S₁ : Type v
S₂ : Type w
S₃ : Type x
inst✝¹ : CommSemiring R
inst✝ : CommSemiring S₁
f : R →+* S₁
g : S₂ → MvPolynomial S₃ R
p✝ p : MvPolynomial S₂ R
s : S₂
hp : (map f) (eval₂ C g p) = eval₂ C (⇑(map f) ∘ g) ((map f) p)
⊢ (map f) (eval₂ C g (p * X s)) = eval₂ C (⇑(map f) ∘ g) ((map f) (p * X s))

Tactic:
rw [eval₂_mul, (map f).map_mul, hp, (map f).map_mul, map_X, eval₂_mul, eval₂_X, eval₂_X,
      comp_apply]

Goal state after: