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

Goal state before:
pp: R : Type u
inst✝ : CommSemiring R
p : ℕ
P : R[X]
r : R
f g : R[X]
hf : eval r ((expand R p) f) = eval (r ^ p) f
hg : eval r ((expand R p) g) = eval (r ^ p) g
⊢ eval r ((expand R p) f + (expand R p) g) = eval (r ^ p) (f + g)

Tactic:
eval_add,

Goal state after:
R : Type u
inst✝ : CommSemiring R
p : ℕ
P : R[X]
r : R
f g : R[X]
hf : eval r ((expand R p) f) = eval (r ^ p) f
hg : eval r ((expand R p) g) = eval (r ^ p) g
⊢ eval r ((expand R p) f) + eval r ((expand R p) g) = eval (r ^ p) (f + g)
Module: Mathlib.Algebra.Polynomial.Expand

Goal state before:
pp: R : Type u
inst✝ : CommSemiring R
p : ℕ
P : R[X]
r : R
f g : R[X]
hf : eval r ((expand R p) f) = eval (r ^ p) f
hg : eval r ((expand R p) g) = eval (r ^ p) g
⊢ eval r ((expand R p) f) + eval r ((expand R p) g) = eval (r ^ p) (f + g)

Tactic:
eval_add,

Goal state after:
R : Type u
inst✝ : CommSemiring R
p : ℕ
P : R[X]
r : R
f g : R[X]
hf : eval r ((expand R p) f) = eval (r ^ p) f
hg : eval r ((expand R p) g) = eval (r ^ p) g
⊢ eval r ((expand R p) f) + eval r ((expand R p) g) = eval (r ^ p) f + eval (r ^ p) g
Module: Mathlib.Algebra.Polynomial.Derivative

Goal state before:
pp: case inl
R : Type u
inst✝ : Semiring R
p : R[X]
hp : p.natDegree ≠ 0
hp' : derivative p = 0
⊢ (derivative p).natDegree < p.natDegree

