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

Goal state before:
pp: k : Type u_1
G : Type u_2
inst✝¹ : Semiring k
inst✝ : AddCommMonoid G
g : G
x : k[G]
⊢ of' k G g * x %ᵒᶠ g = 0

Tactic:
by
  ext g'
  simp only [of'_apply, coeff_zero, Finsupp.coe_zero, Pi.zero_apply]
  obtain ⟨d, rfl⟩ | h := em (∃ d, g' = g + d)
  · rw [coeff_modOf_self_add]
  · rw [coeff_modOf_of_not_exists_add _ _ _ h, coeff_single_mul_of_forall_add_ne]
    simpa [eq_comm] using h

Goal state after:
Module: Mathlib.GroupTheory.OrderOfElement

Goal state before:
pp: G : Type u_6
inst✝ : Group G
a : G
n : ℕ
⊢ a ^ (n % Nat.card G % orderOf a) = a ^ (n % Nat.card G)

Tactic:
pow_mod_orderOf

Goal state after:
G : Type u_6
inst✝ : Group G
a : G
n : ℕ
⊢ a ^ (n % Nat.card G) = a ^ (n % Nat.card G)
Module: Mathlib.GroupTheory.OrderOfElement

Goal state before:
pp: G✝ : Type u_1
H : Type u_2
A : Type u_3
α : Type u_4
β : Type u_5
G : Type u_6
inst✝¹ : Group G
inst✝ : Fintype G
S : Set G
hS : S.Nonempty
one_mem : 1 ∈ S ^ card G
⊢ S ^ card G * S ^ card G = S ^ card G

Tactic:
apply (Set.eq_of_subset_of_card_le (Set.subset_mul_left _ one_mem) (ge_of_eq _)).symm

Goal state after:
G✝ : Type u_1
H : Type u_2
A : Type u_3
α : Type u_4
β : Type u_5
G : Type u_6
inst✝¹ : Group G
inst✝ : Fintype G
S : Set G
hS : S.Nonempty
one_mem : 1 ∈ S ^ card G
⊢ card ↑(S ^ card G) = card ↑(S ^ card G * S ^ card G)
Module: Mathlib.Algebra.Polynomial.Expand

Goal state before:
pp: case neg
R : Type u
inst✝¹ : CommSemiring R
S : Type v
inst✝ : CommSemiring S
p : ℕ
f : R →+* S
q : R[X]
hp : ¬p = 0
n✝ : ℕ
⊢ (map f ((expand R p) q)).coeff n✝ = ((expand S p) (map f q)).coeff n✝

Tactic:
coeff_map,

Goal state after:
case neg
R : Type u
inst✝¹ : CommSemiring R
S : Type v
inst✝ : CommSemiring S
p : ℕ
f : R →+* S
q : R[X]
hp : ¬p = 0
n✝ : ℕ
⊢ f (((expand R p) q).coeff n✝) = ((expand S p) (map f q)).coeff n✝
Module: Mathlib.Algebra.Polynomial.Expand

Goal state before:
pp: case refine_1
R : Type u
inst✝¹ : CommSemiring R
p : ℕ
inst✝ : ExpChar R p
f a b : R[X]
ha : map (frobenius R p) ((expand R p) a) = a ^ p
hb : map (frobenius R p) ((expand R p) b) = b ^ p
⊢ a ^ p + map (frobenius R p) ((expand R p) b) = (a + b) ^ p

Tactic:
hb,

Goal state after:
case refine_1
R : Type u
inst✝¹ : CommSemiring R
p : ℕ
inst✝ : ExpChar R p
f a b : R[X]
ha : map (frobenius R p) ((expand R p) a) = a ^ p
hb : map (frobenius R p) ((expand R p) b) = b ^ p
⊢ a ^ p + b ^ p = (a + b) ^ p
Module: Mathlib.Order.Filter.CountablyGenerated

Goal state before:
pp: α : Type u_1
ι : Type u_4
inst✝ : CompleteLattice α
B : Set ι
Bcbl : B.Countable
f : ι → α
i₀ : ι
h : f i₀ = ⊤
⊢ ∃ x, ⨅ t ∈ B, f t = ⨅ i, f (x i)

Tactic:
by
  rcases B.eq_empty_or_nonempty with hB | Bnonempty
  · rw [hB, iInf_emptyset]
    use fun _ => i₀
    simp [h]
  · exact countable_biInf_eq_iInf_seq Bcbl Bnonempty f

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

Goal state before:
pp: α : Type u_1
ι : Type u_4
inst✝ : Preorder ι
l : Filter α
s : ι → Set α
hs : l.HasAntitoneBasis s
t : Set α
⊢ (∃ i, True ∧ s i ⊆ t) ↔ ∃ i, s i ⊆ t

Tactic:
by simp only [true_and]

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

Goal state before:
pp: R : Type u
inst✝ : CommSemiring R
n k : ℕ
⊢ (⇑derivative)^[k] (X ^ n) = ↑(n.descFactorial k) * X ^ (n - k)

Tactic:
induction k with
  | zero =>
    rw [Function.iterate_zero_apply, tsub_zero, Nat.descFactorial_zero, Nat.cast_one, one_mul]
  | succ k ih =>
    rw [Function.iterate_succ_apply', ih, derivative_natCast_mul, derivative_X_pow, C_eq_natCast,
      Nat.descFactorial_succ, Nat.sub_sub, Nat.cast_mul]
    simp [mul_assoc, mul_left_comm]

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

Goal state before:
pp: case mp
ι : Type u_1
α : ι → Type u_2
f : (i : ι) → Filter (α i)
s : Set ((i : ι) → α i)
⊢ s ∈ pi f → ∃ I, I.Finite ∧ ∃ t, (∀ (i : ι), t i ∈ f i) ∧ I.pi t ⊆ s

pp: case mpr
ι : Type u_1
α : ι → Type u_2
f : (i : ι) → Filter (α i)
s : Set ((i : ι) → α i)
⊢ (∃ I, I.Finite ∧ ∃ t, (∀ (i : ι), t i ∈ f i) ∧ I.pi t ⊆ s) → s ∈ pi f

Tactic:
· simp only [pi, mem_iInf', mem_comap, pi_def]
    rintro ⟨I, If, V, hVf, -, rfl, -⟩
    choose t htf htV using hVf
    exact ⟨I, If, t, htf, iInter₂_mono fun i _ => htV i⟩

Goal state after:
case mpr
ι : Type u_1
α : ι → Type u_2
f : (i : ι) → Filter (α i)
s : Set ((i : ι) → α i)
⊢ (∃ I, I.Finite ∧ ∃ t, (∀ (i : ι), t i ∈ f i) ∧ I.pi t ⊆ s) → s ∈ pi f
Module: Mathlib.Order.Filter.Finite

Goal state before:
pp: case mp
α : Type u
ι : Type u_2
p : ι → Prop
s : ι → Set α
t : Set α
⊢ t ∈ ⨅ i, ⨅ (_ : p i), 𝓟 (s i) → ∃ I, I.Finite ∧ (∀ i ∈ I, p i) ∧ ⋂ i ∈ I, s i ⊆ t

pp: case mpr
α : Type u
ι : Type u_2
p : ι → Prop
s : ι → Set α
t : Set α
⊢ (∃ I, I.Finite ∧ (∀ i ∈ I, p i) ∧ ⋂ i ∈ I, s i ⊆ t) → t ∈ ⨅ i, ⨅ (_ : p i), 𝓟 (s i)

Tactic:
· simp only [mem_iInf (ι := ι), mem_iInf_of_finite, mem_principal]
    rintro ⟨I, hIf, V, hV₁, hV₂, rfl⟩
    choose! t ht₁ ht₂ using hV₁
    refine ⟨I ∩ {i | p i}, hIf.inter_of_left _, fun i ↦ And.right, ?_⟩
    simp only [mem_inter_iff, iInter_and, biInter_eq_iInter, ht₂, mem_ofPred_eq]
    gcongr with i hpi
    exact ht₁ i hpi

Goal state after:
case mpr
α : Type u
ι : Type u_2
p : ι → Prop
s : ι → Set α
t : Set α
⊢ (∃ I, I.Finite ∧ (∀ i ∈ I, p i) ∧ ⋂ i ∈ I, s i ⊆ t) → t ∈ ⨅ i, ⨅ (_ : p i), 𝓟 (s i)
Module: Mathlib.Algebra.Polynomial.Div

Goal state before:
pp: K : Type u_1
inst✝ : Field K
p q : K[X]
hpq : p ∣ q
h₁ : p.degree = q.degree
hq : q = 0
⊢ p = q

Tactic:
simpa [hq] using h₁

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

Goal state before:
pp: case refine_4.refine_2
α : Type u_2
f : Filter α
q : Set α × Filter α
hq : (fun p ↦ p.2 ≤ cofinite ∧ Disjoint (𝓟 p.1) p.2 ∧ f = 𝓟 p.1 ⊔ p.2) q
hqk : f.ker = q.1
⊢ q.2 ≤ ￢f

Tactic:
rw [Filter.hnot_def, le_principal_iff, ← disjoint_principal_left, hqk]
      exact hq.2.1

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

Goal state before:
pp: α : Type u_1
β : Type u_2
f : α → β
inst✝ : TendstoCofinite f
s : Set β
hs : s.Finite
⊢ univ \ s ∈ cofinite

Tactic:
simpa [compl_eq_univ_sdiff]

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

Goal state before:
pp: α : Type u_1
β : Type u_2
f : α → β
inst✝ : TendstoCofinite f
s : Set β
hs : s.Finite
⊢ (f ⁻¹' s).Finite

Tactic:
simpa [compl_eq_univ_sdiff] using TendstoCofinite.tendsto_cofinite f
    (show univ \ s ∈ cofinite by simpa [compl_eq_univ_sdiff])

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

Goal state before:
pp: α : Type u_1
inst✝¹ : CommMonoidWithZero α
inst✝ : IsCancelMulZero α
g : Multiset α
a✝ : ∀ x ∈ 0, Prime x
hg : ∀ x ∈ g, Prime x
h : Multiset.prod 0 ~ᵤ g.prod
x : α
hx : x ∈ g
⊢ IsUnit g.prod

Tactic:
by simpa [associated_one_iff_isUnit] using h.symm

Goal state after:
Module: Mathlib.Algebra.BigOperators.Associated

Goal state before:
pp: M : Type u_2
inst✝ : CommMonoid M
p q : Multiset M
⊢ Multiset.Rel Associated p q ↔ Multiset.map Associates.mk p = Multiset.map Associates.mk q

Tactic:
rw [← Multiset.rel_eq, Multiset.rel_map]

Goal state after:
M : Type u_2
inst✝ : CommMonoid M
p q : Multiset M
⊢ Multiset.Rel Associated p q ↔ Multiset.Rel (fun a b ↦ Associates.mk a = Associates.mk b) p q
Module: Mathlib.RingTheory.UniqueFactorizationDomain.Basic

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

Tactic:
intro g hf hg hfg
    let ⟨b, hbg, hb⟩ :=
      (exists_associated_mem_of_dvd_prod (hf p (by simp)) fun q hq => hg _ hq) <|
        hfg.dvd_iff_dvd_right.1 (show p ∣ (p ::ₘ f).prod by simp)
    have := Classical.decEq α
    rw [← Multiset.cons_erase hbg]
    exact
      Multiset.Rel.cons hb
        (ih (fun q hq => hf _ (by simp [hq]))
          (fun {q} (hq : q ∈ g.erase b) => hg q (Multiset.mem_of_mem_erase hq))
          (Associated.of_mul_left
            (by rwa [← Multiset.prod_cons, ← Multiset.prod_cons, Multiset.cons_erase hbg]) hb
            (hf p (by simp)).ne_zero))

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

Goal state before:
pp: case a
M : Type u_2
inst✝² : CommMonoidWithZero M
inst✝¹ : UniqueFactorizationMonoid M
inst✝ : Subsingleton Mˣ
x p : M
a✝ : p ∈ factors x
⊢ normalize p = id p

Tactic:
exact normalize_eq p

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

Goal state before:
pp: R : Type u
inst✝¹ : CommRing R
inst✝ : IsDomain R
p q : R[X]
h : {x | eval x p = eval x q}.Infinite
⊢ p - q = 0

Tactic:
apply eq_zero_of_infinite_isRoot

Goal state after:
R : Type u
inst✝¹ : CommRing R
inst✝ : IsDomain R
p q : R[X]
h : {x | eval x p = eval x q}.Infinite
⊢ {x | (p - q).IsRoot x}.Infinite
Module: Mathlib.Algebra.Polynomial.Roots

Goal state before:
pp: R : Type u
inst✝¹ : CommRing R
inst✝ : IsDomain R
p : R[X]
a b : R
ha : IsUnit a
⊢ Multiset.map (fun x ↦ a * x + b) (p.comp (C a * X + C b)).roots = p.roots

Tactic:
set f := fun x ↦ a * x + b

Goal state after:
R : Type u
inst✝¹ : CommRing R
inst✝ : IsDomain R
p : R[X]
a b : R
ha : IsUnit a
f : R → R := fun x ↦ a * x + b
⊢ Multiset.map f (p.comp (C a * X + C b)).roots = p.roots
Module: Mathlib.RingTheory.UniqueFactorizationDomain.NormalizedFactors

Goal state before:
pp: α : Type u_1
inst✝² : CommMonoidWithZero α
inst✝¹ : NormalizationMonoid α
inst✝ : UniqueFactorizationMonoid α
x y : α
hx : x ≠ 0
hy : y ≠ 0
⊢ DvdNotUnit x y ↔ normalizedFactors x < normalizedFactors y

Tactic:
by
  constructor
  · rintro ⟨_, c, hc, rfl⟩
    simp only [hx, right_ne_zero_of_mul hy, normalizedFactors_mul, Ne, not_false_iff,
      lt_add_iff_pos_right, normalizedFactors_pos, hc]
  · intro h
    exact
      dvdNotUnit_of_dvd_of_not_dvd
        ((dvd_iff_normalizedFactors_le_normalizedFactors hx hy).mpr h.le)
        (mt (dvd_iff_normalizedFactors_le_normalizedFactors hy hx).mp h.not_ge)

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

Goal state before:
pp: α : Type u_1
inst✝¹ : CommMonoidWithZero α
inst✝ : UniqueFactorizationMonoid α
⊢ (if 1 = 0 then 0 else (map (Classical.choose ⋯) (normalizedFactors 1)).prod) = 1

Tactic:
nontriviality α

Goal state after:
α : Type u_1
inst✝¹ : CommMonoidWithZero α
inst✝ : UniqueFactorizationMonoid α
a✝ : Nontrivial α
⊢ (if 1 = 0 then 0 else (map (Classical.choose ⋯) (normalizedFactors 1)).prod) = 1
Module: Mathlib.RingTheory.Polynomial.Content

Goal state before:
pp: R : Type u_1
inst✝¹ : CommRing R
inst✝ : NormalizedGCDMonoid R
p : R[X]
⊢ (X * p).support.gcd (X * p).coeff = p.support.gcd p.coeff

Tactic:
Finset.gcd_def,

Goal state after:
R : Type u_1
inst✝¹ : CommRing R
inst✝ : NormalizedGCDMonoid R
p : R[X]
⊢ (Multiset.map (X * p).coeff (X * p).support.val).gcd = p.support.gcd p.coeff
Module: Mathlib.RingTheory.UniqueFactorizationDomain.FactorSet

Goal state before:
pp: α : Type u_1
inst✝ : CommMonoidWithZero α
b : FactorSet α
h : ⊤ ≤ b
this : b = ⊤
⊢ ⊤.prod ≤ ⊤.prod

Tactic:
prod_top

Goal state after:
α : Type u_1
inst✝ : CommMonoidWithZero α
b : FactorSet α
h : ⊤ ≤ b
this : b = ⊤
⊢ 0 ≤ 0
Module: Mathlib.RingTheory.UniqueFactorizationDomain.FactorSet

Goal state before:
pp: α : Type u_1
inst✝¹ : CommMonoidWithZero α
inst✝ : UniqueFactorizationMonoid α
a : Associates α
⊢ a.factors = ⊤ ↔ a = 0

Tactic:
nontriviality α

Goal state after:
α : Type u_1
inst✝¹ : CommMonoidWithZero α
inst✝ : UniqueFactorizationMonoid α
a : Associates α
a✝ : Nontrivial α
⊢ a.factors = ⊤ ↔ a = 0
Module: Mathlib.Algebra.Polynomial.FieldDivision

Goal state before:
pp: R : Type u
inst✝ : Field R
p q : R[X]
hq0 : q ≠ 0
h : p / q = 0
⊢ p.degree < q.degree

Tactic:
have := EuclideanDomain.div_add_mod p q

Goal state after:
R : Type u
inst✝ : Field R
p q : R[X]
hq0 : q ≠ 0
h : p / q = 0
this : q * (p / q) + p % q = p
⊢ p.degree < q.degree
Module: Mathlib.RingTheory.UniqueFactorizationDomain.FactorSet

Goal state before:
pp: α : Type u_1
inst✝¹ : CommMonoidWithZero α
inst✝ : UniqueFactorizationMonoid α
a b : Associates α
⊢ (a * b).factors = a.factors + b.factors

Tactic:
nontriviality α

Goal state after:
α : Type u_1
inst✝¹ : CommMonoidWithZero α
inst✝ : UniqueFactorizationMonoid α
a b : Associates α
a✝ : Nontrivial α
⊢ (a * b).factors = a.factors + b.factors
Module: Mathlib.RingTheory.UniqueFactorizationDomain.FactorSet

Goal state before:
pp: α : Type u_1
inst✝¹ : CommMonoidWithZero α
inst✝ : UniqueFactorizationMonoid α
a b : Associates α
⊢ (a.factors ⊔ b.factors).prod * (a.factors ⊓ b.factors).prod = a * b

Tactic:
nontriviality α

Goal state after:
α : Type u_1
inst✝¹ : CommMonoidWithZero α
inst✝ : UniqueFactorizationMonoid α
a b : Associates α
a✝ : Nontrivial α
⊢ (a.factors ⊔ b.factors).prod * (a.factors ⊓ b.factors).prod = a * b
Module: Mathlib.RingTheory.Polynomial.Content

Goal state before:
pp: case pos
R : Type u_1
inst✝¹ : CommRing R
inst✝ : NormalizedGCDMonoid R
p q : R[X]
hp : p.IsPrimitive
hq : q.IsPrimitive
h : ∃ n r, r.natDegree = n ∧ r.IsPrimitive ∧ p ∣ r ∧ q ∣ r
r : R[X]
rdeg : r.natDegree = Nat.find h
rprim : r.IsPrimitive
pr : p ∣ r
qr : q ∣ r
con : ∃ n s, s.natDegree = n ∧ (p ∣ s ∧ q ∣ s) ∧ ¬r ∣ s
s : R[X]
sdeg : s.natDegree = Nat.find con
rs : ¬r ∣ s
ps : p ∣ s
qs : q ∣ s
s0 : s ≠ 0
hs : r.natDegree ≤ s.natDegree
sC : s.natDegree ≤ 0
⊢ False

pp: case neg
R : Type u_1
inst✝¹ : CommRing R
inst✝ : NormalizedGCDMonoid R
p q : R[X]
hp : p.IsPrimitive
hq : q.IsPrimitive
h : ∃ n r, r.natDegree = n ∧ r.IsPrimitive ∧ p ∣ r ∧ q ∣ r
r : R[X]
rdeg : r.natDegree = Nat.find h
rprim : r.IsPrimitive
pr : p ∣ r
qr : q ∣ r
con : ∃ n s, s.natDegree = n ∧ (p ∣ s ∧ q ∣ s) ∧ ¬r ∣ s
s : R[X]
sdeg : s.natDegree = Nat.find con
rs : ¬r ∣ s
ps : p ∣ s
qs : q ∣ s
s0 : s ≠ 0
hs : r.natDegree ≤ s.natDegree
sC : 0 < s.natDegree
⊢ False

Tactic:
· rw [eq_C_of_natDegree_le_zero (le_trans hs sC), isPrimitive_iff_content_eq_one, content_C,
        normalize_eq_one] at rprim
      rw [eq_C_of_natDegree_le_zero (le_trans hs sC), ← dvd_content_iff_C_dvd] at rs
      apply rs rprim.dvd

Goal state after:
case neg
R : Type u_1
inst✝¹ : CommRing R
inst✝ : NormalizedGCDMonoid R
p q : R[X]
hp : p.IsPrimitive
hq : q.IsPrimitive
h : ∃ n r, r.natDegree = n ∧ r.IsPrimitive ∧ p ∣ r ∧ q ∣ r
r : R[X]
rdeg : r.natDegree = Nat.find h
rprim : r.IsPrimitive
pr : p ∣ r
qr : q ∣ r
con : ∃ n s, s.natDegree = n ∧ (p ∣ s ∧ q ∣ s) ∧ ¬r ∣ s
s : R[X]
sdeg : s.natDegree = Nat.find con
rs : ¬r ∣ s
ps : p ∣ s
qs : q ∣ s
s0 : s ≠ 0
hs : r.natDegree ≤ s.natDegree
sC : 0 < s.natDegree
⊢ False
Module: Mathlib.Algebra.Polynomial.FieldDivision

Goal state before:
pp: R : Type u
inst✝ : Field R
p q : R[X]
hpq : q.degree ≤ p.degree
⊢ (p / q).leadingCoeff = p.leadingCoeff / q.leadingCoeff

Tactic:
by
  by_cases hq : q = 0
  · simp [hq]
  rw [div_def, leadingCoeff_mul, leadingCoeff_C,
    leadingCoeff_divByMonic_of_monic (monic_mul_leadingCoeff_inv hq) _, mul_comm,
    div_eq_mul_inv]
  rwa [degree_mul_leadingCoeff_inv q hq]

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

Goal state before:
pp: α : Type u_1
inst✝² : CommMonoidWithZero α
inst✝¹ : UniqueFactorizationMonoid α
inst✝ : Nontrivial α
p : Associates α
hp : Irreducible p
⊢ p = {p}.prod

Tactic:
rw [prod_singleton]

Goal state after:
Module: Mathlib.RingTheory.Polynomial.UniqueFactorization

Goal state before:
pp: case succ
σ : Type v
D : Type u
inst✝² : CommRing D
inst✝¹ : UniqueFactorizationMonoid D
inst✝ : Finite σ
this : Fintype σ
d : ℕ
hd : UniqueFactorizationMonoid (MvPolynomial (Fin d) D)
⊢ UniqueFactorizationMonoid (MvPolynomial (Fin (d + 1)) D)

Tactic:
apply (finSuccEquiv D d).toMulEquiv.symm.uniqueFactorizationMonoid
      exact Polynomial.uniqueFactorizationMonoid

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

Goal state before:
pp: α : Type u_1
inst✝³ : CommMonoidWithZero α
inst✝² : UniqueFactorizationMonoid α
inst✝¹ : DecidableEq (Associates α)
inst✝ : (p : Associates α) → Decidable (Irreducible p)
a : Associates α
ha : a ≠ 0
k : ℕ
hk : ∀ (p : Associates α), Irreducible p → k ∣ p.count a.factors
⊢ ∃ b, a = b ^ k

Tactic:
nontriviality α

Goal state after:
α : Type u_1
inst✝³ : CommMonoidWithZero α
inst✝² : UniqueFactorizationMonoid α
inst✝¹ : DecidableEq (Associates α)
inst✝ : (p : Associates α) → Decidable (Irreducible p)
a : Associates α
ha : a ≠ 0
k : ℕ
hk : ∀ (p : Associates α), Irreducible p → k ∣ p.count a.factors
a✝ : Nontrivial α
⊢ ∃ b, a = b ^ k
Module: Mathlib.RingTheory.UniqueFactorizationDomain.FactorSet

Goal state before:
pp: α : Type u_1
inst✝³ : CommMonoidWithZero α
inst✝² : UniqueFactorizationMonoid α
inst✝¹ : DecidableEq (Associates α)
inst✝ : (p : Associates α) → Decidable (Irreducible p)
p a : Associates α
hp : Irreducible p
n : ℕ
h : a ∣ p ^ n
⊢ a = p ^ p.count a.factors

Tactic:
nontriviality α

Goal state after:
α : Type u_1
inst✝³ : CommMonoidWithZero α
inst✝² : UniqueFactorizationMonoid α
inst✝¹ : DecidableEq (Associates α)
inst✝ : (p : Associates α) → Decidable (Irreducible p)
p a : Associates α
hp : Irreducible p
n : ℕ
h : a ∣ p ^ n
a✝ : Nontrivial α
⊢ a = p ^ p.count a.factors
Module: Mathlib.RingTheory.UniqueFactorizationDomain.FactorSet

Goal state before:
pp: α : Type u_1
inst✝¹ : CommMonoidWithZero α
inst✝ : UniqueFactorizationMonoid α
a b c : Associates α
ha : a ≠ 0
hb : b ≠ 0
hab : ∀ (d : Associates α), d ∣ a → d ∣ b → ¬Prime d
k : ℕ
h : a * b = c ^ k
⊢ ∃ d, a = d ^ k

Tactic:
nontriviality α

Goal state after:
α : Type u_1
inst✝¹ : CommMonoidWithZero α
inst✝ : UniqueFactorizationMonoid α
a b c : Associates α
ha : a ≠ 0
hb : b ≠ 0
hab : ∀ (d : Associates α), d ∣ a → d ∣ b → ¬Prime d
k : ℕ
h : a * b = c ^ k
a✝ : Nontrivial α
⊢ ∃ d, a = d ^ k
Module: Mathlib.RingTheory.Algebraic.Basic

Goal state before:
pp: R : Type u
S : Type u_1
A : Type v
inst✝⁶ : CommRing R
inst✝⁵ : CommRing S
inst✝⁴ : Ring A
inst✝³ : Algebra R A
inst✝² : Algebra R S
inst✝¹ : Algebra S A
inst✝ : IsScalarTower R S A
a : S
h : Function.Injective ⇑(algebraMap S A)
⊢ ¬IsAlgebraic R ((algebraMap S A) a) ↔ ¬IsAlgebraic R a

Tactic:
isAlgebraic_algebraMap_iff h

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

Goal state before:
pp: R : Type u_1
M : Type u_2
N : Type u_3
P : Type u_4
inst✝⁸ : CommRing R
inst✝⁷ : AddCommGroup M
inst✝⁶ : AddCommGroup N
inst✝⁵ : AddCommGroup P
inst✝⁴ : Module R M
inst✝³ : Module R N
inst✝² : Module R P
f : M →ₗ[R] N
g : N →ₗ[R] P
Q : Type u_5
inst✝¹ : AddCommGroup Q
inst✝ : Module R Q
hfg✝ : Exact ⇑f ⇑g
hg : Surjective ⇑g
h : P → N
hfg : Exact ⇑f ⇑g
hgh : RightInverse h ⇑g
p p' : P
q : Q
⊢ ((TensorProduct.mk R Q N).flip (h (p + p'))) q -
      (fun x1 x2 ↦ x1 + x2) (((TensorProduct.mk R Q N).flip (h p)) q) (((TensorProduct.mk R Q N).flip (h p')) q) ∈
    (lTensor Q f).range

Tactic:
by
      change q ⊗ₜ[R] (h (p + p')) - (q ⊗ₜ[R] (h p) + q ⊗ₜ[R] (h p')) ∈ range (lTensor Q f)
      rw [← TensorProduct.tmul_add, ← TensorProduct.tmul_sub]
      apply le_comap_range_lTensor f
      rw [exact_iff] at hfg
      simp only [← hfg, mem_ker, map_sub, map_add, hgh _, sub_self]

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

Goal state before:
pp: R : Type u_1
inst✝² : CommRing R
Q : Type u_5
inst✝¹ : AddCommGroup Q
inst✝ : Module R Q
I : Ideal R
⊢ ((TensorProduct.mk R (R ⧸ I) Q) 1).ker = I • ⊤

Tactic:
apply comap_injective_of_surjective (TensorProduct.lid R Q).surjective

Goal state after:
R : Type u_1
inst✝² : CommRing R
Q : Type u_5
inst✝¹ : AddCommGroup Q
inst✝ : Module R Q
I : Ideal R
⊢ comap (↑(TensorProduct.lid R Q)) ((TensorProduct.mk R (R ⧸ I) Q) 1).ker = comap (↑(TensorProduct.lid R Q)) (I • ⊤)
Module: Mathlib.LinearAlgebra.TensorProduct.Finiteness

Goal state before:
pp: R : Type u_1
M : Type u_2
N : Type u_3
inst✝⁴ : CommSemiring R
inst✝³ : AddCommMonoid M
inst✝² : AddCommMonoid N
inst✝¹ : Module R M
inst✝ : Module R N
s : Set (M ⊗[R] N)
hs : s.Finite
⊢ ∃ N', Module.Finite R ↥N' ∧ s ⊆ ↑(LinearMap.lTensor M N'.subtype).range

Tactic:
obtain ⟨_, N', _, hfin, h⟩ := exists_finite_submodule_of_setFinite s hs

Goal state after:
R : Type u_1
M : Type u_2
N : Type u_3
inst✝⁴ : CommSemiring R
inst✝³ : AddCommMonoid M
inst✝² : AddCommMonoid N
inst✝¹ : Module R M
inst✝ : Module R N
s : Set (M ⊗[R] N)
hs : s.Finite
w✝ : Submodule R M
N' : Submodule R N
left✝ : Module.Finite R ↥w✝
hfin : Module.Finite R ↥N'
h : s ⊆ ↑(mapIncl w✝ N').range
⊢ ∃ N', Module.Finite R ↥N' ∧ s ⊆ ↑(LinearMap.lTensor M N'.subtype).range
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 : ι) → DivisionRing (G i)
inst✝² : DivisionRing C
inst✝¹ : ∀ (i j : ι) (h : i ≤ j), RingHomClass (T h) (G i) (G j)
inst✝ : ∀ (i : ι), RingHomClass (H i) (G i) C
g : (i : ι) → H i
h : ∀ (i j : ι) (h : i ≤ j) (x : G i), (g i) x = (g j) ((f i j h) x)
q : ℚ
i : ι
⊢ DirectLimit.lift f (fun x ↦ ⇑(g x)) h ↑q = ↑q

Tactic:
ratCast_def,

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 : ι) → DivisionRing (G i)
inst✝² : DivisionRing C
inst✝¹ : ∀ (i j : ι) (h : i ≤ j), RingHomClass (T h) (G i) (G j)
inst✝ : ∀ (i : ι), RingHomClass (H i) (G i) C
g : (i : ι) → H i
h : ∀ (i j : ι) (h : i ≤ j) (x : G i), (g i) x = (g j) ((f i j h) x)
q : ℚ
i : ι
⊢ DirectLimit.lift f (fun x ↦ ⇑(g x)) h ⟦⟨?i, ↑q⟩⟧ = ↑q

case i
ι : 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 : ι) → DivisionRing (G i)
inst✝² : DivisionRing C
inst✝¹ : ∀ (i j : ι) (h : i ≤ j), RingHomClass (T h) (G i) (G j)
inst✝ : ∀ (i : ι), RingHomClass (H i) (G i) C
g : (i : ι) → H i
h : ∀ (i j : ι) (h : i ≤ j) (x : G i), (g i) x = (g j) ((f i j h) x)
q : ℚ
i : ι
⊢ ι
Module: Mathlib.Algebra.Group.EvenFunction

Goal state before:
pp: α : Type u_1
inst✝¹ : Neg α
R : Type u_3
inst✝ : Mul R
f g : α → R
hf : Function.Even f
hg : Function.Even g
⊢ Function.Even (f * g)

Tactic:
intro a
  simp only [Pi.mul_apply, hf a, hg a]

Goal state after:
Module: Mathlib.Algebra.BigOperators.Group.Finset.Interval

Goal state before:
pp: case succ
α : Type u_1
inst✝ : CommGroup α
f : ℤ → α
hf : Function.Even f
N : ℕ
ih : ∏ m ∈ Icc (-↑N) ↑N, f m = (∏ m ∈ range (N + 1), f ↑m) ^ 2 / f 0
⊢ ∏ m ∈ Icc (-↑(N + 1)) ↑(N + 1), f m = (∏ m ∈ range (N + 1 + 1), f ↑m) ^ 2 / f 0

Tactic:
rw [Nat.cast_add, Nat.cast_one, Icc_succ_succ, prod_union (by simp), prod_pair (by lia), ih,
      prod_range_succ _ (N + 1), hf, ← pow_two, div_mul_eq_mul_div, ← mul_pow, Nat.cast_succ]

Goal state after:
Module: Mathlib.RingTheory.IsTensorProduct

Goal state before:
pp: case refine_2
R : Type u_1
M : Type v₁
N : Type v₂
S : Type v₃
inst✝¹² : AddCommMonoid M
inst✝¹¹ : AddCommMonoid N
inst✝¹⁰ : CommSemiring R
inst✝⁹ : CommSemiring S
inst✝⁸ : Algebra R S
inst✝⁷ : Module R M
inst✝⁶ : Module R N
inst✝⁵ : Module S N
inst✝⁴ : IsScalarTower R S N
f : M →ₗ[R] N
h : IsBaseChange S f
P : Type u_2
Q : Type u_3
inst✝³ : AddCommMonoid P
inst✝² : Module R P
inst✝¹ : AddCommMonoid Q
inst✝ : Module S Q
r : S
x : S ⊗[R] M
⊢ ∀ (x : S) (y : M), (IsTensorProduct.equiv h) (r • x ⊗ₜ[R] y) = r • (IsTensorProduct.equiv h) (x ⊗ₜ[R] y)

Tactic:
intro x y
        simp [smul_tmul', Algebra.linearMap_apply, smul_comm r x]

Goal state after: