mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Data.Nat.Factorization.Basic

Goal state before:
pp: case inr.inr
n d : ℕ
hn : n ≠ 0
hd : d ≠ 0
⊢ (∀ (p k : ℕ), Prime p → p ^ k ∣ d → p ^ k ∣ n) → ∀ (p : ℕ), Prime p → d.factorization p ≤ n.factorization p

Tactic:
intro h p pp

Goal state after:
case inr.inr
n d : ℕ
hn : n ≠ 0
hd : d ≠ 0
h : ∀ (p k : ℕ), Prime p → p ^ k ∣ d → p ^ k ∣ n
p : ℕ
pp : Prime p
⊢ d.factorization p ≤ n.factorization p
Module: Mathlib.GroupTheory.OrderOfElement

Goal state before:
pp: G : Type u_1
inst✝ : Group G
s : Set G
hs : ∀ x ∈ s, IsOfFinOrder x
⊢ (closure s).toSubmonoid = Submonoid.closure s

Tactic:
refine le_antisymm ?_ (le_closure_toSubmonoid s)

Goal state after:
G : Type u_1
inst✝ : Group G
s : Set G
hs : ∀ x ∈ s, IsOfFinOrder x
⊢ (closure s).toSubmonoid ≤ Submonoid.closure s
Module: Mathlib.GroupTheory.OrderOfElement

Goal state before:
pp: G : Type u_1
inst✝ : Group G
g : G
k : ℤ
⊢ g ∈ zpowers (g ^ k) ↔ ∃ x, k * x ≡ 1 [ZMOD ↑(orderOf g)]

Tactic:
← zpow_eq_zpow_iff_modEq,

Goal state after:
G : Type u_1
inst✝ : Group G
g : G
k : ℤ
⊢ g ∈ zpowers (g ^ k) ↔ ∃ x, g ^ (k * x) = g ^ 1
Module: Mathlib.GroupTheory.OrderOfElement

Goal state before:
pp: G : Type u_1
inst✝¹ : Group G
inst✝ : Fintype G
x : G
⊢ x ^ card G = 1

Tactic:
← Nat.card_eq_fintype_card,

Goal state after:
G : Type u_1
inst✝¹ : Group G
inst✝ : Fintype G
x : G
⊢ x ^ Nat.card G = 1
Module: Mathlib.Algebra.MonoidAlgebra.Division

Goal state before:
pp: k : Type u_1
G : Type u_2
inst✝¹ : Semiring k
inst✝ : AddCommMonoid G
x : k[G]
g g' : G
h : ∃ d, g' = g + d
⊢ (x %ᵒᶠ g).coeff g' = 0

Tactic:
classical exact Finsupp.filter_apply_neg _ _ <| by rwa [Classical.not_not]

Goal state after:
Module: Mathlib.Data.Nat.Factorization.Basic

Goal state before:
pp: case h
a b m n : ℕ
hmn : m.Coprime n
h : a ^ m = b ^ n
ha0 : ¬a = 0
hn0 : ¬n = 0
factors : ℕ →₀ ℕ := mapRange (fun x ↦ x / n) ⋯ a.factorization
c : ℕ := factors.prod fun x1 x2 ↦ x1 ^ x2
hc : c = factors.prod fun x1 x2 ↦ x1 ^ x2
p : ℕ
foo : ∀ p ∈ factors.support, Prime p
⊢ n ∣ a.factorization p

Tactic:
refine hmn.symm.dvd_of_dvd_mul_left ⟨b.factorization p, ?_⟩

Goal state after:
case h
a b m n : ℕ
hmn : m.Coprime n
h : a ^ m = b ^ n
ha0 : ¬a = 0
hn0 : ¬n = 0
factors : ℕ →₀ ℕ := mapRange (fun x ↦ x / n) ⋯ a.factorization
c : ℕ := factors.prod fun x1 x2 ↦ x1 ^ x2
hc : c = factors.prod fun x1 x2 ↦ x1 ^ x2
p : ℕ
foo : ∀ p ∈ factors.support, Prime p
⊢ m * a.factorization p = n * b.factorization p
Module: Mathlib.Algebra.Polynomial.RingDivision

