mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.RingTheory.UniqueFactorizationDomain.NormalizedFactors

Goal state before:
pp: α : Type u_1
inst✝² : CommMonoidWithZero α
inst✝¹ : NormalizationMonoid α
inst✝ : UniqueFactorizationMonoid α
a : α
ane0 : a ≠ 0
⊢ (normalizedFactors a).prod ~ᵤ a

Tactic:
rw [normalizedFactors, factors, dif_neg ane0]
  refine Associated.trans ?_ (Classical.choose_spec (exists_prime_factors a ane0)).2
  rw [← Associates.mk_eq_mk_iff_associated, ← Associates.prod_mk, ← Associates.prod_mk,
    Multiset.map_map]
  congr 2
  ext
  rw [Function.comp_apply, Associates.mk_normalize]

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 _)

Goal state after:
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
ia : Irreducible a
⊢ normalizedFactors (a ::ₘ s).prod = Multiset.map normalize (a ::ₘ s)
Module: Mathlib.RingTheory.UniqueFactorizationDomain.NormalizedFactors

Goal state before:
pp: α : Type u_1
inst✝² : CommMonoidWithZero α
inst✝¹ : NormalizationMonoid α
inst✝ : UniqueFactorizationMonoid α
p x : α
h : x ≠ 0
x✝ : Irreducible p ∧ normalize p = p ∧ p ∣ x
h₁ : Irreducible p
h₂ : normalize p = p
h₃ : p ∣ x
y : α
hy₁ : y ∈ factors x
hy₂ : p ~ᵤ y
⊢ normalize y = p

Tactic:
rwa [← h₂, normalize_eq_normalize_iff_associated, Associated.comm]

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

Goal state before:
pp: case inr
α : Type u_1
inst✝³ : CommMonoidWithZero α
inst✝² : NormalizationMonoid α
inst✝¹ : UniqueFactorizationMonoid α
inst✝ : Subsingleton αˣ
m : Multiset α
h : ∀ p ∈ m, Prime p
h✝ : Nontrivial α
⊢ normalizedFactors m.prod = m

Tactic:
simpa only [← Multiset.rel_eq, ← associated_eq_eq] using
      prime_factors_unique prime_of_normalized_factor h
        (prod_normalizedFactors (m.prod_ne_zero_of_prime h))

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

Goal state before:
pp: R : Type u
inst✝¹ : CommRing R
inst✝ : IsDomain R
n : ℕ
a : R
hn : n = 0
h : X ^ n - C a = 0
⊢ (nthRoots n a).card ≤ n

Tactic:
simp [nthRoots, roots, h, empty_eq_zero, Multiset.card_zero]

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

Goal state before:
pp: case refine_1
α : Type u_1
inst✝¹ : CommMonoidWithZero α
inst✝ : UniqueFactorizationMonoid α
p q : Multiset (Associates α)
s t : Multiset α
hs : ∀ a ∈ map (Quot.mk ⇑(Associated.setoid α)) t, Irreducible a
ht : ∀ a ∈ map (Quot.mk ⇑(Associated.setoid α)) s, Irreducible a
eq : (map (Quot.mk ⇑(Associated.setoid α)) t).prod = (map (Quot.mk ⇑(Associated.setoid α)) s).prod
⊢ ∀ x ∈ t, Irreducible x

Tactic:
exact fun a ha => irreducible_mk.1 <| hs _ <| Multiset.mem_map_of_mem _ ha

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:
by
  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.Algebra.Polynomial.Roots

Goal state before:
pp: S : Type v
T : Type w
inst✝⁵ : CommRing T
inst✝⁴ : IsDomain T
inst✝³ : CommRing S
inst✝² : IsDomain S
inst✝¹ : Algebra T S
inst✝ : Module.IsTorsionFree T S
p q : T[X]
hpq : p * q ≠ 0
⊢ (p * q).aroots S = p.aroots S + q.aroots S

Tactic:
suffices map (algebraMap T S) p * map (algebraMap T S) q ≠ 0 by
    rw [aroots_def, Polynomial.map_mul, roots_mul this]

Goal state after:
S : Type v
T : Type w
inst✝⁵ : CommRing T
inst✝⁴ : IsDomain T
inst✝³ : CommRing S
inst✝² : IsDomain S
inst✝¹ : Algebra T S
inst✝ : Module.IsTorsionFree T S
p q : T[X]
hpq : p * q ≠ 0
⊢ map (algebraMap T S) p * map (algebraMap T S) q ≠ 0
Module: Mathlib.RingTheory.Polynomial.Content

Goal state before:
pp: R : Type u_1
inst✝¹ : CommRing R
inst✝ : NormalizedGCDMonoid R
r : R
p : R[X]
⊢ Associated (C r * p).content (r * p.content)

Tactic:
by
  by_cases h0 : r = 0; · simp [h0]
  refine .trans (.of_eq ?_) (Finset.gcd_mul_left' _ _ _)
  rw [content]; refine congr (congr rfl ?_) ?_ <;> ext <;> simp [h0, mem_support_iff]

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

Goal state before:
pp: S : Type v
T : Type w
inst✝⁵ : CommRing T
inst✝⁴ : IsDomain T
inst✝³ : CommRing S
inst✝² : IsDomain S
inst✝¹ : Algebra T S
inst✝ : Module.IsTorsionFree T S
a : T
p : T[X]
ha : a ≠ 0
⊢ (a • p).aroots S = p.aroots S

Tactic:
rw [smul_eq_C_mul, aroots_C_mul _ ha]

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

Goal state before:
pp: T : Type w
inst✝⁴ : CommRing T
p : T[X]
S : Type u_1
inst✝³ : CommRing S
inst✝² : IsDomain S
inst✝¹ : Algebra T S
inst✝ : DecidableEq S
⊢ p.rootSet S = ↑(p.aroots S).toFinset

Tactic:
by
  rw [rootSet]
  convert! rfl

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

Goal state before:
pp: R : Type u
S : Type v
inst✝⁶ : CommRing R
inst✝⁵ : IsDomain R
inst✝⁴ : CommRing S
inst✝³ : Algebra S R
G : Type u_1
inst✝² : Monoid G
inst✝¹ : MulSemiringAction G R
inst✝ : SMulCommClass G S R
f : S[X]
g : G
x : R
hx : x ∈ f.rootSet R
⊢ g • x ∈ f.rootSet R

Tactic:
simp [mem_rootSet', aeval_smul, aeval_eq_zero_of_mem_rootSet hx, (mem_rootSet'.mp hx).1]

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

Goal state before:
pp: R : Type u
S : Type v
k : Type y
A : Type z
a b : R
n : ℕ
inst✝² : CommRing R
inst✝¹ : NoZeroDivisors R
inst✝ : NormalizationMonoid R
a✝ : R[X]
u : R[X]ˣ
h : a✝ ≠ 0
w : Rˣ
h2 : C ↑w = ↑u
⊢ C ↑(normUnit (a✝ * ↑u).leadingCoeff) = ↑u⁻¹ * C ↑(normUnit a✝.leadingCoeff)

Tactic:
rw [leadingCoeff_mul, ← h2, leadingCoeff_C, normUnit_mul_units _ (leadingCoeff_ne_zero.2 h),
      Units.eq_inv_mul_iff_mul_eq, Units.val_mul, C_mul, ← mul_assoc, ← h2, ← C_mul]

Goal state after:
R : Type u
S : Type v
k : Type y
A : Type z
a b : R
n : ℕ
inst✝² : CommRing R
inst✝¹ : NoZeroDivisors R
inst✝ : NormalizationMonoid R
a✝ : R[X]
u : R[X]ˣ
h : a✝ ≠ 0
w : Rˣ
h2 : C ↑w = ↑u
⊢ C (↑w * ↑w⁻¹) * C ↑(normUnit a✝.leadingCoeff) = C ↑(normUnit a✝.leadingCoeff)
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
s : R[X]
⊢ ∀ (n : ℕ) (s : R[X]), s.natDegree = n → p ∣ s ∧ q ∣ s → r ∣ s

Tactic:
clear s

Goal state after:
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
⊢ ∀ (n : ℕ) (s : R[X]), s.natDegree = n → p ∣ s ∧ q ∣ s → r ∣ s
Module: Mathlib.RingTheory.UniqueFactorizationDomain.FactorSet