Tactic:
rw [hp', Polynomial.natDegree_zero]

Goal state after:
case inl
R : Type u
inst✝ : Semiring R
p : R[X]
hp : p.natDegree ≠ 0
hp' : derivative p = 0
⊢ 0 < p.natDegree
Module: Mathlib.Algebra.Polynomial.Expand

Goal state before:
pp: case pos
R : Type u
inst✝ : CommSemiring R
p : ℕ
hp : p ≠ 0
f g : R[X]
n x y : ℕ
eq : (p * x, p * y).1 + (p * x, p * y).2 = n * p
nex : ¬∃ a, a.1 + a.2 = n ∧ (a.1 * p, a.2 * p) = (p * x, p * y)
⊢ p * ((x, y).1 + (x, y).2) = (p * x, p * y).1 + (p * x, p * y).2

Tactic:
mul_add

Goal state after:
case pos
R : Type u
inst✝ : CommSemiring R
p : ℕ
hp : p ≠ 0
f g : R[X]
n x y : ℕ
eq : (p * x, p * y).1 + (p * x, p * y).2 = n * p
nex : ¬∃ a, a.1 + a.2 = n ∧ (a.1 * p, a.2 * p) = (p * x, p * y)
⊢ p * (x, y).1 + p * (x, y).2 = (p * x, p * y).1 + (p * x, p * y).2
Module: Mathlib.Algebra.Polynomial.Expand

Goal state before:
pp: case neg.succ
R : Type u
inst✝² : CommSemiring R
p : ℕ
inst✝¹ : CharP R p
inst✝ : NoZeroDivisors R
f : R[X]
hf : derivative f = 0
hp : p ≠ 0
n : ℕ
h : ¬p ∣ n + 1
⊢ 0 = f.coeff (n + 1)

Tactic:
have := coeff_derivative f n

Goal state after:
case neg.succ
R : Type u
inst✝² : CommSemiring R
p : ℕ
inst✝¹ : CharP R p
inst✝ : NoZeroDivisors R
f : R[X]
hf : derivative f = 0
hp : p ≠ 0
n : ℕ
h : ¬p ∣ n + 1
this : (derivative f).coeff n = f.coeff (n + 1) * (↑n + 1)
⊢ 0 = f.coeff (n + 1)
Module: Mathlib.Algebra.Polynomial.Div

Goal state before:
pp: R : Type u
inst✝ : Ring R
f g q r : R[X]
hg : g.Monic
h : r + g * q = f ∧ r.degree < g.degree
a✝ : Nontrivial R
⊢ r - f %ₘ g - -g * (q - f /ₘ g) = 0

Tactic:
by
        rw [← sub_eq_zero_of_eq (h.1.trans (modByMonic_add_div f g).symm)]
        simp [mul_add, sub_eq_add_neg, add_comm, add_left_comm, add_assoc]

Goal state after:
Module: Mathlib.RingTheory.Algebraic.Defs

Goal state before:
pp: R : Type u
A : Type v
inst✝² : CommRing R
inst✝¹ : Ring A
inst✝ : Algebra R A
S : Subalgebra R A
x : ↥S
p : R[X]
⊢ (aeval ↑x) p = 0 ↔ (aeval x) p = 0

Tactic:
have h : Function.Injective S.val := Subtype.val_injective

Goal state after:
R : Type u
A : Type v
inst✝² : CommRing R
inst✝¹ : Ring A
inst✝ : Algebra R A
S : Subalgebra R A
x : ↥S
p : R[X]
h : Function.Injective ⇑S.val
⊢ (aeval ↑x) p = 0 ↔ (aeval x) p = 0
Module: Mathlib.Algebra.Polynomial.Derivative

Goal state before:
pp: case succ.e_a.refine_1
R : Type u
inst✝ : Semiring R
p q : R[X]
n : ℕ
IH : (⇑derivative)^[n] (p * q) = ∑ k ∈ range n.succ, n.choose k • ((⇑derivative)^[n - k] p * (⇑derivative)^[k] q)
⊢ ∑ k ∈ range n, n.choose (k + 1) • ((⇑derivative)^[n - (k + 1) + 1] p * (⇑derivative)^[k + 1] q) =
    ∑ k ∈ range n.succ, n.choose k.succ • ((⇑derivative)^[n - k] p * (⇑derivative)^[k + 1] q)

Tactic:
rw [sum_range_succ, Nat.choose_succ_self, zero_smul, add_zero]
      refine sum_congr rfl fun k hk => ?_
      rw [mem_range] at hk
      congr
      lia

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

Goal state before:
pp: R : Type u
inst✝ : Semiring R
p : R[X]
n : ℕ
h : p.natDegree < n
⊢ (derivativeFinsupp p).support ⊆ range n

Tactic:
by
  dsimp [derivativeFinsupp]
  exact Finsupp.support_onFinset_subset.trans (Finset.range_subset_range.mpr h)

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

Goal state before:
pp: R : Type u
a : R
inst✝ : CommRing R
p : R[X]
h : X - C a ∣ p
⊢ p.IsRoot a

Tactic:
← modByMonic_eq_zero_iff_dvd (monic_X_sub_C _),

Goal state after:
R : Type u
a : R
inst✝ : CommRing R
p : R[X]
h : p %ₘ (X - C a) = 0
⊢ p.IsRoot a
Module: Mathlib.Order.Filter.CountablyGenerated

Goal state before:
pp: α✝ : Type u_1
β : Type u_2
γ : Type u_3
ι✝ : Type u_4
ι' : Sort u_5
ι : Sort u_6
α : Type u_7
inst✝¹ : Countable ι
f : ι → Filter α
inst✝ : ∀ (i : ι), (f i).IsCountablyGenerated
⊢ (⨅ i, f i).IsCountablyGenerated

Tactic:
by
  choose s hs using fun i => exists_antitone_basis (f i)
  rw [← PLift.down_surjective.iInf_comp]
  refine HasCountableBasis.isCountablyGenerated ⟨.iInf fun n => (hs _).1, ?_⟩
  refine (countable_range <| Sigma.map ((↑) : Finset (PLift ι) → Set (PLift ι)) fun _ => id).mono ?_
  rintro ⟨I, f⟩ ⟨hI, -⟩
  lift I to Finset (PLift ι) using hI
  exact ⟨⟨I, f⟩, rfl⟩

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

Goal state before:
pp: ι : Sort u_1
α : Type u_2
f : ι → Filter α
⊢ (⨆ i, f i).ker = ⋃ i, (f i).ker

Tactic:
refine subset_antisymm (fun x hx ↦ ?_) ker_mono.le_map_iSup

Goal state after:
ι : Sort u_1
α : Type u_2
f : ι → Filter α
x : α
hx : x ∈ (⨆ i, f i).ker
⊢ x ∈ ⋃ i, (f i).ker
Module: Mathlib.Algebra.Polynomial.Div

Goal state before:
pp: R : Type u
inst✝ : CommRing R
p : R[X]
t : R
hp : p ≠ 0
m : ℕ := rootMultiplicity t p
g : R[X] := p /ₘ (X - C t) ^ m
mul_eq : (X - C t) ^ m * g = p
⊢ eval (eval 0 (X + C t)) g = eval t g

Tactic:
eval_add,

Goal state after:
R : Type u
inst✝ : CommRing R
p : R[X]
t : R
hp : p ≠ 0
m : ℕ := rootMultiplicity t p
g : R[X] := p /ₘ (X - C t) ^ m
mul_eq : (X - C t) ^ m * g = p
⊢ eval (eval 0 X + eval 0 (C t)) g = eval t g
Module: Mathlib.Order.Filter.Prod

Goal state before:
pp: α : Type u_1
β : Type u_2
g : Filter β
⊢ ⊤ ⊓ comap Prod.snd g = comap Prod.snd g

Tactic:
top_inf_eq

Goal state after:
α : Type u_1
β : Type u_2
g : Filter β
⊢ comap Prod.snd g = comap Prod.snd g
Module: Mathlib.Algebra.Group.TypeTags.Pointwise

Goal state before:
pp: case zero
M : Type u_1
inst✝ : AddMonoid M
s : Set M
⊢ ⇑ofAdd '' (0 • s) = (⇑ofAdd '' s) ^ 0

Tactic:
simp; rfl

Goal state after:
Module: Mathlib.Algebra.Group.TypeTags.Pointwise

Goal state before:
pp: case zero
M : Type u_1
inst✝ : AddMonoid M
s : Set (Multiplicative M)
⊢ ⇑toAdd '' s ^ 0 = 0 • ⇑toAdd '' s

Tactic:
simp; rfl

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

Goal state before:
pp: α : Type u_2
s t : Set α
ht : t.Finite
⊢ cofinite ⊓ 𝓟 tᶜ ⊓ 𝓟 s = cofinite ⊓ 𝓟 s

Tactic:
ht.cofinite_inf_principal_compl

Goal state after:
α : Type u_2
s t : Set α
ht : t.Finite
⊢ cofinite ⊓ 𝓟 s = cofinite ⊓ 𝓟 s
Module: Mathlib.RingTheory.UniqueFactorizationDomain.Basic

Goal state before:
pp: α : Type u_1
inst✝¹ : CommMonoidWithZero α
inst✝ : IsCancelMulZero α
f : Multiset α
⊢ ∀ {g : Multiset α}, (∀ x ∈ f, Prime x) → (∀ x ∈ g, Prime x) → f.prod ~ᵤ g.prod → Multiset.Rel Associated f g

Tactic:
induction f using Multiset.induction_on with

Goal state after:
Module: Mathlib.RingTheory.UniqueFactorizationDomain.NormalizedFactors

Goal state before:
pp: case empty
α : Type u_1
inst✝² : CommMonoidWithZero α
inst✝¹ : NormalizationMonoid α
inst✝ : UniqueFactorizationMonoid α
hs : ∀ a ∈ 0, Irreducible a
⊢ normalizedFactors (Multiset.prod 0) = Multiset.map normalize 0

Tactic:
rw [Multiset.prod_zero, normalizedFactors_one, Multiset.map_zero]

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

Goal state before:
pp: R : Type u_1
S : Type u_2
inst✝³ : Semiring R
inst✝² : CommRing S
inst✝¹ : IsDomain S
inst✝ : DecidableEq S
m : R →+* S
d : ℕ
U : Set R
h : U.Finite
⊢ Set.Finite fun f ↦ f.natDegree ≤ d ∧ ∀ (i : ℕ), f.coeff i ∈ U

Tactic:
let π : R[X] → Fin (d + 1) → R := fun f i => f.coeff i

Goal state after:
R : Type u_1
S : Type u_2
inst✝³ : Semiring R
inst✝² : CommRing S
inst✝¹ : IsDomain S
inst✝ : DecidableEq S
m : R →+* S
d : ℕ
U : Set R
h : U.Finite
π : R[X] → Fin (d + 1) → R := fun f i ↦ f.coeff ↑i
⊢ Set.Finite fun f ↦ f.natDegree ≤ d ∧ ∀ (i : ℕ), f.coeff i ∈ U
Module: Mathlib.Algebra.Polynomial.FieldDivision

Goal state before:
pp: R : Type u
inst✝ : CommRing R
p : R[X]
t : R
⊢ eval t ((⇑derivative)^[rootMultiplicity t p] p) =
    (rootMultiplicity t p)! • eval t (p /ₘ (X - C t) ^ rootMultiplicity t p)

Tactic:
set m := p.rootMultiplicity t with hm

Goal state after:
R : Type u
inst✝ : CommRing R
p : R[X]
t : R
m : ℕ := rootMultiplicity t p
hm : m = rootMultiplicity t p
⊢ eval t ((⇑derivative)^[m] p) = m ! • eval t (p /ₘ (X - C t) ^ m)
Module: Mathlib.RingTheory.UniqueFactorizationDomain.FactorSet

Goal state before:
pp: α : Type u_1
inst✝ : CommMonoidWithZero α
p : Associates α
hp : Irreducible p
⊢ p ∈ ⊤

Tactic:
dsimp only [Membership.mem]; dsimp only [FactorSetMem]; split_ifs; exact trivial

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

Goal state before:
pp: R : Type u
inst✝² : CommRing R
inst✝¹ : NoZeroDivisors R
inst✝ : CharZero R
f g : R[X]
hf0 : f ≠ 0
a : R
haf : f.IsRoot a
r : R[X]
hr : derivative f * g = f * r
hdf0 : derivative f ≠ 0
hg : ¬g.IsRoot a
hdfg0 : derivative f * g ≠ 0
hr' : rootMultiplicity a (derivative f * g) = rootMultiplicity a (f * r)
this : IsDomain R
⊢ False

Tactic:
rw [rootMultiplicity_mul hdfg0, derivative_rootMultiplicity_of_root haf,
    rootMultiplicity_eq_zero hg, add_zero, rootMultiplicity_mul (hr ▸ hdfg0), add_comm,
    Nat.sub_eq_iff_eq_add (Nat.succ_le_iff.2 ((rootMultiplicity_pos hf0).2 haf))] at hr'

Goal state after:
R : Type u
inst✝² : CommRing R
inst✝¹ : NoZeroDivisors R
inst✝ : CharZero R
f g : R[X]
hf0 : f ≠ 0
a : R
haf : f.IsRoot a
r : R[X]
hr : derivative f * g = f * r
hdf0 : derivative f ≠ 0
hg : ¬g.IsRoot a
hdfg0 : derivative f * g ≠ 0
hr' : rootMultiplicity a f = rootMultiplicity a r + rootMultiplicity a f + Nat.succ 0
this : IsDomain R
⊢ False
Module: Mathlib.Algebra.Polynomial.FieldDivision

Goal state before:
pp: R : Type u
inst✝ : Field R
p q : R[X]
hq0 : q ≠ 0
h : p.degree < q.degree
hlt : p.degree < (q * C q.leadingCoeff⁻¹).degree
hm : (q * C q.leadingCoeff⁻¹).Monic
⊢ C q.leadingCoeff⁻¹ * (p /ₘ (q * C q.leadingCoeff⁻¹)) = 0

Tactic:
(divByMonic_eq_zero_iff hm).2 hlt,

Goal state after:
R : Type u
inst✝ : Field R
p q : R[X]
hq0 : q ≠ 0
h : p.degree < q.degree
hlt : p.degree < (q * C q.leadingCoeff⁻¹).degree
hm : (q * C q.leadingCoeff⁻¹).Monic
⊢ C q.leadingCoeff⁻¹ * 0 = 0
Module: Mathlib.RingTheory.UniqueFactorizationDomain.FactorSet

Goal state before:
pp: case refine_2
α : Type u_1
inst✝¹ : CommMonoidWithZero α
inst✝ : UniqueFactorizationMonoid α
a b : α
ha : a ≠ 0
hb : b ≠ 0
h : Associates.mk a ⊓ Associates.mk b ≠ 1
hz : ↑(factors' a ⊓ factors' b) ≠ 0
p : α
p0_irr : Irreducible (Associates.mk p)
p0_mem : ⟨Associates.mk p, p0_irr⟩ ∈ factors' a ∩ factors' b
⊢ p ∣ a

Tactic:
apply dvd_of_mk_le_mk
    apply dvd_of_mem_factors' (Multiset.mem_inter.mp p0_mem).left
    apply ha

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

Goal state before:
pp: K : Type u_1
inst✝ : Field K
f : K[X]
a : K
h : X - C a ∣ f /ₘ (X - C a)
this : X - C a ∣ derivative f
⊢ eval a (derivative f) = 0

Tactic:
← modByMonic_eq_zero_iff_dvd (monic_X_sub_C _),

Goal state after:
K : Type u_1
inst✝ : Field K
f : K[X]
a : K
h : X - C a ∣ f /ₘ (X - C a)
this : derivative f %ₘ (X - C a) = 0
⊢ eval a (derivative f) = 0
Module: Mathlib.Algebra.AlgebraicCard

Goal state before:
pp: R : Type u
A : Type v
inst✝⁵ : CommRing R
inst✝⁴ : IsDomain R
inst✝³ : CommRing A
inst✝² : IsDomain A
inst✝¹ : Algebra R A
inst✝ : Module.IsTorsionFree R A
g : ↑{x | IsAlgebraic R x} → R[X]
hg₁ : ∀ (x : ↑{x | IsAlgebraic R x}), g x ≠ 0
hg₂ : ∀ (x : ↑{x | IsAlgebraic R x}), (aeval ↑x) (g x) = 0
f : R[X]
⊢ lift.{u, v} #↑(g ⁻¹' {f}) ≤ ℵ₀

Tactic:
lift_le_aleph0,

Goal state after:
R : Type u
A : Type v
inst✝⁵ : CommRing R
inst✝⁴ : IsDomain R
inst✝³ : CommRing A
inst✝² : IsDomain A
inst✝¹ : Algebra R A
inst✝ : Module.IsTorsionFree R A
g : ↑{x | IsAlgebraic R x} → R[X]
hg₁ : ∀ (x : ↑{x | IsAlgebraic R x}), g x ≠ 0
hg₂ : ∀ (x : ↑{x | IsAlgebraic R x}), (aeval ↑x) (g x) = 0
f : R[X]
⊢ #↑(g ⁻¹' {f}) ≤ ℵ₀
Module: Mathlib.RingTheory.UniqueFactorizationDomain.FactorSet

Goal state before:
pp: case h
α : Type u_1
inst✝³ : CommMonoidWithZero α
inst✝² : UniqueFactorizationMonoid α
inst✝¹ : DecidableEq (Associates α)
inst✝ : (p : Associates α) → Decidable (Irreducible p)
k : ℕ
a✝ : Nontrivial α
a0 : α
hz : a0 ≠ 0
ha : Associates.mk a0 ≠ 0
hk : ∀ (p : Associates α), Irreducible p → k ∣ p.count ↑(factors' a0)
hk' : ∀ p ∈ factors' a0, k ∣ Multiset.count p (factors' a0)
u : Multiset { a // Irreducible a }
hu : factors' a0 = k • u
⊢ (Associates.mk a0).factors = (FactorSet.prod ↑u ^ k).factors

Tactic:
pow_factors,

Goal state after:
case h
α : Type u_1
inst✝³ : CommMonoidWithZero α
inst✝² : UniqueFactorizationMonoid α
inst✝¹ : DecidableEq (Associates α)
inst✝ : (p : Associates α) → Decidable (Irreducible p)
k : ℕ
a✝ : Nontrivial α
a0 : α
hz : a0 ≠ 0
ha : Associates.mk a0 ≠ 0
hk : ∀ (p : Associates α), Irreducible p → k ∣ p.count ↑(factors' a0)
hk' : ∀ p ∈ factors' a0, k ∣ Multiset.count p (factors' a0)
u : Multiset { a // Irreducible a }
hu : factors' a0 = k • u
⊢ (Associates.mk a0).factors = k • (FactorSet.prod ↑u).factors
Module: Mathlib.RingTheory.Algebraic.Basic

Goal state before:
pp: case inr
R : Type u
S : Type u_1
inst✝⁴ : CommRing R
inst✝³ : CommRing S
inst✝² : Algebra R S
inst✝¹ : Nontrivial R
M : Submonoid R
inst✝ : IsLocalization M S
x : S
hx : x ≠ 0
r : R
m : ↥M
h : x * (algebraMap R S) ↑(r, m).2 = (algebraMap R S) (r, m).1
eq : C ↑m * X - C r = 0
⊢ x = 0

Tactic:
rwa [← eq_mk'_iff_mul_eq, show r = 0 by simpa using congr(coeff $eq 0), mk'_zero] at h

Goal state after:
Module: Mathlib.Algebra.Central.End

Goal state before:
pp: R : Type u_1
S : Type u_2
M : Type u_3
inst✝¹⁴ : Semiring R
inst✝¹³ : AddCommMonoid M
inst✝¹² : Module R M
inst✝¹¹ : Free R M
inst✝¹⁰ : CommSemiring S
inst✝⁹ : Module S M
inst✝⁸ : SMulCommClass R S M
inst✝⁷ : Algebra S R
inst✝⁶ : IsScalarTower S R M
M₂ : Type u_4
inst✝⁵ : AddCommMonoid M₂
inst✝⁴ : Module R M₂
inst✝³ : Module S M₂
inst✝² : SMulCommClass R S M₂
inst✝¹ : IsScalarTower S R M₂
inst✝ : Algebra.IsCentral S R
f g : M ≃ₗ[R] M₂
⊢ ↑g.symm ∘ₗ ↑f ∈ Set.range ⇑(algebraMap S (End R M)) ↔ ∃ α, ⇑f = α • ⇑g

Tactic:
Set.mem_range,

Goal state after:
R : Type u_1
S : Type u_2
M : Type u_3
inst✝¹⁴ : Semiring R
inst✝¹³ : AddCommMonoid M
inst✝¹² : Module R M
inst✝¹¹ : Free R M
inst✝¹⁰ : CommSemiring S
inst✝⁹ : Module S M
inst✝⁸ : SMulCommClass R S M
inst✝⁷ : Algebra S R
inst✝⁶ : IsScalarTower S R M
M₂ : Type u_4
inst✝⁵ : AddCommMonoid M₂
inst✝⁴ : Module R M₂
inst✝³ : Module S M₂
inst✝² : SMulCommClass R S M₂
inst✝¹ : IsScalarTower S R M₂
inst✝ : Algebra.IsCentral S R
f g : M ≃ₗ[R] M₂
⊢ (∃ y, (algebraMap S (End R M)) y = ↑g.symm ∘ₗ ↑f) ↔ ∃ α, ⇑f = α • ⇑g
Module: Mathlib.Algebra.Central.End

Goal state before:
pp: R : Type u_1
M : Type u_3
inst✝¹⁶ : Semiring R
inst✝¹⁵ : AddCommMonoid M
inst✝¹⁴ : Module R M
inst✝¹³ : Free R M
S : Type u_4
M₂ : Type u_5
inst✝¹² : CommRing S
inst✝¹¹ : IsCancelMulZero S
inst✝¹⁰ : Module S M
inst✝⁹ : SMulCommClass R S M
inst✝⁸ : Algebra S R
inst✝⁷ : IsScalarTower S R M
inst✝⁶ : AddCommGroup M₂
inst✝⁵ : Module R M₂
inst✝⁴ : Module S M₂
inst✝³ : SMulCommClass R S M₂
inst✝² : IsScalarTower S R M₂
inst✝¹ : Algebra.IsCentral S R
inst✝ : IsTorsionFree S M₂
f g : M ≃ₗ[R] M₂
h : conjAlgEquiv S f = conjAlgEquiv S g
h✝ : Subsingleton M
x✝ : M
⊢ f x✝ = (1 • g) x✝

Tactic:
simp [Subsingleton.eq_zero (α := M)]

Goal state after:
Module: Mathlib.Algebra.Central.End

Goal state before:
pp: R : Type u_1
M : Type u_3
inst✝¹⁶ : Semiring R
inst✝¹⁵ : AddCommMonoid M
inst✝¹⁴ : Module R M
inst✝¹³ : Free R M
S : Type u_4
M₂ : Type u_5
inst✝¹² : CommRing S
inst✝¹¹ : IsCancelMulZero S
inst✝¹⁰ : Module S M
inst✝⁹ : SMulCommClass R S M
inst✝⁸ : Algebra S R
inst✝⁷ : IsScalarTower S R M
inst✝⁶ : AddCommGroup M₂
inst✝⁵ : Module R M₂
inst✝⁴ : Module S M₂
inst✝³ : SMulCommClass R S M₂
inst✝² : IsScalarTower S R M₂
inst✝¹ : Algebra.IsCentral S R
inst✝ : IsTorsionFree S M₂
f g : M ≃ₗ[R] M₂
h : conjAlgEquiv S f = conjAlgEquiv S g
h✝ : Nontrivial M
α : S
hα : ⇑f = α • ⇑g
β : S
hβ : ⇑g = β • ⇑f
x : M
hx : x ≠ 0
this : 1 = α * β
x✝ : M
⊢ f x✝ = ({ val := α, inv := β, val_inv := ⋯, inv_val := ⋯ } • g) x✝

Tactic:
by simpa using congr($hα _)

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

Goal state before:
pp: R : Type u
inst✝² : CommRing R
K : Type u_2
inst✝¹ : Field K
inst✝ : Algebra R K
x : K
⊢ IsAlgebraic R x⁻¹ ↔ IsAlgebraic R x

Tactic:
by
  by_cases hx : x = 0
  · simp [hx]
  let := invertibleOfNonzero hx
  exact IsAlgebraic.invOf_iff (R := R) (x := x)

Goal state after:
Module: Mathlib.Order.DirectedInverseSystem

Goal state before:
pp: case inl
ι✝ : Type u_1
inst✝¹ : Preorder ι✝
F₁ : ι✝ → Type u_2
F₂ : ι✝ → Type u_3
F : ι✝ → Type u_4
X✝ : ι✝ → Type u_5
f✝ : ⦃i j : ι✝⦄ → i ≤ j → F j → F i
i✝ j✝ : ι✝
h : i✝ ≤ j✝
ι : Type u_6
inst✝ : LinearOrder ι
X : ι → Type u_7
i : ι
hi : IsSuccPrelimit i
f : ↑(limit piLTProj i)
j : ↑(Iio i)
l : ↑(Iio ↑j)
k : ↑(Ioo (↑l) i) := hi.mid ⋯
le : j ≤ ⟨↑k, ⋯⟩
⊢ ↑((fun f ↦ ⟨fun j ↦ piLTProj ⋯ f, ⋯⟩)
          ((fun f l ↦
              let k := hi.mid ⋯;
              ↑f ⟨↑k, ⋯⟩ ⟨↑l, ⋯⟩)
            f))
      j l =
    ↑f j l

pp: case inr
ι✝ : Type u_1
inst✝¹ : Preorder ι✝
F₁ : ι✝ → Type u_2
F₂ : ι✝ → Type u_3
F : ι✝ → Type u_4
X✝ : ι✝ → Type u_5
f✝ : ⦃i j : ι✝⦄ → i ≤ j → F j → F i
i✝ j✝ : ι✝
h : i✝ ≤ j✝
ι : Type u_6
inst✝ : LinearOrder ι
X : ι → Type u_7
i : ι
hi : IsSuccPrelimit i
f : ↑(limit piLTProj i)
j : ↑(Iio i)
l : ↑(Iio ↑j)
k : ↑(Ioo (↑l) i) := hi.mid ⋯
le : ⟨↑k, ⋯⟩ ≤ j
⊢ ↑((fun f ↦ ⟨fun j ↦ piLTProj ⋯ f, ⋯⟩)
          ((fun f l ↦
              let k := hi.mid ⋯;
              ↑f ⟨↑k, ⋯⟩ ⟨↑l, ⋯⟩)
            f))
      j l =
    ↑f j l

Tactic:
exacts [congr_fun (f.2 le) l, (congr_fun (f.2 le) ⟨l, _⟩).symm]

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

Goal state before:
pp: R : Type u_1
inst✝⁶ : Semiring R
ι : Type u_2
inst✝⁵ : Preorder ι
G : ι → Type u_3
inst✝⁴ : (i : ι) → AddCommMonoid (G i)
inst✝³ : (i : ι) → Module R (G i)
f : (i j : ι) → i ≤ j → G i →ₗ[R] G j
inst✝² : DecidableEq ι
inst✝¹ : DirectedSystem G fun x1 x2 x3 ↦ ⇑(f x1 x2 x3)
inst✝ : IsDirectedOrder ι
i : ι
x : G i
H : (of R ι G f i) x = 0
⊢ ∃ j, ∃ (hij : i ≤ j), (f i j hij) x = 0

Tactic:
convert! exists_eq_of_of_eq (H.trans (map_zero <| _).symm)

Goal state after:
R : Type u_1
inst✝⁶ : Semiring R
ι : Type u_2
inst✝⁵ : Preorder ι
G : ι → Type u_3
inst✝⁴ : (i : ι) → AddCommMonoid (G i)
inst✝³ : (i : ι) → Module R (G i)
f : (i j : ι) → i ≤ j → G i →ₗ[R] G j
inst✝² : DecidableEq ι
inst✝¹ : DirectedSystem G fun x1 x2 x3 ↦ ⇑(f x1 x2 x3)
inst✝ : IsDirectedOrder ι
i : ι
x : G i
H : (of R ι G f i) x = 0
x✝¹ : ι
x✝ : i ≤ x✝¹
⊢ 0 = (f i x✝¹ x✝) 0
Module: Mathlib.LinearAlgebra.TensorProduct.RightExactness

Goal state before:
pp: case a.refine_4.add
R : Type u_1
inst✝⁴ : CommSemiring R
A : Type u_2
B : Type u_3
inst✝³ : Semiring A
inst✝² : Semiring B
inst✝¹ : Algebra R A
inst✝ : Algebra R B
I : Ideal A
x✝ : A ⊗[R] B
hx : x✝ ∈ ↑(Submodule.restrictScalars R (Submodule.span (A ⊗[R] B) (⇑includeLeft '' ↑I)))
x : ↥(Submodule.restrictScalars R I) ⊗[R] B
a b : A ⊗[R] B
ha :
  ∃ y,
    (LinearMap.rTensor B (Submodule.restrictScalars R I).subtype) y =
      a • (LinearMap.rTensor B (Submodule.restrictScalars R I).subtype) x
hb :
  ∃ y,
    (LinearMap.rTensor B (Submodule.restrictScalars R I).subtype) y =
      b • (LinearMap.rTensor B (Submodule.restrictScalars R I).subtype) x
⊢ ∃ y,
    (LinearMap.rTensor B (Submodule.restrictScalars R I).subtype) y =
      (a + b) • (LinearMap.rTensor B (Submodule.restrictScalars R I).subtype) x

Tactic:
| add a b ha hb =>

Goal state after:
Module: Mathlib.LinearAlgebra.TensorProduct.RightExactness

Goal state before:
pp: case a.refine_4.add
R : Type u_1
inst✝⁴ : CommSemiring R
A : Type u_2
B : Type u_3
inst✝³ : Semiring A
inst✝² : Semiring B
inst✝¹ : Algebra R A
inst✝ : Algebra R B
I : Ideal B
x✝ : A ⊗[R] B
hx : x✝ ∈ ↑(Submodule.restrictScalars R (Submodule.span (A ⊗[R] B) (⇑includeRight '' ↑I)))
x : A ⊗[R] ↥(Submodule.restrictScalars R I)
a b : A ⊗[R] B
ha :
  ∃ y,
    (LinearMap.lTensor A (Submodule.restrictScalars R I).subtype) y =
      a • (LinearMap.lTensor A (Submodule.restrictScalars R I).subtype) x
hb :
  ∃ y,
    (LinearMap.lTensor A (Submodule.restrictScalars R I).subtype) y =
      b • (LinearMap.lTensor A (Submodule.restrictScalars R I).subtype) x
⊢ ∃ y,
    (LinearMap.lTensor A (Submodule.restrictScalars R I).subtype) y =
      (a + b) • (LinearMap.lTensor A (Submodule.restrictScalars R I).subtype) x

Tactic:
| add a b ha hb =>

Goal state after:
Module: Mathlib.Algebra.Colimit.DirectLimit

Goal state before:
pp: ι : Type u_2
inst✝⁹ : Preorder ι
G : ι → Type u_3
H : ι → Type u_4
C : Type u_5
T : ⦃i j : ι⦄ → i ≤ j → Type u_6
f : (x x_1 : ι) → (h : x ≤ x_1) → T h
inst✝⁸ : (i j : ι) → (h : i ≤ j) → FunLike (T h) (G i) (G j)
inst✝⁷ : (i : ι) → FunLike (H i) (G i) C
inst✝⁶ : DirectedSystem G fun x1 x2 x3 ↦ ⇑(f x1 x2 x3)
inst✝⁵ : IsDirectedOrder ι
inst✝⁴ : Nonempty ι
inst✝³ : (i : ι) → One (G i)
inst✝² : One C
inst✝¹ : ∀ (i : ι), OneHomClass (H i) (G i) C
inst✝ : ∀ (i j : ι) (h : i ≤ j), OneHomClass (T h) (G i) (G j)
g : (i : ι) → H i
h : ∀ (i j : ι) (h : i ≤ j) (x : G i), (g i) x = (g j) ((f i j h) x)
i : ι
⊢ (g ⟨?m.94, 1⟩.fst) ⟨?m.94, 1⟩.snd = 1

pp: ι : Type u_2
inst✝⁹ : Preorder ι
G : ι → Type u_3
H : ι → Type u_4
C : Type u_5
T : ⦃i j : ι⦄ → i ≤ j → Type u_6
f : (x x_1 : ι) → (h : x ≤ x_1) → T h
inst✝⁸ : (i j : ι) → (h : i ≤ j) → FunLike (T h) (G i) (G j)
inst✝⁷ : (i : ι) → FunLike (H i) (G i) C
inst✝⁶ : DirectedSystem G fun x1 x2 x3 ↦ ⇑(f x1 x2 x3)
inst✝⁵ : IsDirectedOrder ι
inst✝⁴ : Nonempty ι
inst✝³ : (i : ι) → One (G i)
inst✝² : One C
inst✝¹ : ∀ (i : ι), OneHomClass (H i) (G i) C
inst✝ : ∀ (i j : ι) (h : i ≤ j), OneHomClass (T h) (G i) (G j)
g : (i : ι) → H i
h : ∀ (i j : ι) (h : i ≤ j) (x : G i), (g i) x = (g j) ((f i j h) x)
i : ι
⊢ ι

Tactic:
map_one (g i)

Goal state after:
ι : Type u_2
inst✝⁹ : Preorder ι
G : ι → Type u_3
H : ι → Type u_4
C : Type u_5
T : ⦃i j : ι⦄ → i ≤ j → Type u_6
f : (x x_1 : ι) → (h : x ≤ x_1) → T h
inst✝⁸ : (i j : ι) → (h : i ≤ j) → FunLike (T h) (G i) (G j)
inst✝⁷ : (i : ι) → FunLike (H i) (G i) C
inst✝⁶ : DirectedSystem G fun x1 x2 x3 ↦ ⇑(f x1 x2 x3)
inst✝⁵ : IsDirectedOrder ι
inst✝⁴ : Nonempty ι
inst✝³ : (i : ι) → One (G i)
inst✝² : One C
inst✝¹ : ∀ (i : ι), OneHomClass (H i) (G i) C
inst✝ : ∀ (i j : ι) (h : i ≤ j), OneHomClass (T h) (G i) (G j)
g : (i : ι) → H i
h : ∀ (i j : ι) (h : i ≤ j) (x : G i), (g i) x = (g j) ((f i j h) x)
i : ι
⊢ 1 = 1