Goal state before:
pp: R : Type u
inst✝ : CommRing R
q : R[X]
c : R
p : R[X]
hq : q.Monic
hR : Nontrivial R
⊢ c • (p %ₘ q) + c • (q * (p /ₘ q)) = c • p

Tactic:
← smul_add,

Goal state after:
R : Type u
inst✝ : CommRing R
q : R[X]
c : R
p : R[X]
hq : q.Monic
hR : Nontrivial R
⊢ c • (p %ₘ q + q * (p /ₘ q)) = c • p
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:
rw [coeff_map, coeff_expand (Nat.pos_of_ne_zero hp), coeff_expand (Nat.pos_of_ne_zero hp)]

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 (if p ∣ n✝ then q.coeff (n✝ / p) else 0) = if p ∣ n✝ then (map f q).coeff (n✝ / p) else 0
Module: Mathlib.Algebra.Polynomial.Derivative

Goal state before:
pp: R : Type u
inst✝ : Semiring R
a : R
⊢ C (a * ↑2) * X ^ (2 - 1) = C (a * 2) * X

Tactic:
Nat.cast_two,

Goal state after:
R : Type u
inst✝ : Semiring R
a : R
⊢ C (a * 2) * X ^ (2 - 1) = C (a * 2) * X
Module: Mathlib.Algebra.Polynomial.Derivative

Goal state before:
pp: R : Type u
inst✝ : Semiring R
⊢ C ↑2 * X ^ (2 - 1) = C 2 * X

Tactic:
Nat.cast_two,

Goal state after:
R : Type u
inst✝ : Semiring R
⊢ C 2 * X ^ (2 - 1) = C 2 * X
Module: Mathlib.Algebra.Polynomial.Derivative

Goal state before:
pp: R : Type u
inst✝ : Semiring R
p : R[X]
k : ℕ
⊢ ((⇑derivative)^[k] p).natDegree ≤ p.natDegree - k

Tactic:
by
  induction k with
  | zero => rw [Function.iterate_zero_apply, Nat.sub_zero]
  | succ d hd =>
      rw [Function.iterate_succ_apply', Nat.sub_succ']
      exact (natDegree_derivative_le _).trans <| Nat.sub_le_sub_right hd 1

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
⊢ Algebra.Transcendental R A ↔ ¬Algebra.IsAlgebraic R A

Tactic:
simp [isAlgebraic_def, transcendental_def, Transcendental]

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

Goal state before:
pp: R : Type u
inst✝ : Ring R
p q : R[X]
hq : q.Monic
h✝ : q ∣ p
a✝ : Nontrivial R
r : R[X]
hr : p = q * r
hpq0 : ¬p %ₘ q = 0
hmod : p %ₘ q = q * (r - p /ₘ q)
this : (q * (r - p /ₘ q)).degree < q.degree
h : (r - p /ₘ q).leadingCoeff = 0
⊢ (p %ₘ q).leadingCoeff = 0

Tactic:
hmod,

Goal state after:
R : Type u
inst✝ : Ring R
p q : R[X]
hq : q.Monic
h✝ : q ∣ p
a✝ : Nontrivial R
r : R[X]
hr : p = q * r
hpq0 : ¬p %ₘ q = 0
hmod : p %ₘ q = q * (r - p /ₘ q)
this : (q * (r - p /ₘ q)).degree < q.degree
h : (r - p /ₘ q).leadingCoeff = 0
⊢ (q * (r - p /ₘ q)).leadingCoeff = 0
Module: Mathlib.Algebra.Polynomial.Derivative

Goal state before:
pp: case a
R : Type u
inst✝¹ : Semiring R
p : R[X]
inst✝ : IsAddTorsionFree R
hp : p.natDegree ≠ 0
⊢ ↑(p.natDegree - 1) ≤ (derivative p).degree

Tactic:
refine le_sup ?_

Goal state after:
case a
R : Type u
inst✝¹ : Semiring R
p : R[X]
inst✝ : IsAddTorsionFree R
hp : p.natDegree ≠ 0
⊢ p.natDegree - 1 ∈ (derivative p).support
Module: Mathlib.Algebra.Polynomial.Div

Goal state before:
pp: R : Type u
inst✝ : CommRing R
p : R[X]
p0 : p ≠ 0
a : R
n : ℕ
⊢ n ≤ rootMultiplicity a p ↔ (X - C a) ^ n ∣ p

Tactic:
simp_rw [rootMultiplicity, dif_neg p0, Nat.le_find_iff, not_not]

Goal state after:
R : Type u
inst✝ : CommRing R
p : R[X]
p0 : p ≠ 0
a : R
n : ℕ
⊢ (∀ m < n, (X - C a) ^ (m + 1) ∣ p) ↔ (X - C a) ^ n ∣ p
Module: Mathlib.Algebra.Polynomial.Div

Goal state before:
pp: R : Type u
inst✝ : CommRing R
p : R[X]
p0 : p ≠ 0
a : R
n : ℕ
⊢ n ≤ rootMultiplicity a p ↔ (X - C a) ^ n ∣ p

Tactic:
by
  simp_rw [rootMultiplicity, dif_neg p0, Nat.le_find_iff, not_not]
  refine ⟨fun h => ?_, fun h m hm => (pow_dvd_pow _ hm).trans h⟩
  rcases n with - | n
  · rw [pow_zero]
    apply one_dvd
  · exact h n n.lt_succ_self

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

Goal state before:
pp: case mpr
α : Type u_6
β : Type u_7
ι : Type u_8
a : α
b : β
i : ι
b' : β
i' : ι
h₁ : (b', i').1 ∈ {b}
right✝ : (b', i').2 ∈ univ
⊢ (b', i') ∈ Prod.map (fun x ↦ b) id '' ({a}ᶜ ×ˢ {i}ᶜ)ᶜ