Goal state before:
pp: case neg.inl
α : Type u_1
inst✝³ : CommMonoidWithZero α
inst✝² : UniqueFactorizationMonoid α
inst✝¹ : DecidableEq (Associates α)
inst✝ : (p : Associates α) → Decidable (Irreducible p)
a b : Associates α
hb : b ≠ 0
p : Associates α
hp : Irreducible p
hab : ∀ (d : Associates α), d ∣ a → d ∣ b → ¬Prime d
k : ℕ
habk : k ∣ p.count (a * b).factors
ha : ¬a = 0
hz : p.count a.factors = 0
⊢ k ∣ p.count a.factors

Tactic:
hz

Goal state after:
case neg.inl
α : Type u_1
inst✝³ : CommMonoidWithZero α
inst✝² : UniqueFactorizationMonoid α
inst✝¹ : DecidableEq (Associates α)
inst✝ : (p : Associates α) → Decidable (Irreducible p)
a b : Associates α
hb : b ≠ 0
p : Associates α
hp : Irreducible p
hab : ∀ (d : Associates α), d ∣ a → d ∣ b → ¬Prime d
k : ℕ
habk : k ∣ p.count (a * b).factors
ha : ¬a = 0
hz : p.count a.factors = 0
⊢ k ∣ 0
Module: Mathlib.RingTheory.UniqueFactorizationDomain.FactorSet

Goal state before:
pp: case neg.inl
α : Type u_1
inst✝³ : CommMonoidWithZero α
inst✝² : UniqueFactorizationMonoid α
inst✝¹ : DecidableEq (Associates α)
inst✝ : (p : Associates α) → Decidable (Irreducible p)
a b : Associates α
hb : b ≠ 0
p : Associates α
hp : Irreducible p
hab : ∀ (d : Associates α), d ∣ a → d ∣ b → ¬Prime d
k : ℕ
habk : k ∣ p.count (a * b).factors
ha : ¬a = 0
hz : p.count a.factors = 0
⊢ k ∣ p.count a.factors

pp: case neg.inr
α : Type u_1
inst✝³ : CommMonoidWithZero α
inst✝² : UniqueFactorizationMonoid α
inst✝¹ : DecidableEq (Associates α)
inst✝ : (p : Associates α) → Decidable (Irreducible p)
a b : Associates α
hb : b ≠ 0
p : Associates α
hp : Irreducible p
hab : ∀ (d : Associates α), d ∣ a → d ∣ b → ¬Prime d
k : ℕ
habk : k ∣ p.count (a * b).factors
ha : ¬a = 0
h : p.count b.factors = 0
⊢ k ∣ p.count a.factors

Tactic:
· rw [hz]
    exact dvd_zero k

Goal state after:
case neg.inr
α : Type u_1
inst✝³ : CommMonoidWithZero α
inst✝² : UniqueFactorizationMonoid α
inst✝¹ : DecidableEq (Associates α)
inst✝ : (p : Associates α) → Decidable (Irreducible p)
a b : Associates α
hb : b ≠ 0
p : Associates α
hp : Irreducible p
hab : ∀ (d : Associates α), d ∣ a → d ∣ b → ¬Prime d
k : ℕ
habk : k ∣ p.count (a * b).factors
ha : ¬a = 0
h : p.count b.factors = 0
⊢ k ∣ p.count a.factors
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
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 ⋯
⊢ ↑((fun f ↦ ⟨fun j ↦ piLTProj ⋯ f, ⋯⟩)
          ((fun f l ↦
              let k := hi.mid ⋯;
              ↑f ⟨↑k, ⋯⟩ ⟨↑l, ⋯⟩)
            f))
      j l =
    ↑f j l

Tactic:
obtain le | le := le_total j ⟨k, k.2.2⟩

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

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
Module: Mathlib.RingTheory.MvPolynomial.Basic

Goal state before:
pp: σ : Type u
R : Type v
inst✝¹ : CommSemiring R
p m : ℕ
inst✝ : CharP R p
n : ℕ
⊢ ↑n = 0 ↔ p ∣ n

Tactic:
by rw [← C_eq_coe_nat, ← C_0, C_inj, CharP.cast_eq_zero_iff R p]

Goal state after:
Module: Mathlib.RingTheory.Finiteness.Small

Goal state before:
pp: R : Type u_1
M : Type u_2
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
P Q : { P // Small.{u, u_2} ↥P }
⊢ P ≤ ⟨↑P ⊔ ↑Q, ⋯⟩

Tactic:
rw [← Subtype.coe_le_coe]

Goal state after:
R : Type u_1
M : Type u_2
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
P Q : { P // Small.{u, u_2} ↥P }
⊢ ↑P ≤ ↑⟨↑P ⊔ ↑Q, ⋯⟩
Module: Mathlib.RingTheory.Finiteness.Small

Goal state before:
pp: R : Type u_1
M : Type u_2
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
P Q : { P // Small.{u, u_2} ↥P }
⊢ Q ≤ ⟨↑P ⊔ ↑Q, ⋯⟩

Tactic:
rw [← Subtype.coe_le_coe]

Goal state after:
R : Type u_1
M : Type u_2
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
P Q : { P // Small.{u, u_2} ↥P }
⊢ ↑Q ≤ ↑⟨↑P ⊔ ↑Q, ⋯⟩
Module: Mathlib.RingTheory.MvPolynomial.Basic

Goal state before:
pp: σ : Type u
R : Type v
inst✝¹ : CommSemiring R
p m : ℕ
inst✝ : Finite σ
N : ℕ
this : Finite ↑{f | ∀ (a : σ), f a ≤ N}
⊢ Finite ↑{s | (s.sum fun x e ↦ e) ≤ N}

Tactic:
by
    rw [Set.finite_coe_iff] at this ⊢
    exact this.subset fun n hn i ↦ (eq_or_ne (n i) 0).elim
      (fun h ↦ h.trans_le N.zero_le) fun h ↦
        (Finset.single_le_sum (fun _ _ ↦ Nat.zero_le _) <| Finsupp.mem_support_iff.mpr h).trans hn

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

Goal state before:
pp: case h
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
x y : M ⊗[R] N
Sx : M →₀ N
hx : x = Sx.sum fun m n ↦ m ⊗ₜ[R] n
Sy : M →₀ N
hy : y = Sy.sum fun m n ↦ m ⊗ₜ[R] n
⊢ ((Sx.sum fun m n ↦ m ⊗ₜ[R] n) + Sy.sum fun m n ↦ m ⊗ₜ[R] n) = (Sx + Sy).sum fun m n ↦ m ⊗ₜ[R] n

Tactic:
exact (Finsupp.sum_add_index' (by simp) TensorProduct.tmul_add).symm

Goal state after:
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
M₁ : Submodule R M
N₁ : Submodule R N
s : Set (↥M₁ ⊗[R] ↥N₁)
hs : s.Finite
M' : Submodule R ↥M₁
N' : Submodule R ↥N₁
left✝¹ : Module.Finite R ↥M'
left✝ : Module.Finite R ↥N'
hM : Submodule.map M₁.subtype M' ≤ M₁
hN : Submodule.map N₁.subtype N' ≤ N₁
h : s ⊆ ↑(map (inclusion hM ∘ₗ M₁.subtype.submoduleMap M') (inclusion hN ∘ₗ N₁.subtype.submoduleMap N')).range
⊢ s ⊆ ↑(map (inclusion hM) (inclusion hN)).range

Tactic:
map_comp

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
M₁ : Submodule R M
N₁ : Submodule R N
s : Set (↥M₁ ⊗[R] ↥N₁)
hs : s.Finite
M' : Submodule R ↥M₁
N' : Submodule R ↥N₁
left✝¹ : Module.Finite R ↥M'
left✝ : Module.Finite R ↥N'
hM : Submodule.map M₁.subtype M' ≤ M₁
hN : Submodule.map N₁.subtype N' ≤ N₁
h : s ⊆ ↑(map (inclusion hM) (inclusion hN) ∘ₗ map (M₁.subtype.submoduleMap M') (N₁.subtype.submoduleMap N')).range
⊢ s ⊆ ↑(map (inclusion hM) (inclusion hN)).range
Module: Mathlib.LinearAlgebra.TensorProduct.Finiteness

Goal state before:
pp: case add
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
kx : ℕ
mx : Fin kx → M
nx : Fin kx → N
ky : ℕ
my : Fin ky → M
ny : Fin ky → N
⊢ ∃ k m n, ∑ j, mx j ⊗ₜ[R] nx j + ∑ j, my j ⊗ₜ[R] ny j = ∑ j, m j ⊗ₜ[R] n j

Tactic:
use kx + ky, Fin.addCases mx my, Fin.addCases nx ny

Goal state after:
case h
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
kx : ℕ
mx : Fin kx → M
nx : Fin kx → N
ky : ℕ
my : Fin ky → M
ny : Fin ky → N
⊢ ∑ j, mx j ⊗ₜ[R] nx j + ∑ j, my j ⊗ₜ[R] ny j = ∑ j, Fin.addCases mx my j ⊗ₜ[R] (fun i ↦ Fin.addCases nx ny i) j
Module: Mathlib.Order.Interval.Finset.Gaps

Goal state before:
pp: α : Type u_1
inst✝ : LinearOrder α
F : Finset (α × α)
k : ℕ
h : #F = k
a b : α
z : α × α
⊢ z ∈ ↑F → z ∈ (fun j ↦ ((F.intervalGapsWithin h a b ↑j).2, (F.intervalGapsWithin h a b ↑j.succ).1)) '' Iio k

Tactic:
hz

Goal state after:
α : Type u_1
inst✝ : LinearOrder α
F : Finset (α × α)
k : ℕ
h : #F = k
a b : α
z : α × α
hz : z ∈ ↑F
⊢ z ∈ (fun j ↦ ((F.intervalGapsWithin h a b ↑j).2, (F.intervalGapsWithin h a b ↑j.succ).1)) '' Iio k
Module: Mathlib.Algebra.BigOperators.Group.Finset.Gaps

Goal state before:
pp: case i_surj
α : Type u_1
β : Type u_2
inst✝¹ : LinearOrder α
inst✝ : CommGroup β
F : Finset (α × α)
k : ℕ
h : #F = k
a b : α
f : α → α → β
p : Fin (k + 1) → α × α := F.intervalGapsWithin h a b
z : α × α
⊢ z ∈ F → ∃ a, ∃ (_ : a ∈ range k), ((p ↑a).2, (p ↑a.succ).1) = z

Tactic:
hz

Goal state after:
case i_surj
α : Type u_1
β : Type u_2
inst✝¹ : LinearOrder α
inst✝ : CommGroup β
F : Finset (α × α)
k : ℕ
h : #F = k
a b : α
f : α → α → β
p : Fin (k + 1) → α × α := F.intervalGapsWithin h a b
z : α × α
hz : z ∈ F
⊢ ∃ a, ∃ (_ : a ∈ range k), ((p ↑a).2, (p ↑a.succ).1) = z
Module: Mathlib.Algebra.BigOperators.Group.Finset.Interval

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

Tactic:
by
  induction N with
  | zero => simp [sq]
  | succ N ih =>
    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.Data.List.Sym

Goal state before:
pp: case cons
α : Type u_1
β : Type u_2
f : α → β
x : α
xs : List α
ih : (map f xs).sym2 = map (Sym2.map f) xs.sym2
⊢ (map f (x :: xs)).sym2 = map (Sym2.map f) (x :: xs).sym2

Tactic:
simp [List.sym2, ih, Function.comp]

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

Goal state before:
pp: α : Type u_1
x : α
xs : List α
ih : xs.sym2.Nodup
h : x ∉ xs ∧ xs.Nodup
z : Sym2 α
⊢ z ∈ map (fun y ↦ s(x, y)) (x :: xs) → z ∈ xs.sym2 → False

Tactic:
hz

Goal state after:
α : Type u_1
x : α
xs : List α
ih : xs.sym2.Nodup
h : x ∉ xs ∧ xs.Nodup
z : Sym2 α
hz : z ∈ map (fun y ↦ s(x, y)) (x :: xs)
⊢ z ∈ xs.sym2 → False
Module: Mathlib.Data.List.Sym

Goal state before:
pp: α : Type u_1
n✝ : ℕ
xs✝ : List α
n : ℕ
x : α
xs : List α
h : (x :: xs).Nodup
z : Sym α (n + 1)
⊢ z ∈ map (fun p ↦ x ::ₛ p) (List.sym n (x :: xs)) → z ∈ List.sym (n + 1) xs → False

Tactic:
hz

Goal state after:
α : Type u_1
n✝ : ℕ
xs✝ : List α
n : ℕ
x : α
xs : List α
h : (x :: xs).Nodup
z : Sym α (n + 1)
hz : z ∈ map (fun p ↦ x ::ₛ p) (List.sym n (x :: xs))
⊢ z ∈ List.sym (n + 1) xs → False
Module: Mathlib.Algebra.BigOperators.WithTop

Goal state before:
pp: ι : Type u_1
M₀ : Type u_3
inst✝³ : CommMonoidWithZero M₀
inst✝² : NoZeroDivisors M₀
inst✝¹ : Nontrivial M₀
inst✝ : DecidableEq M₀
s : Finset ι
f : ι → WithTop M₀
i : ι
hi : i ∈ s
hi' : f i = ⊤
h : ∀ j ∈ s, f j ≠ 0
a✝¹ : ι
a✝ : a✝¹ ∈ s.erase i
⊢ f a✝¹ ≠ 0

Tactic:
simp_all only [ne_eq, mem_erase, not_false_eq_true]

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

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
P : α → Prop
f : (a : α) → P a → β
s : Sym2 α
g : (p : α × α) → (∀ a ∈ s(p.1, p.2), P a) → Sym2 β := fun p H ↦ s(f p.1 ⋯, f p.2 ⋯)
p q : α × α
hpq : Rel α p q
Hq : ∀ a ∈ Quot.mk (Rel α) q, P a
⊢ Eq.ndrec (motive := fun x ↦ (∀ a ∈ x, P a) → Sym2 β) (g p) ⋯ Hq = g q Hq

Tactic:
by
    rw [rel_iff'] at hpq
    have Hp : ∀ a ∈ s(p.1, p.2), P a := fun a hmem =>
      Hq a (Sym2.mk_eq_mk_iff.2 hpq ▸ hmem : a ∈ s(q.1, q.2))
    have h : ∀ {s₂ e H}, Eq.ndrec (motive := fun s => (∀ a ∈ s, P a) → Sym2 β) (g p) (b := s₂) e H =
      g p Hp := by
      rintro s₂ rfl _
      rfl
    refine h.trans (Quot.sound ?_)
    rw [rel_iff', Prod.mk.injEq, Prod.swap_prod_mk]
    apply hpq.imp <;> rintro rfl <;> simp

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

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
z : Sym2 α
f : α → β
a : α
⊢ (fun x ↦ (↑x).diagElem ⋯) ((fun a ↦ ⟨diag a, ⋯⟩) a) = a

Tactic:
by simp [diag]

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

Goal state before:
pp: α : Type u_1
r : α → α → Prop
sym : Std.Symm r
⊢ fromRel sym = ∅ ↔ r = ⊥

Tactic:
refine ⟨fun h ↦ ?_, (· ▸ fromRel_bot)⟩

Goal state after:
α : Type u_1
r : α → α → Prop
sym : Std.Symm r
h : fromRel sym = ∅
⊢ r = ⊥
Module: Mathlib.RingTheory.IsTensorProduct

Goal state before:
pp: R : Type u_1
S : Type v₃
inst✝¹⁵ : CommSemiring R
inst✝¹⁴ : CommSemiring S
inst✝¹³ : Algebra R S
A : Type u_8
B : Type u_9
inst✝¹² : CommRing A
inst✝¹¹ : CommRing B
inst✝¹⁰ : Algebra R A
inst✝⁹ : Algebra R B
inst✝⁸ : Algebra A B
inst✝⁷ : Algebra S B
inst✝⁶ : IsScalarTower R A B
inst✝⁵ : IsScalarTower R S B
inst✝⁴ : IsPushout R S A B
M : Type u_10
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : Module A M
inst✝ : IsScalarTower R A M
m : M
⊢ (cancelBaseChangeAux R S A B M).symm.symm (1 ⊗ₜ[A] m) = 1 ⊗ₜ[R] m

Tactic:
simp [cancelBaseChangeAux, TensorProduct.one_def]

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

Goal state before:
pp: case mp
C : Type u
inst✝ : CategoryStruct.{v, u} C
X Y Z : C
⊢ pair X Y Z → X = Z ∨ Y = Z

Tactic:
rintro ⟨_ | _⟩

Goal state after:
case mp.inl
C : Type u
inst✝ : CategoryStruct.{v, u} C
X Y : C
val✝ : Unit
⊢ X = Sum.elim (fun x ↦ X) (fun x ↦ Y) (Sum.inl val✝) ∨ Y = Sum.elim (fun x ↦ X) (fun x ↦ Y) (Sum.inl val✝)

case mp.inr
C : Type u
inst✝ : CategoryStruct.{v, u} C
X Y : C
val✝ : Unit
⊢ X = Sum.elim (fun x ↦ X) (fun x ↦ Y) (Sum.inr val✝) ∨ Y = Sum.elim (fun x ↦ X) (fun x ↦ Y) (Sum.inr val✝)
Module: Mathlib.Logic.Lemmas

Goal state before:
pp: f : Prop → Prop
x✝ : ∃ p, f p
p : Prop
h : f p
⊢ f True ∨ f False

Tactic:
refine (em p).imp ?_ ?_ <;> intro H

Goal state after:
case refine_1
f : Prop → Prop
x✝ : ∃ p, f p
p : Prop
h : f p
H : p
⊢ f True

case refine_2
f : Prop → Prop
x✝ : ∃ p, f p
p : Prop
h : f p
H : ¬p
⊢ f False
Module: Mathlib.Combinatorics.Quiver.Symmetric

Goal state before:
pp: V : Type u_2
inst✝ : Quiver V
h : HasInvolutiveReverse V
a b : V
f : a ⟶ b
g : b ⟶ a
⊢ f = reverse g ↔ reverse f = g

Tactic:
← reverse_inj,

Goal state after:
V : Type u_2
inst✝ : Quiver V
h : HasInvolutiveReverse V
a b : V
f : a ⟶ b
g : b ⟶ a
⊢ reverse f = reverse (reverse g) ↔ reverse f = g
Module: Mathlib.CategoryTheory.Functor.ReflectsIso.Basic

Goal state before:
pp: C : Type u_1
inst✝⁴ : Category.{v_1, u_1} C
D : Type u_2
inst✝³ : Category.{v_2, u_2} D
E : Type u_3
inst✝² : Category.{v_3, u_3} E
F : C ⥤ D
G : D ⥤ E
inst✝¹ : F.ReflectsIsomorphisms
inst✝ : G.ReflectsIsomorphisms
A✝ B✝ : C
f : A✝ ⟶ B✝
hf : IsIso (G.map (F.map f))
⊢ IsIso f

Tactic:
have := isIso_of_reflects_iso (F.map f) G
    exact isIso_of_reflects_iso f F

Goal state after:
Module: Mathlib.CategoryTheory.Equivalence

Goal state before:
pp: C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
e : C ≌ D
Y : D
⊢ e.unit.app (e.inverse.obj Y) ≫
      e.inverse.map
          (e.counitInv.app (e.functor.obj (e.inverse.obj Y)) ≫ e.functor.map (e.unitInv.app (e.inverse.obj Y))) ≫
        e.inverse.map (e.counit.app Y) =
    𝟙 (e.inverse.obj Y)

Tactic:
map_comp

Goal state after:
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
e : C ≌ D
Y : D
⊢ e.unit.app (e.inverse.obj Y) ≫
      (e.inverse.map (e.counitInv.app (e.functor.obj (e.inverse.obj Y))) ≫
          e.inverse.map (e.functor.map (e.unitInv.app (e.inverse.obj Y)))) ≫
        e.inverse.map (e.counit.app Y) =
    𝟙 (e.inverse.obj Y)
Module: Mathlib.CategoryTheory.Whiskering

Goal state before:
pp: C : Type u₁
inst✝² : Category.{v₁, u₁} C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
E : Type u₃
inst✝ : Category.{v₃, u₃} E
F : C ⥤ D
G H : D ⥤ E
α : G ⟶ H
X Y : C
f : X ⟶ Y
⊢ (F ⋙ G).map f ≫ α.app (F.obj Y) = α.app (F.obj X) ≫ (F ⋙ H).map f

Tactic:
by rw [Functor.comp_map, Functor.comp_map, α.naturality]

Goal state after: