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

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

Tactic:
set g := p /ₘ (X - C t) ^ m

Goal state after:
case inr
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 t g = (p.comp (X + C t)).trailingCoeff
Module: Mathlib.Order.Filter.Finite

Goal state before:
pp: α : Type u
ι : Type u_2
f : ι → Filter α
⊢ (⨅ i, f i).sets = ⋃ t, (⨅ i ∈ t, f i).sets

Tactic:
by
  rw [iInf_eq_iInf_finset, iInf_sets_eq]
  exact directed_of_isDirected_le fun _ _ => biInf_mono

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

Goal state before:
pp: α : Type u
ι : Type w
s : Set ι
hs : s.Finite
f : ι → Set α
⊢ ⨅ i ∈ s, 𝓟 (f i) = 𝓟 (⋂ i ∈ s, f i)

Tactic:
by
  lift s to Finset ι using hs
  exact mod_cast iInf_principal_finset s f

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

Goal state before:
pp: α : Type u_1
β : Type u_2
f₁ f₂ : Filter α
g₁ g₂ : Filter β
inst✝¹ : f₁.NeBot
inst✝ : g₁.NeBot
h : f₁ ×ˢ g₁ = f₂ ×ˢ g₂
hle : f₁ ≤ f₂ ∧ g₁ ≤ g₂
this✝ : f₂.NeBot
this : g₂.NeBot
⊢ f₁ = f₂ ∧ g₁ = g₂

Tactic:
exact ⟨hle.1.antisymm <| (prod_le_prod.1 h.ge).1, hle.2.antisymm <| (prod_le_prod.1 h.ge).2⟩

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

Goal state before:
pp: R : Type u
inst✝ : CommSemiring R
p q p₁ p₂ : R[X]
ih₁ : derivative (eval₂ C q p₁) = eval₂ C q (derivative p₁) * derivative q
ih₂ : derivative (eval₂ C q p₂) = eval₂ C q (derivative p₂) * derivative q
⊢ eval₂ C q (derivative p₁) * derivative q + derivative (eval₂ C q p₂) = eval₂ C q (derivative (p₁ + p₂)) * derivative q

Tactic:
ih₂,

Goal state after:
R : Type u
inst✝ : CommSemiring R
p q p₁ p₂ : R[X]
ih₁ : derivative (eval₂ C q p₁) = eval₂ C q (derivative p₁) * derivative q
ih₂ : derivative (eval₂ C q p₂) = eval₂ C q (derivative p₂) * derivative q
⊢ eval₂ C q (derivative p₁) * derivative q + eval₂ C q (derivative p₂) * derivative q =
    eval₂ C q (derivative (p₁ + p₂)) * derivative q
Module: Mathlib.Order.Filter.Cofinite

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

Tactic:
by
  simpa using hs.compl_mem_cofinite

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

Goal state before:
pp: α : Type u_1
β : Type u_2
s : Set α
t : Set β
⊢ 𝓟 s ×ˢ 𝓟 t = 𝓟 (s ×ˢ t)

Tactic:
by
  simp only [prod_eq_inf, comap_principal, principal_eq_iff_eq, comap_principal, inf_principal]; rfl

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

Goal state before:
pp: α : Type u_1
β : Type u_2
s : Set (α × β)
f : Filter α
g : Filter β
⊢ s ∈ f.coprod g ↔ (∃ t₁ ∈ f, Prod.fst ⁻¹' t₁ ⊆ s) ∧ ∃ t₂ ∈ g, Prod.snd ⁻¹' t₂ ⊆ s

Tactic:
by
  simp [Filter.coprod]

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

Goal state before:
pp: α : Type u_1
β : Type u_2
l : Filter β
⊢ ⊥.coprod l = comap Prod.snd l

Tactic:
by
  simp [Filter.coprod]

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

Goal state before:
pp: α : Type u_1
β : Type u_2
l : Filter α
⊢ l.coprod ⊥ = comap Prod.fst l

Tactic:
by
  simp [Filter.coprod]

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

Goal state before:
pp: α : Type u_1
β : Type u_2
f : Filter α
g : Filter β
⊢ (f.coprod g).NeBot ↔ f.NeBot ∧ Nonempty β ∨ Nonempty α ∧ g.NeBot

Tactic:
by
  simp [Filter.coprod]

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

Goal state before:
pp: case left_neg
R : Type u
inst✝ : CommRing R
S : Finset R
k : ℕ
ind : (⇑derivative)^[k] (∏ a ∈ S, (X - C a)) = ↑k ! * ∑ T ∈ powersetCard (#S - k) S, ∏ a ∈ T, (X - C a)
hk : k + 1 ≤ #S
⊢ ∀ (a : Finset R × R)
    (ha :
      a ∈
        {x ∈ powersetCard (#S - k) S ×ˢ S |
          match x with
          | (T, i) => i ∈ T}),
    (match
        match a, ha with
        | (T, i), x => (T.erase i, i),
        ⋯ with
      | (T, i), x => (insert i T, i)) =
      a

Tactic:
intro r hr

Goal state after:
case left_neg
R : Type u
inst✝ : CommRing R
S : Finset R
k : ℕ
ind : (⇑derivative)^[k] (∏ a ∈ S, (X - C a)) = ↑k ! * ∑ T ∈ powersetCard (#S - k) S, ∏ a ∈ T, (X - C a)
hk : k + 1 ≤ #S
r : Finset R × R
hr :
  r ∈
    {x ∈ powersetCard (#S - k) S ×ˢ S |
      match x with
      | (T, i) => i ∈ T}
⊢ (match
      match r, hr with
      | (T, i), x => (T.erase i, i),
      ⋯ with
    | (T, i), x => (insert i T, i)) =
    r
Module: Mathlib.Algebra.BigOperators.Associated

Goal state before:
pp: case insert
M : Type u_4
inst✝ : CommMonoid M
ι : Type u_5
s✝ : Finset ι
f g : ι → M
j : ι
s : Finset ι
hjs : j ∉ s
IH : (∀ i ∈ s, f i ~ᵤ g i) → ∏ i ∈ s, f i ~ᵤ ∏ i ∈ s, g i
h : ∀ i ∈ insert j s, f i ~ᵤ g i
⊢ ∏ i ∈ insert j s, f i ~ᵤ ∏ i ∈ insert j s, g i

Tactic:
| insert j s hjs IH =>

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

Goal state before:
pp: case right_neg
R : Type u
inst✝ : CommRing R
S : Finset R
k : ℕ
ind : (⇑derivative)^[k] (∏ a ∈ S, (X - C a)) = ↑k ! * ∑ T ∈ powersetCard (#S - k) S, ∏ a ∈ T, (X - C a)
hk : k + 1 ≤ #S
⊢ ∀ (a : Finset R × R)
    (ha :
      a ∈
        {x ∈ powersetCard (#S - (k + 1)) S ×ˢ S |
          match x with
          | (T, i) => i ∉ T}),
    (match
        match a, ha with
        | (T, i), x => (insert i T, i),
        ⋯ with
      | (T, i), x => (T.erase i, i)) =
      a

Tactic:
intro r hr

Goal state after:
case right_neg
R : Type u
inst✝ : CommRing R
S : Finset R
k : ℕ
ind : (⇑derivative)^[k] (∏ a ∈ S, (X - C a)) = ↑k ! * ∑ T ∈ powersetCard (#S - k) S, ∏ a ∈ T, (X - C a)
hk : k + 1 ≤ #S
r : Finset R × R
hr :
  r ∈
    {x ∈ powersetCard (#S - (k + 1)) S ×ˢ S |
      match x with
      | (T, i) => i ∉ T}
⊢ (match
      match r, hr with
      | (T, i), x => (insert i T, i),
      ⋯ with
    | (T, i), x => (T.erase i, i)) =
    r
Module: Mathlib.Data.Finsupp.Weight

Goal state before:
pp: σ : Type u_1
M : Type u_2
R : Type u_3
inst✝³ : Semiring R
w : σ → M
inst✝² : AddCommMonoid M
inst✝¹ : Module R M
inst✝ : Fintype σ
f : σ →₀ R
⊢ (f.sum fun i c ↦ c • w i) = ∑ i, f i • w i

Tactic:
f.sum_fintype (fun i c ↦ c • w i) fun _ ↦ zero_smul _ _

Goal state after:
σ : Type u_1
M : Type u_2
R : Type u_3
inst✝³ : Semiring R
w : σ → M
inst✝² : AddCommMonoid M
inst✝¹ : Module R M
inst✝ : Fintype σ
f : σ →₀ R
⊢ ∑ i, f i • w i = ∑ i, f i • w i
Module: Mathlib.RingTheory.UniqueFactorizationDomain.Basic

Goal state before:
pp: α : Type u_1
inst✝¹ : CommMonoidWithZero α
inst✝ : UniqueFactorizationMonoid α
x : α
hx : x ≠ 0
h : ¬IsUnit x
⊢ ∃ p, p ∈ factors x

Tactic:
by
  obtain ⟨p', hp', hp'x⟩ := WfDvdMonoid.exists_irreducible_factor h hx
  obtain ⟨p, hp, _⟩ := exists_mem_factors_of_dvd hx hp' hp'x
  exact ⟨p, hp⟩

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

Goal state before:
pp: R : Type u
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : Infinite R
p : R[X]
h : ∀ (x : R), eval x p = 0
⊢ p = 0

Tactic:
classical
  by_contra hp
  refine @Fintype.false R _ ?_
  exact ⟨p.roots.toFinset, fun x => Multiset.mem_toFinset.mpr ((mem_roots hp).mpr (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 = 0 ↔ p = 0

Tactic:
rw [content, Finset.gcd_eq_zero_iff]
  constructor <;> intro h
  · ext n
    simp_all
  · intro x
    simp [h]

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

Goal state before:
pp: case neg
R : Type u_1
inst✝¹ : CommRing R
inst✝ : NormalizedGCDMonoid R
p : R[X]
hp0 : ¬p.content = 0
⊢ p.content * ↑(normUnit p.content) = p.content * ↑1

Tactic:
← normalize_apply,

Goal state after:
case neg
R : Type u_1
inst✝¹ : CommRing R
inst✝ : NormalizedGCDMonoid R
p : R[X]
hp0 : ¬p.content = 0
⊢ normalize p.content = p.content * ↑1
Module: Mathlib.RingTheory.UniqueFactorizationDomain.Basic

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝¹ : CommMonoidWithZero α
inst✝ : CommMonoidWithZero β
e : α ≃* β
hα : ∀ (a : α), a ≠ 0 → ∃ f, (∀ b ∈ f, Prime b) ∧ f.prod ~ᵤ a
this : IsCancelMulZero β
a : β
ha : a ≠ 0
w : Multiset α
hp : ∀ b ∈ w, Prime b
u : αˣ
h : w.prod * ↑u = e.symm a
⊢ e w.prod * e ↑u = a

Tactic:
← map_mul e,

Goal state after:
α : Type u_1
β : Type u_2
inst✝¹ : CommMonoidWithZero α
inst✝ : CommMonoidWithZero β
e : α ≃* β
hα : ∀ (a : α), a ≠ 0 → ∃ f, (∀ b ∈ f, Prime b) ∧ f.prod ~ᵤ a
this : IsCancelMulZero β
a : β
ha : a ≠ 0
w : Multiset α
hp : ∀ b ∈ w, Prime b
u : αˣ
h : w.prod * ↑u = e.symm a
⊢ e (w.prod * ↑u) = a
Module: Mathlib.RingTheory.UniqueFactorizationDomain.Basic

Goal state before:
pp: case pos.refine_2
R : Type u_2
inst✝¹ : CommMonoidWithZero R
inst✝ : UniqueFactorizationMonoid R
a✝ a p : R
a_ne_zero : a ≠ 0
p_prime : Prime p
ih_a : a ≠ 0 → ∀ (b : R), ∃ a' b' c', IsRelPrime a' b' ∧ c' * a' = a ∧ c' * b' = b
pa_ne_zero : p * a ≠ 0
b a' b' c' : R
no_factor : IsRelPrime a' b'
ha' : c' * a' = a
hb' : c' * b' = b
⊢ p * c' * b' = p * b

Tactic:
rw [mul_assoc, hb']

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

Goal state before:
pp: R : Type u
k : Type y
inst✝¹ : Field R
p q : R[X]
inst✝ : Field k
f : R →+* k
⊢ map f (p % q) = map f p % map f q

Tactic:
by_cases hq0 : q = 0
  · simp [hq0]
  · rw [mod_def, mod_def, leadingCoeff_map f, ← map_inv₀ f, ← map_C f, ← Polynomial.map_mul f,
      map_modByMonic f (monic_mul_leadingCoeff_inv hq0)]

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

Goal state before:
pp: 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
⊢ False

Tactic:
by_cases! sC : s.natDegree ≤ 0

Goal state after:
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

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.RingTheory.UniqueFactorizationDomain.FactorSet

Goal state before:
pp: α : Type u_1
inst✝² : CommMonoidWithZero α
inst✝¹ : UniqueFactorizationMonoid α
inst✝ : DecidableEq (Associates α)
p : Associates α
h₂ : Irreducible p
k : ℕ
m : α
hm : m ≠ 0
h₁ : Associates.mk m ≠ 0
this : Nontrivial α
⊢ p ^ k ≤ Associates.mk m ↔ replicate k ⟨p, h₂⟩ ≤ factors' m

pp: case h
α : Type u_1
inst✝² : CommMonoidWithZero α
inst✝¹ : UniqueFactorizationMonoid α
inst✝ : DecidableEq (Associates α)
p : Associates α
h₂ : Irreducible p
k : ℕ
m : α
hm : m ≠ 0
h₁ : Associates.mk m ≠ 0
this : Nontrivial α
⊢ m ≠ 0

Tactic:
← factors_le,

Goal state after:
α : Type u_1
inst✝² : CommMonoidWithZero α
inst✝¹ : UniqueFactorizationMonoid α
inst✝ : DecidableEq (Associates α)
p : Associates α
h₂ : Irreducible p
k : ℕ
m : α
hm : m ≠ 0
h₁ : Associates.mk m ≠ 0
this : Nontrivial α
⊢ (p ^ k).factors ≤ (Associates.mk m).factors ↔ replicate k ⟨p, h₂⟩ ≤ factors' m

case h
α : Type u_1
inst✝² : CommMonoidWithZero α
inst✝¹ : UniqueFactorizationMonoid α
inst✝ : DecidableEq (Associates α)
p : Associates α
h₂ : Irreducible p
k : ℕ
m : α
hm : m ≠ 0
h₁ : Associates.mk m ≠ 0
this : Nontrivial α
⊢ m ≠ 0
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
  · simpa [sub_eq_zero] using h
  simp_rw [Polynomial.mod_def]
  apply Polynomial.modByMonic_eq_of_dvd_sub (by simp [Polynomial.Monic.def, hq])
  rw [mul_comm]
  exact (Polynomial.C_mul_dvd (by simpa using hq)).mpr h

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

Goal state before:
pp: R : Type u_1
S : Type u_2
inst✝² : CommRing R
inst✝¹ : Ring S
inst✝ : Algebra R S
s : S
hs : s ∈ S⁰
p : R[X]
hp0 : p ≠ 0
hp : (aeval s) p = 0
q : R[X]
hpq : p = (X - C 0) ^ rootMultiplicity 0 p * q
hq : ¬X - C 0 ∣ q
⊢ ∃ q, q.coeff 0 ≠ 0 ∧ (aeval s) q = 0

Tactic:
simp only [C_0, sub_zero, X_pow_mul, X_dvd_iff] at hpq hq

Goal state after:
R : Type u_1
S : Type u_2
inst✝² : CommRing R
inst✝¹ : Ring S
inst✝ : Algebra R S
s : S
hs : s ∈ S⁰
p : R[X]
hp0 : p ≠ 0
hp : (aeval s) p = 0
q : R[X]
hpq : p = q * X ^ rootMultiplicity 0 p
hq : ¬q.coeff 0 = 0
⊢ ∃ q, q.coeff 0 ≠ 0 ∧ (aeval s) q = 0
Module: Mathlib.Order.DirectedInverseSystem

Goal state before:
pp: ι : Type u_1
inst✝³ : Preorder ι
F : ι → Type u_4
T : ⦃i j : ι⦄ → i ≤ j → Sort u_8
f : (i j : ι) → (h : i ≤ j) → T h
inst✝² : ⦃i j : ι⦄ → (h : i ≤ j) → FunLike (T h) (F i) (F j)
inst✝¹ : DirectedSystem F fun x1 x2 x3 ↦ ⇑(f x1 x2 x3)
inst✝ : IsDirectedOrder ι
z : DirectLimit F f
⊢ ∃ i x, z = ⟦⟨i, x⟩⟧

Tactic:
by rcases z; exact ⟨_, _, rfl⟩

Goal state after:
Module: Mathlib.Order.DirectedInverseSystem

Goal state before:
pp: case inr
ι : Type u_6
F : ι → Type u_7
X : ι → Type u_8
i : ι
inst✝² : LinearOrder ι
f : ⦃i j : ι⦄ → i ≤ j → F j → F i
inst✝¹ : SuccOrder ι
equiv : (j : ↑(Iic i)) → F ↑j ≃ piLT X ↑j
e : F i⁺ ≃ F i × X i
hi : ¬IsMax i
inst✝ : InverseSystem f
H : ∀ (x : F i⁺), (e x).1 = f ⋯ x
nat : IsNatEquiv f equiv
j k : ι
hj✝ : j ∈ Iic i⁺
hk : k ∈ Iic i⁺
h : k ≤ j
x : F j
lt_succ : ∀ {j : ι}, j ≤ i → j < i⁺
hj : j ≤ i
⊢ (piSplitLE
        (fun j ↦ equiv ⟨↑j, ⋯⟩,
          e.trans (((equiv ⟨i, ⋯⟩).prodCongr (Equiv.refl (X i))).trans (piSplitLE.trans (Equiv.piCongrSet ⋯))))
        ⟨k, hk⟩)
      (f h x) =
    piLTProj h
      ((piSplitLE
          (fun j ↦ equiv ⟨↑j, ⋯⟩,
            e.trans (((equiv ⟨i, ⋯⟩).prodCongr (Equiv.refl (X i))).trans (piSplitLE.trans (Equiv.piCongrSet ⋯))))
          ⟨j, hj✝⟩)
        x)

Tactic:
piSplitLE_lt (h.trans_lt <| lt_succ hj),

Goal state after:
case inr
ι : Type u_6
F : ι → Type u_7
X : ι → Type u_8
i : ι
inst✝² : LinearOrder ι
f : ⦃i j : ι⦄ → i ≤ j → F j → F i
inst✝¹ : SuccOrder ι
equiv : (j : ↑(Iic i)) → F ↑j ≃ piLT X ↑j
e : F i⁺ ≃ F i × X i
hi : ¬IsMax i
inst✝ : InverseSystem f
H : ∀ (x : F i⁺), (e x).1 = f ⋯ x
nat : IsNatEquiv f equiv
j k : ι
hj✝ : j ∈ Iic i⁺
hk : k ∈ Iic i⁺
h : k ≤ j
x : F j
lt_succ : ∀ {j : ι}, j ≤ i → j < i⁺
hj : j ≤ i
⊢ ((fun j ↦ equiv ⟨↑j, ⋯⟩,
            e.trans (((equiv ⟨i, ⋯⟩).prodCongr (Equiv.refl (X i))).trans (piSplitLE.trans (Equiv.piCongrSet ⋯)))).1
        ⟨k, ⋯⟩)
      (f h x) =
    piLTProj h
      ((piSplitLE
          (fun j ↦ equiv ⟨↑j, ⋯⟩,
            e.trans (((equiv ⟨i, ⋯⟩).prodCongr (Equiv.refl (X i))).trans (piSplitLE.trans (Equiv.piCongrSet ⋯))))
          ⟨j, hj✝⟩)
        x)
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
⊢ comap (↑(TensorProduct.lid R Q)) ((TensorProduct.mk R (R ⧸ I) Q) 1).ker = comap (↑(TensorProduct.lid R Q)) (I • ⊤)

Tactic:
rw [← ker_comp]

Goal state after:
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 ∘ₗ ↑(TensorProduct.lid R Q)).ker = comap (↑(TensorProduct.lid R Q)) (I • ⊤)
Module: Mathlib.RingTheory.Flat.Basic

Goal state before:
pp: R : Type u
M : Type v
N✝ : Type u_1
P✝ : Type u_2
inst✝⁷ : CommSemiring R
inst✝⁶ : AddCommMonoid M
inst✝⁵ : Module R M
inst✝⁴ : AddCommMonoid N✝
inst✝³ : Module R N✝
inst✝² : AddCommMonoid P✝
inst✝¹ : Module R P✝
inst✝ : Flat R M
f : N✝ →ₗ[R] P✝
hf : Injective ⇑f
N : Submodule R N✝
P : Submodule R P✝
Nfg : N.FG
Pfg : P.FG
le : N ≤ comap f P
⊢ Injective ⇑(rTensor M (f.restrict le))

Tactic:
rw [← Finite.iff_fg] at Nfg Pfg

Goal state after:
R : Type u
M : Type v
N✝ : Type u_1
P✝ : Type u_2
inst✝⁷ : CommSemiring R
inst✝⁶ : AddCommMonoid M
inst✝⁵ : Module R M
inst✝⁴ : AddCommMonoid N✝
inst✝³ : Module R N✝
inst✝² : AddCommMonoid P✝
inst✝¹ : Module R P✝
inst✝ : Flat R M
f : N✝ →ₗ[R] P✝
hf : Injective ⇑f
N : Submodule R N✝
P : Submodule R P✝
Nfg : Module.Finite R ↥N
Pfg : Module.Finite R ↥P
le : N ≤ comap f P
⊢ Injective ⇑(rTensor M (f.restrict le))
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 : ι
⊢ DirectLimit.lift f (fun x ↦ ⇑(g x)) h 1 = 1

Tactic:
one_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 : ι) → 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 : ι
⊢ DirectLimit.lift f (fun x ↦ ⇑(g x)) h ⟦⟨?m.94, 1⟩⟧ = 1

ι : 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 : ι
⊢ ι
Module: Mathlib.RingTheory.Flat.Basic

Goal state before:
pp: R : Type u
M : Type v
inst✝³ : CommRing R
inst✝² : AddCommGroup M
inst✝¹ : Module R M
inst✝ : Small.{v', u} R
H :
  ∀ ⦃N N' N'' : Type v'⦄ [inst : AddCommGroup N] [inst_1 : AddCommGroup N'] [inst_2 : AddCommGroup N'']
    [inst_3 : Module R N] [inst_4 : Module R N'] [inst_5 : Module R N''] ⦃f : N →ₗ[R] N'⦄ ⦃g : N' →ₗ[R] N''⦄,
    Function.Exact ⇑f ⇑g → Function.Exact ⇑(rTensor M f) ⇑(rTensor M g)
N' N'' : Type v'
x✝³ : AddCommGroup N'
x✝² : AddCommGroup N''
x✝¹ : Module R N'
x✝ : Module R N''
f : N' →ₗ[R] N''
hf : Injective ⇑f
x : N' ⊗[R] M
hx : (rTensor M f) x = 0
⊢ x ∈ ⊥

Tactic:
simpa [Eq.comm] using @H PUnit N' N'' _ _ _ _ _ _ 0 f (fun x ↦ by
    simp_rw [Set.mem_range, LinearMap.zero_apply, exists_const]
    exact (f.map_eq_zero_iff hf).trans eq_comm) x |>.mp hx

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

Goal state before:
pp: R : Type u_1
C : Type u_2
A : Type u_3
inst✝⁵ : CommSemiring R
inst✝⁴ : CommSemiring C
inst✝³ : Semiring A
inst✝² : Algebra R A
inst✝¹ : Algebra R C
inst✝ : Module.Flat R C
h : ∀ (B : Subalgebra R A), B.FG → IsReduced (C ⊗[R] ↥B)
h_contra : ¬IsReduced (C ⊗[R] A)
x : C ⊗[R] A
hx : x ≠ 0 ∧ IsNilpotent x
D : Subalgebra R A
hD : D.FG ∧ x ∈ Subalgebra.baseChange C D
⊢ False

Tactic:
have h_inj : Function.Injective
      (Algebra.TensorProduct.map (AlgHom.id C C) D.val) :=
    Module.Flat.lTensor_preserves_injective_linearMap _ Subtype.val_injective

Goal state after:
R : Type u_1
C : Type u_2
A : Type u_3
inst✝⁵ : CommSemiring R
inst✝⁴ : CommSemiring C
inst✝³ : Semiring A
inst✝² : Algebra R A
inst✝¹ : Algebra R C
inst✝ : Module.Flat R C
h : ∀ (B : Subalgebra R A), B.FG → IsReduced (C ⊗[R] ↥B)
h_contra : ¬IsReduced (C ⊗[R] A)
x : C ⊗[R] A
hx : x ≠ 0 ∧ IsNilpotent x
D : Subalgebra R A
hD : D.FG ∧ x ∈ Subalgebra.baseChange C D
h_inj : Function.Injective ⇑(Algebra.TensorProduct.map (AlgHom.id C C) D.val)
⊢ False
Module: Mathlib.Algebra.BigOperators.Group.Finset.Indicator

Goal state before:
pp: ι : Type u_1
α : Type u_3
β : Type u_4
inst✝¹ : CommMonoid β
inst✝ : One α
f : ι → α
g : ι → α → β
s t : Finset ι
h : s ⊆ t
hg : ∀ (a : ι), g a 1 = 1
i : ι
x✝ : i ∈ t
hn : i ∉ s
⊢ g i ((↑s).mulIndicator f i) = 1

Tactic:
simp [hn, hg]

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

Goal state before:
pp: α : Type u_1
x : α
xs : List α
z : Sym2 α
⊢ z ∈ (x :: xs).sym2 ↔ z = s(x, x) ∨ (∃ y ∈ xs, z = s(x, y)) ∨ z ∈ xs.sym2

Tactic:
simp only [List.sym2, map_cons, cons_append, mem_cons, mem_append, mem_map]
  simp only [eq_comm]

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

Goal state before:
pp: case cons.inr
α : Type u_1
inst✝ : DecidableEq α
x : α
xs : List α
ih : xs.sym2.dedup = xs.dedup.sym2
hm : x ∉ xs
⊢ (s(x, x) :: (map (fun y ↦ s(x, y)) xs ++ xs.sym2)).dedup = (x :: xs).dedup.sym2

Tactic:
rw [dedup_cons_of_notMem hm, List.sym2, map_cons, ← ih, dedup_cons_of_notMem, cons_append,
        List.Disjoint.dedup_append, dedup_map_of_injective]

Goal state after:
case cons.inr.hf
α : Type u_1
inst✝ : DecidableEq α
x : α
xs : List α
ih : xs.sym2.dedup = xs.dedup.sym2
hm : x ∉ xs
⊢ Function.Injective fun y ↦ s(x, y)

case cons.inr
α : Type u_1
inst✝ : DecidableEq α
x : α
xs : List α
ih : xs.sym2.dedup = xs.dedup.sym2
hm : x ∉ xs
⊢ (map (fun y ↦ s(x, y)) xs).Disjoint xs.sym2

case cons.inr
α : Type u_1
inst✝ : DecidableEq α
x : α
xs : List α
ih : xs.sym2.dedup = xs.dedup.sym2
hm : x ∉ xs
⊢ s(x, x) ∉ map (fun y ↦ s(x, y)) xs ++ xs.sym2
Module: Mathlib.Data.Sym.Sym2

Goal state before:
pp: case mk.mk
α : Type u_1
β : Type u_2
γ : Type u_3
z z' : Sym2 α
x y x' y' : α
h : ∀ (x_1 : α), Sym2.Mem x_1 (Quot.mk (Rel α) (x, y)) ↔ Sym2.Mem x_1 (Quot.mk (Rel α) (x', y'))
hx : Sym2.Mem x (Quot.mk (Rel α) (x, y)) ↔ Sym2.Mem x (Quot.mk (Rel α) (x', y'))
hy : Sym2.Mem y (Quot.mk (Rel α) (x, y)) ↔ Sym2.Mem y (Quot.mk (Rel α) (x', y'))
⊢ Quot.mk (Rel α) (x, y) = Quot.mk (Rel α) (x', y')

Tactic:
have hx' := h x'

Goal state after:
case mk.mk
α : Type u_1
β : Type u_2
γ : Type u_3
z z' : Sym2 α
x y x' y' : α
h : ∀ (x_1 : α), Sym2.Mem x_1 (Quot.mk (Rel α) (x, y)) ↔ Sym2.Mem x_1 (Quot.mk (Rel α) (x', y'))
hx : Sym2.Mem x (Quot.mk (Rel α) (x, y)) ↔ Sym2.Mem x (Quot.mk (Rel α) (x', y'))
hy : Sym2.Mem y (Quot.mk (Rel α) (x, y)) ↔ Sym2.Mem y (Quot.mk (Rel α) (x', y'))
hx' : Sym2.Mem x' (Quot.mk (Rel α) (x, y)) ↔ Sym2.Mem x' (Quot.mk (Rel α) (x', y'))
⊢ Quot.mk (Rel α) (x, y) = Quot.mk (Rel α) (x', y')
Module: Mathlib.Data.Sym.Sym2

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
z : Sym2 α
f : α → β
inst✝ : DecidableEq α
a : α
⊢ ∀ (a_1 b c d : α) (h : Rel α (a_1, b) (c, d)),
    Eq.ndrec (motive := fun x ↦ a ∈ x → α) (fun x ↦ if a = a_1 then b else a_1) ⋯ = fun x ↦ if a = c then d else c

Tactic:
intro b c d e h

Goal state after:
α : Type u_1
β : Type u_2
γ : Type u_3
z : Sym2 α
f : α → β
inst✝ : DecidableEq α
a b c d e : α
h : Rel α (b, c) (d, e)
⊢ Eq.ndrec (motive := fun x ↦ a ∈ x → α) (fun x ↦ if a = b then c else b) ⋯ = fun x ↦ if a = d then e else d