Tactic:
use (a, i')

Goal state after:
case h
α : Type u_6
β : Type u_7
ι : Type u_8
a : α
b : β
i : ι
b' : β
i' : ι
h₁ : (b', i').1 ∈ {b}
right✝ : (b', i').2 ∈ univ
⊢ (a, i') ∈ ({a}ᶜ ×ˢ {i}ᶜ)ᶜ ∧ Prod.map (fun x ↦ b) id (a, i') = (b', i')
Module: Mathlib.Order.Filter.TendstoCofinite

Goal state before:
pp: α : Type u_1
β : Type u_2
ι : Type u_3
f : α → β
g : β → ι
inst✝¹ : TendstoCofinite g
inst✝ : TendstoCofinite f
r : ι
⊢ (g ∘ f ⁻¹' {r}).Finite

Tactic:
simpa using! TendstoCofinite.finite_preimage f (TendstoCofinite.finite_preimage g (by simp))

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

Goal state before:
pp: α : Type u_1
β : Type u_2
R : Type u_4
M : Type u_5
f : α → β
inst✝² : AddCommMonoid M
inst✝¹ : TendstoCofinite f
inst✝ : DistribSMul R M
r : R
v : α → M
x✝ : β
⊢ mapDomain f (r • v) x✝ = (r • mapDomain f v) x✝

Tactic:
simp [mapDomain, Finset.smul_sum]

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

Goal state before:
pp: α : Type u_1
inst✝¹ : CommMonoidWithZero α
inst✝ : IsCancelMulZero α
h : WellFoundedLT (Associates α)
⊢ WellFounded DvdNotUnit

Tactic:
convert h.wf; exact Associates.dvdNotUnit_iff_lt

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

Goal state before:
pp: R : Type u
a : R
inst✝¹ : CommRing R
inst✝ : IsDomain R
p : R[X]
⊢ 0 < rootMultiplicity a p ↔ p ≠ 0 ∧ p.IsRoot a

Tactic:
rootMultiplicity_pos'

Goal state after:
R : Type u
a : R
inst✝¹ : CommRing R
inst✝ : IsDomain R
p : R[X]
⊢ p ≠ 0 ∧ p.IsRoot a ↔ p ≠ 0 ∧ p.IsRoot a
Module: Mathlib.Algebra.Polynomial.Roots

Goal state before:
pp: R : Type u
inst✝¹ : CommRing R
inst✝ : IsDomain R
p : R[X]
⊢ p.roots = 0 ↔ p = 0 ∨ p.IsRoot = ⊥

Tactic:
rcases eq_or_ne p 0 with rfl | hp0; · simp
  simp [roots_eq_zero_iff_isRoot_eq_bot hp0, hp0]

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

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

Tactic:
have ia := hs a (Multiset.mem_cons_self a _)
    have ib := fun b h => hs b (Multiset.mem_cons_of_mem h)
    obtain rfl | ⟨b, hb⟩ := s.empty_or_exists_mem
    · rw [Multiset.cons_zero, Multiset.prod_singleton, Multiset.map_singleton,
        normalizedFactors_irreducible ia]
    have := nontrivial_of_ne b 0 (ib b hb).ne_zero
    rw [Multiset.prod_cons, Multiset.map_cons,
      normalizedFactors_mul ia.ne_zero (Multiset.prod_ne_zero fun h => (ib 0 h).ne_zero rfl),
      normalizedFactors_irreducible ia, ih ib, Multiset.singleton_add]

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

Goal state before:
pp: α : Type u_1
inst✝¹ : CommMonoidWithZero α
inst✝ : UniqueFactorizationMonoid α
x y : α
hx : x ≠ 0
hy : y ≠ 0
⊢ x * y ~ᵤ (factors x + factors y).prod

Tactic:
prod_add

Goal state after:
α : Type u_1
inst✝¹ : CommMonoidWithZero α
inst✝ : UniqueFactorizationMonoid α
x y : α
hx : x ≠ 0
hy : y ≠ 0
⊢ x * y ~ᵤ (factors x).prod * (factors y).prod
Module: Mathlib.RingTheory.UniqueFactorizationDomain.Basic

Goal state before:
pp: α : Type u_1
inst✝¹ : CommMonoidWithZero α
inst✝ : UniqueFactorizationMonoid α
x : α
hx : x ≠ 0
h : factors x = 0
⊢ IsUnit x

Tactic:
by contrapose! h; simpa [eq_zero_iff_forall_notMem] using exists_mem_factors hx h

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

Goal state before:
pp: R : Type u_1
inst✝¹ : CommRing R
inst✝ : NormalizedGCDMonoid R
p : R[X]
⊢ p.content = gcd p.leadingCoeff p.eraseLead.content

Tactic:
by_cases h : p = 0
  · simp [h]
  rw [← leadingCoeff_eq_zero, leadingCoeff, ← Ne, ← mem_support_iff] at h
  rw [content, ← Finset.insert_erase h, Finset.gcd_insert, leadingCoeff, content,
    eraseLead_support]
  refine congr rfl (Finset.gcd_congr rfl fun i hi => ?_)
  rw [Finset.mem_erase] at hi
  rw [eraseLead_coeff, if_neg hi.1]

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

Goal state before:
pp: R : Type u_1
inst✝¹ : CommRing R
inst✝ : NormalizedGCDMonoid R
p : R[X]
a✝ : Nontrivial R
h : ¬C p.content = 0
| p.natDegree

Tactic:
rw [p.eq_C_content_mul_primPart, natDegree_mul h p.primPart_ne_zero, natDegree_C, zero_add]

Goal state after:
R : Type u_1
inst✝¹ : CommRing R
inst✝ : NormalizedGCDMonoid R
p : R[X]
a✝ : Nontrivial R
h : ¬C p.content = 0
| p.primPart.natDegree
Module: Mathlib.RingTheory.Polynomial.Content

Goal state before:
pp: R : Type u_1
inst✝³ : CommRing R
inst✝² : NormalizedGCDMonoid R
S : Type u_2
inst✝¹ : CommSemiring S
inst✝ : IsDomain S
f : R →+* S
hinj : Function.Injective ⇑f
p : R[X]
s : S
hpzero : p ≠ 0
hp : eval₂ f s p = 0
⊢ eval₂ f s p.primPart = 0

Tactic:
rw [eq_C_content_mul_primPart p, eval₂_mul, eval₂_C] at hp
  refine eq_zero_of_ne_zero_of_mul_left_eq_zero ?_ hp
  rwa [hinj.ne_iff' (map_zero _), Ne, content_eq_zero_iff]

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

Goal state before:
pp: case mpr
α : Type u_1
M : Type u_2
inst✝² : CommMonoidWithZero M
inst✝¹ : UniqueFactorizationMonoid M
inst✝ : Fintype Mˣ
y : M
hy : y ≠ 0
this✝² : Nontrivial M
this✝¹ : StrongNormalizationMonoid M
this✝ : DecidableEq M
this : DecidableEq (Associates M)
x : M
⊢ x ∣ y → ∃ a, a.1 ≤ normalizedFactors y ∧ ↑a.2 * a.1.prod = x

Tactic:
rintro (h : x ∣ y)
    have hx : x ≠ 0 := by
      refine mt (fun hx => ?_) hy
      rwa [hx, zero_dvd_iff] at h
    obtain ⟨u, hu⟩ := prod_normalizedFactors hx
    refine ⟨⟨normalizedFactors x, u⟩, ?_, (mul_comm _ _).trans hu⟩
    exact (dvd_iff_normalizedFactors_le_normalizedFactors hx hy).mp h

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

Goal state before:
pp: case h
R : Type u_1
inst✝¹ : CommRing R
inst✝ : NormalizedGCDMonoid R
a : R
p q : R[X]
x : ℕ
a✝ : x ∈ Finset.range (max p.natDegree q.natDegree).succ
w : R[X]
hw : p - q = C a * w
⊢ (p - q).coeff x = a * w.coeff x

Tactic:
hw,

Goal state after:
case h
R : Type u_1
inst✝¹ : CommRing R
inst✝ : NormalizedGCDMonoid R
a : R
p q : R[X]
x : ℕ
a✝ : x ∈ Finset.range (max p.natDegree q.natDegree).succ
w : R[X]
hw : p - q = C a * w
⊢ (C a * w).coeff x = a * w.coeff x
Module: Mathlib.Algebra.Polynomial.Roots

Goal state before:
pp: R : Type u
inst✝¹ : CommRing R
inst✝ : IsDomain R
p q : R[X]
he : p = (Multiset.map (fun a ↦ X - C a) p.roots).prod * q
⊢ ∃ q, (Multiset.map (fun a ↦ X - C a) p.roots).prod * q = p ∧ p.roots.card + q.natDegree = p.natDegree ∧ q.roots = 0

Tactic:
use q, he.symm

Goal state after:
case right
R : Type u
inst✝¹ : CommRing R
inst✝ : IsDomain R
p q : R[X]
he : p = (Multiset.map (fun a ↦ X - C a) p.roots).prod * q
⊢ p.roots.card + q.natDegree = p.natDegree ∧ q.roots = 0
Module: Mathlib.Algebra.Polynomial.Roots

Goal state before:
pp: case right
R : Type u
inst✝¹ : CommRing R
inst✝ : IsDomain R
p q : R[X]
he : p = (Multiset.map (fun a ↦ X - C a) p.roots).prod * q
⊢ p.roots.card + q.natDegree = p.natDegree ∧ q.roots = 0

Tactic:
obtain rfl | hq := eq_or_ne q 0

Goal state after:
case right.inl
R : Type u
inst✝¹ : CommRing R
inst✝ : IsDomain R
p : R[X]
he : p = (Multiset.map (fun a ↦ X - C a) p.roots).prod * 0
⊢ p.roots.card + natDegree 0 = p.natDegree ∧ roots 0 = 0

case right.inr
R : Type u
inst✝¹ : CommRing R
inst✝ : IsDomain R
p q : R[X]
he : p = (Multiset.map (fun a ↦ X - C a) p.roots).prod * q
hq : q ≠ 0
⊢ p.roots.card + q.natDegree = p.natDegree ∧ q.roots = 0
Module: Mathlib.Algebra.Polynomial.FieldDivision

Goal state before:
pp: R : Type u
inst✝ : DivisionRing R
p : R[X]
hp0 : C (p.coeff 0) ≠ 0
hp : ¬IsUnit (C (p.coeff 0))
h : p.degree ≤ 0
⊢ False

Tactic:
exact hp (IsUnit.map C (IsUnit.mk0 (coeff p 0) (mt C_inj.2 (by simpa using hp0))))

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

Goal state before:
pp: case pos
A : Type u_1
B : Type u_2
inst✝⁴ : CommRing A
inst✝³ : CommRing B
inst✝² : IsDomain A
inst✝¹ : IsDomain B
f : A →+* B
inst✝ : DecidablePred fun x ↦ x ∈ f.range
hf : Function.Injective ⇑f
p : A[X]
b : B
h : b ∈ f.range
⊢ count b (map f p).roots = count b (Multiset.map (⇑f) p.roots)

Tactic:
obtain ⟨a, rfl⟩ := h
    simp [hf, Multiset.count_map_eq_count', eq_rootMultiplicity_map hf]

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

Goal state before:
pp: R : Type u
inst✝ : Field R
p₁ p₂ q : R[X]
h : q ∣ p₁ - p₂
⊢ p₁ % q = p₂ % q

Tactic:
obtain rfl | hq := eq_or_ne q 0

Goal state after:
case inl
R : Type u
inst✝ : Field R
p₁ p₂ : R[X]
h : 0 ∣ p₁ - p₂
⊢ p₁ % 0 = p₂ % 0

case inr
R : Type u
inst✝ : Field R
p₁ p₂ q : R[X]
h : q ∣ p₁ - p₂
hq : q ≠ 0
⊢ p₁ % q = p₂ % q
Module: Mathlib.Algebra.Central.End

Goal state before:
pp: case neg
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
⊢ ∃ α, f = α • g

Tactic:
obtain ⟨x, hx⟩ := exists_ne (0 : M)

Goal state after:
case neg
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
⊢ ∃ α, f = α • g
Module: Mathlib.Algebra.Central.End

Goal state before:
pp: case neg
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 = α * β
⊢ ∃ α, f = α • g

Tactic:
exact ⟨.mk α β this.symm (mul_comm α β ▸ this.symm), ext fun _ ↦ by simpa using congr($hα _)⟩

Goal state after:
Module: Mathlib.Order.DirectedInverseSystem

Goal state before:
pp: ι✝ : 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
F : ι → Type u_7
X : ι → Type u_8
i : ι
inst✝ : LinearOrder ι
f : ⦃i j : ι⦄ → i ≤ j → F j → F i
equiv : (j : ↑(Iio i)) → F ↑j ≃ piLT X ↑j
nat : IsNatEquiv f equiv
t : ↑(limit f i)
x✝¹ x✝ : ↑(Iio i)
h : ↑x✝¹ ≤ ↑x✝
⊢ (fun l ↦ (equiv l) (↑t l)) x✝¹ = piLTProj h ((fun l ↦ (equiv l) (↑t l)) x✝)

Tactic:
simp_rw [← t.2 h]

Goal state after:
ι✝ : 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
F : ι → Type u_7
X : ι → Type u_8
i : ι
inst✝ : LinearOrder ι
f : ⦃i j : ι⦄ → i ≤ j → F j → F i
equiv : (j : ↑(Iio i)) → F ↑j ≃ piLT X ↑j
nat : IsNatEquiv f equiv
t : ↑(limit f i)
x✝¹ x✝ : ↑(Iio i)
h : ↑x✝¹ ≤ ↑x✝
⊢ (equiv x✝¹) (f h (↑t x✝)) = piLTProj h ((equiv x✝) (↑t x✝))
Module: Mathlib.Order.Interval.Finset.Gaps

Goal state before:
pp: case pos
α : Type u_1
inst✝ : LinearOrder α
F : Finset (α × α)
k : ℕ
h : #F = k
j✝ : ℕ
a b : α
hab : a ≤ b
hFab : ∀ ⦃z : α × α⦄, z ∈ F → a ≤ z.1 ∧ z.1 ≤ z.2 ∧ z.2 ≤ b
hF : (↑F).PairwiseDisjoint fun z ↦ Icc z.1 z.2
j : ℕ
hj : j < k + 1
hj₁ : ¬j = 0
hk : k - 1 + 1 = k
hj₂ : j = k
⊢ (F.intervalGapsWithin h a b ↑j).1 ≤ (F.intervalGapsWithin h a b ↑j).2

Tactic:
simp only [hj₂, natCast_eq_last, intervalGapsWithin_last_snd, ge_iff_le]
    convert! hFab (F.intervalGapsWithin_mapsTo h a b (x := j - 1) (by grind)) |>.right.right using 1
    simp [hj₂, hk]

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

Goal state before:
pp: α : Type u_1
β : Type u_2
s : Finset α
a : α
inst✝ : CommMonoid β
ha : a ∉ s
f : Finset α → β
⊢ ∏ t ∈ (cons a s ha).powerset, f t = (∏ t ∈ s.powerset, f t) * ∏ t ∈ s.powerset.attach, f (cons a ↑t ⋯)

Tactic:
by
  classical
  simp_rw [cons_eq_insert]
  rw [prod_powerset_insert ha, prod_attach _ fun t ↦ f (insert a t)]

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
P : Type u_2
Q : Type u_3
inst✝⁵ : AddCommMonoid P
inst✝⁴ : Module R P
inst✝³ : AddCommMonoid Q
inst✝² : Module S Q
inst✝¹ : Module R Q
inst✝ : IsScalarTower R S Q
f' : P →ₗ[R] Q
eM : M ≃ₗ[R] P
eN : N ≃ₗ[S] Q
comm : f' ∘ₗ ↑eM = ↑(LinearEquiv.restrictScalars R eN) ∘ₗ f
this : ∀ (m : M), f' (eM m) = eN (f m)
ist : IsTensorProduct (↑R ((Algebra.linearMap S (Module.End S (P →ₗ[R] Q))).flip f'))
⊢ IsTensorProduct (↑R ((Algebra.linearMap S (Module.End S (M →ₗ[R] N))).flip f))

Tactic:
convert! (ist.compl₂_linearEquiv eM).compr₂_linearEquiv (eN.symm.restrictScalars R)

Goal state after:
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
P : Type u_2
Q : Type u_3
inst✝⁵ : AddCommMonoid P
inst✝⁴ : Module R P
inst✝³ : AddCommMonoid Q
inst✝² : Module S Q
inst✝¹ : Module R Q
inst✝ : IsScalarTower R S Q
f' : P →ₗ[R] Q
eM : M ≃ₗ[R] P
eN : N ≃ₗ[S] Q
comm : f' ∘ₗ ↑eM = ↑(LinearEquiv.restrictScalars R eN) ∘ₗ f
this : ∀ (m : M), f' (eM m) = eN (f m)
ist : IsTensorProduct (↑R ((Algebra.linearMap S (Module.End S (P →ₗ[R] Q))).flip f'))
⊢ ↑R ((Algebra.linearMap S (Module.End S (M →ₗ[R] N))).flip f) =
    ((↑R ((Algebra.linearMap S (Module.End S (P →ₗ[R] Q))).flip f')).compl₂ ↑eM).compr₂
      ↑(LinearEquiv.restrictScalars R eN.symm)
Module: Mathlib.Data.Sym.Sym2.Order

Goal state before:
pp: α : Type ?u.3
inst✝ : LinearOrder α
a b : α
⊢ (↑((fun s ↦ ⟨(s.inf, s.sup), ⋯⟩) s(a, b))).1 = a ∧ (↑((fun s ↦ ⟨(s.inf, s.sup), ⋯⟩) s(a, b))).2 = b ∨
    (↑((fun s ↦ ⟨(s.inf, s.sup), ⋯⟩) s(a, b))).1 = b ∧ (↑((fun s ↦ ⟨(s.inf, s.sup), ⋯⟩) s(a, b))).2 = a

Tactic:
cases le_total a b with
    | inl h => simp [h]
    | inr h => simp [h]

Goal state after:
Module: Mathlib.Data.Sym.Sym2.Order

Goal state before:
pp: case h.h.inl.inl
α : Type u_1
inst✝ : LinearOrder α
a b c d : α
hab : a ≤ b
hcd : c ≤ d
⊢ s(a, b).inf = s(c, d).inf ∧ s(a, b).sup = s(c, d).sup ↔ s(a, b) = s(c, d)

Tactic:
aesop (add unsafe le_antisymm)

Goal state after:
Module: Mathlib.Data.Sym.Sym2.Order

Goal state before:
pp: case h.h.inl.inr
α : Type u_1
inst✝ : LinearOrder α
a b c d : α
hab : a ≤ b
hdc : d ≤ c
⊢ s(a, b).inf = s(c, d).inf ∧ s(a, b).sup = s(c, d).sup ↔ s(a, b) = s(c, d)

Tactic:
aesop (add unsafe le_antisymm)

Goal state after:
Module: Mathlib.Data.Sym.Sym2.Order

Goal state before:
pp: case h.h.inr.inl
α : Type u_1
inst✝ : LinearOrder α
a b c d : α
hba : b ≤ a
hcd : c ≤ d
⊢ s(a, b).inf = s(c, d).inf ∧ s(a, b).sup = s(c, d).sup ↔ s(a, b) = s(c, d)

Tactic:
aesop (add unsafe le_antisymm)

Goal state after:
Module: Mathlib.Data.Sym.Sym2.Order

Goal state before:
pp: case h.h.inr.inr
α : Type u_1
inst✝ : LinearOrder α
a b c d : α
hba : b ≤ a
hdc : d ≤ c
⊢ s(a, b).inf = s(c, d).inf ∧ s(a, b).sup = s(c, d).sup ↔ s(a, b) = s(c, d)

Tactic:
aesop (add unsafe le_antisymm)

Goal state after:
Module: Mathlib.Data.Sym.Sym2

Goal state before:
pp: α : Type u_1
x y : α
z : Sym2 α
hne : x ≠ y
⊢ x ∈ z ∧ y ∈ z ↔ z = s(x, y)

Tactic:
constructor
  · cases z
    rw [mem_iff, mem_iff]
    aesop
  · rintro rfl
    simp

Goal state after:
Module: Mathlib.CategoryTheory.Groupoid

Goal state before:
pp: C : Type u_1
inst✝ : Category.{v_1, u_1} C
⊢ IsGroupoid C ↔ isomorphisms C = ⊤

Tactic:
by
  constructor
  · rw [eq_top_iff]
    intro _ _
    simp only [isomorphisms.iff, top_apply]
    infer_instance
  · intro h
    exact ⟨of_eq_top h⟩

Goal state after:
Module: Mathlib.CategoryTheory.EpiMono

Goal state before:
pp: C : Type u₁
inst✝² : Category.{v₁, u₁} C
X Y : C
f : X ⟶ Y
inst✝¹ : Mono f
inst✝ : IsSplitEpi f
⊢ f ≫ section_ f = 𝟙 X

Tactic:
simp [← cancel_mono f]

Goal state after:
Module: Mathlib.CategoryTheory.MorphismProperty.Basic

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
P : MorphismProperty C
inst✝ : P.RespectsIso
⊢ P.isoClosure = P

Tactic:
P.isoClosure_eq_self

Goal state after:
C : Type u
inst✝¹ : Category.{v, u} C
P : MorphismProperty C
inst✝ : P.RespectsIso
⊢ P = P