mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.GroupTheory.OrderOfElement

Goal state before:
pp: case hx
G : Type u_1
inst✝ : Monoid G
x y : G
h : Commute x y
hy : IsOfFinOrder y
hdvd : ∀ (p : ℕ), Nat.Prime p → p ∣ orderOf x → p * orderOf x ∣ orderOf y
hoy : 0 < orderOf y
hxy : orderOf x ∣ orderOf y
⊢ orderOf (x * y) ∣ orderOf y

pp: case hd
G : Type u_1
inst✝ : Monoid G
x y : G
h : Commute x y
hy : IsOfFinOrder y
hdvd : ∀ (p : ℕ), Nat.Prime p → p ∣ orderOf x → p * orderOf x ∣ orderOf y
hoy : 0 < orderOf y
hxy : orderOf x ∣ orderOf y
⊢ ∀ (p : ℕ), Nat.Prime p → p ∣ orderOf y → ¬orderOf (x * y) ∣ orderOf y / p

Tactic:
· exact h.orderOf_mul_dvd_lcm.trans (Nat.lcm_dvd hxy dvd_rfl)

Goal state after:
case hd
G : Type u_1
inst✝ : Monoid G
x y : G
h : Commute x y
hy : IsOfFinOrder y
hdvd : ∀ (p : ℕ), Nat.Prime p → p ∣ orderOf x → p * orderOf x ∣ orderOf y
hoy : 0 < orderOf y
hxy : orderOf x ∣ orderOf y
⊢ ∀ (p : ℕ), Nat.Prime p → p ∣ orderOf y → ¬orderOf (x * y) ∣ orderOf y / p
Module: Mathlib.GroupTheory.OrderOfElement

Goal state before:
pp: G : Type u_1
inst✝ : Monoid G
x : G
n m✝ : ℕ
hx : IsOfFinOrder x
m k : ℕ
hmn : m ≤ m + k
⊢ x ^ k = 1 ↔ m + k ≡ m [MOD orderOf x]

Tactic:
pow_eq_one_iff_modEq

Goal state after:
G : Type u_1
inst✝ : Monoid G
x : G
n m✝ : ℕ
hx : IsOfFinOrder x
m k : ℕ
hmn : m ≤ m + k
⊢ k ≡ 0 [MOD orderOf x] ↔ m + k ≡ m [MOD orderOf x]
Module: Mathlib.GroupTheory.OrderOfElement

Goal state before:
pp: G : Type u_1
inst✝ : LeftCancelMonoid G
x : G
m✝ n m k : ℕ
hmn : m ≤ m + k
⊢ x ^ k = 1 ↔ m + k ≡ m [MOD orderOf x]

Tactic:
pow_eq_one_iff_modEq

Goal state after:
G : Type u_1
inst✝ : LeftCancelMonoid G
x : G
m✝ n m k : ℕ
hmn : m ≤ m + k
⊢ k ≡ 0 [MOD orderOf x] ↔ m + k ≡ m [MOD orderOf x]
Module: Mathlib.GroupTheory.OrderOfElement

Goal state before:
pp: case neg
G : Type u_1
inst✝ : Group G
x : G
i : ℤ
h : ¬IsOfFinOrder x
⊢ (x ^ i) ^ 0 = 1

Tactic:
_root_.pow_zero

Goal state after:
case neg
G : Type u_1
inst✝ : Group G
x : G
i : ℤ
h : ¬IsOfFinOrder x
⊢ 1 = 1
Module: Mathlib.GroupTheory.OrderOfElement

Goal state before:
pp: G : Type u_1
inst✝ : Group G
x y : G
hx : IsOfFinOrder x
x✝ : y ∈ zpowers x
i : ℤ
hi : (fun x_1 ↦ x ^ x_1) i = y
⊢ (fun x_1 ↦ x ^ x_1) (i % ↑(orderOf x)).natAbs = y

Tactic:
dsimp only
    rwa [← zpow_natCast, Int.natAbs_of_nonneg <| Int.emod_nonneg _ <|
      Int.natCast_ne_zero_iff_pos.2 <| hx.orderOf_pos, zpow_mod_orderOf]

Goal state after:
Module: Mathlib.Algebra.CharP.Frobenius

Goal state before:
pp: R : Type u_1
inst✝¹ : CommSemiring R
p m n : ℕ
inst✝ : ExpChar R p
x : R
⊢ (iterateFrobenius R p (m + n)) x = (iterateFrobenius R p m) ((iterateFrobenius R p n) x)

Tactic:
by
  simp_rw [iterateFrobenius_def, add_comm m n, pow_add, pow_mul]

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

Goal state before:
pp: case zero
n b : ℕ
hn : n ≠ 0
i : ℕ
h2 : 1 ≤ i
h : i < n
pp : Prime 0
hb : n < 0 ^ b
h1 : 0 ^ i ∣ n
⊢ i < b

Tactic:
rw [zero_pow (by lia), zero_dvd_iff] at h1
    exact (hn h1).elim

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

Goal state before:
pp: case refine_1
n k : ℕ
hn : n ≠ 0
hk : k ≠ 0
h : n ∣ k ^ n
⊢ n.primeFactors ⊆ k.primeFactors

pp: case refine_2
n k : ℕ
hn : n ≠ 0
hk : k ≠ 0
h : n.primeFactors ⊆ k.primeFactors
⊢ n ∣ k ^ n

Tactic:
· grw [← Nat.primeFactors_pow k hn, Nat.primeFactors_mono h <| pow_ne_zero n hk]

Goal state after:
case refine_2
n k : ℕ
hn : n ≠ 0
hk : k ≠ 0
h : n.primeFactors ⊆ k.primeFactors
⊢ n ∣ k ^ n
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✝ : ℕ
⊢ f (if p ∣ n✝ then q.coeff (n✝ / p) else 0) = if p ∣ n✝ then (map f q).coeff (n✝ / p) else 0

Tactic:
split_ifs <;> simp_all

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

Goal state before:
pp: case pos
R : Type u
inst✝ : Semiring R
p : R[X]
ih : ∀ m < p.natDegree, ∀ {p : R[X]} {x : ℕ}, p.natDegree < x → p.natDegree = m → (⇑derivative)^[x] p = 0
t : ℕ
hx : p.natDegree < t.succ
hp : p.natDegree = 0
⊢ (⇑derivative)^[t] (derivative p) = 0

pp: case neg
R : Type u
inst✝ : Semiring R
p : R[X]
ih : ∀ m < p.natDegree, ∀ {p : R[X]} {x : ℕ}, p.natDegree < x → p.natDegree = m → (⇑derivative)^[x] p = 0
t : ℕ
hx : p.natDegree < t.succ
hp : ¬p.natDegree = 0
⊢ (⇑derivative)^[t] (derivative p) = 0

Tactic:
· rw [derivative_of_natDegree_zero hp, iterate_derivative_zero]

Goal state after:
case neg
R : Type u
inst✝ : Semiring R
p : R[X]
ih : ∀ m < p.natDegree, ∀ {p : R[X]} {x : ℕ}, p.natDegree < x → p.natDegree = m → (⇑derivative)^[x] p = 0
t : ℕ
hx : p.natDegree < t.succ
hp : ¬p.natDegree = 0
⊢ (⇑derivative)^[t] (derivative p) = 0
Module: Mathlib.Algebra.Polynomial.Expand

Goal state before:
pp: R : Type u
inst✝¹ : CommRing R
inst✝ : IsDomain R
p : ℕ
hp : 0 < p
f : R[X]
hf1 : IsUnit ((expand R p) f)
hf2 : (expand R p) f = C (f.coeff 0)
⊢ IsUnit f

Tactic:
hf2,

Goal state after:
R : Type u
inst✝¹ : CommRing R
inst✝ : IsDomain R
p : ℕ
hp : 0 < p
f : R[X]
hf1 : IsUnit (C (f.coeff 0))
hf2 : (expand R p) f = C (f.coeff 0)
⊢ IsUnit f
Module: Mathlib.Algebra.Polynomial.Expand

Goal state before:
pp: R : Type u
inst✝¹ : CommRing R
inst✝ : IsDomain R
p : ℕ
hp : 0 < p
f : R[X]
hf1 : IsUnit (f.coeff 0)
hf2 : f = C (f.coeff 0)
⊢ IsUnit f

Tactic:
hf2,

Goal state after:
R : Type u
inst✝¹ : CommRing R
inst✝ : IsDomain R
p : ℕ
hp : 0 < p
f : R[X]
hf1 : IsUnit (f.coeff 0)
hf2 : f = C (f.coeff 0)
⊢ IsUnit (C (f.coeff 0))
Module: Mathlib.RingTheory.Polynomial.Tower

Goal state before:
pp: R : Type u_1
A : Type u_2
B : Type u_3
inst✝⁶ : CommSemiring R
inst✝⁵ : CommSemiring A
inst✝⁴ : Semiring B
inst✝³ : Algebra R A
inst✝² : Algebra A B
inst✝¹ : Algebra R B
inst✝ : IsScalarTower R A B
x : B
p : R[X]
⊢ (aeval x) (map (algebraMap R A) p) = (aeval x) p

Tactic:
rw [aeval_def, aeval_def, eval₂_map, IsScalarTower.algebraMap_eq R A B]

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

Goal state before:
pp: α : Type u_1
ι' : Sort u_5
f : Filter α
h : f.IsCountablyGenerated
p : ι' → Prop
s : ι' → Set α
hs : f.HasBasis p s
⊢ ∃ x, f = ⨅ i, 𝓟 (x i)

Tactic:
rcases h with ⟨s, hsc, rfl⟩
    rw [generate_eq_biInf]
    exact countable_biInf_principal_eq_seq_iInf hsc

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

Goal state before:
pp: case inl
R : Type u
inst✝¹ : CommRing R
inst✝ : IsDomain R
p : R[X]
hpq : p ∣ 0
h₁ : natDegree 0 ≤ p.natDegree
h₂ : p.leadingCoeff = leadingCoeff 0
⊢ p = 0

pp: case inr
R : Type u
inst✝¹ : CommRing R
inst✝ : IsDomain R
p q : R[X]
hpq : p ∣ q
h₁ : q.natDegree ≤ p.natDegree
h₂ : p.leadingCoeff = q.leadingCoeff
hq : q ≠ 0
⊢ p = q

Tactic:
· simpa using h₂

Goal state after:
case inr
R : Type u
inst✝¹ : CommRing R
inst✝ : IsDomain R
p q : R[X]
hpq : p ∣ q
h₁ : q.natDegree ≤ p.natDegree
h₂ : p.leadingCoeff = q.leadingCoeff
hq : q ≠ 0
⊢ p = q
Module: Mathlib.Order.Filter.Prod

Goal state before:
pp: α : Type u_1
β : Type u_2
f : Filter α
g : Filter β
p : α × β → Prop
⊢ (∀ᶠ (x : α × β) in f ×ˢ g, p x) ↔ ∀ᶠ (y : β × α) in g ×ˢ f, p y.swap

Tactic:
prod_comm

Goal state after:
α : Type u_1
β : Type u_2
f : Filter α
g : Filter β
p : α × β → Prop
⊢ (∀ᶠ (x : α × β) in map Prod.swap (g ×ˢ f), p x) ↔ ∀ᶠ (y : β × α) in g ×ˢ f, p y.swap
Module: Mathlib.Algebra.Polynomial.Derivative

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

Tactic:
mul_right_comm

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

Goal state before:
pp: α : Type u_1
β : Type u_2
a : α
f : Filter β
⊢ (map Prod.mk (pure a)).seq f = map (Prod.mk a) f

Tactic:
map_pure,

Goal state after:
α : Type u_1
β : Type u_2
a : α
f : Filter β
⊢ (pure (Prod.mk a)).seq f = map (Prod.mk a) f
Module: Mathlib.Algebra.Polynomial.Derivative

Goal state before:
pp: R : Type u
inst✝¹ : CommRing R
inst✝ : DecidableEq R
S : Multiset R
r : R
hr : r ∈ S
⊢ eval r (derivative (Multiset.map (fun a ↦ X - C a) S).prod) = (Multiset.map (fun a ↦ r - a) (S.erase r)).prod

Tactic:
← Multiset.cons_erase hr

Goal state after:
R : Type u
inst✝¹ : CommRing R
inst✝ : DecidableEq R
S : Multiset R
r : R
hr : r ∈ S
⊢ eval r (derivative (Multiset.map (fun a ↦ X - C a) (r ::ₘ S.erase r)).prod) =
    (Multiset.map (fun a ↦ r - a) (S.erase r)).prod
Module: Mathlib.Algebra.Polynomial.Derivative

Goal state before:
pp: R : Type u
inst✝ : CommRing R
k : ℕ
ind : ∀ {P : R[X]}, P.degree < ↑k → (⇑derivative)^[k] P = 0
P : R[X]
h : P.degree < ↑(k + 1)
hP : ¬P = 0
hP' : ¬derivative P = 0
⊢ (⇑derivative)^[k] (derivative P) = 0

Tactic:
have hP'' : P.natDegree ≠ 0 := by
          contrapose hP'
          exact derivative_of_natDegree_zero hP'
        refine ind <| (natDegree_lt_iff_degree_lt hP').mp ?_
        linarith [(natDegree_lt_iff_degree_lt hP).mpr h, natDegree_derivative_lt hP'']

Goal state after:
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✝¹ : IsDomain R
inst✝ : IsTorsionFree R M
hw : ∀ (i : σ), w i ≠ 0
n : R
s : σ
h : n = 0 ∨ w s = 0
⊢ n = 0

Tactic:
or_iff_not_imp_right

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✝¹ : IsDomain R
inst✝ : IsTorsionFree R M
hw : ∀ (i : σ), w i ≠ 0
n : R
s : σ
h : ¬w s = 0 → n = 0
⊢ n = 0
Module: Mathlib.Algebra.Polynomial.Roots

Goal state before:
pp: R : Type u
inst✝¹ : CommRing R
inst✝ : IsDomain R
s : Multiset R
⊢ (Multiset.map (fun a ↦ X - C a) s).bind roots = s

pp: case a
R : Type u
inst✝¹ : CommRing R
inst✝ : IsDomain R
s : Multiset R
⊢ 0 ∉ Multiset.map (fun a ↦ X - C a) s

Tactic:
Multiset.bind_map

Goal state after:
R : Type u
inst✝¹ : CommRing R
inst✝ : IsDomain R
s : Multiset R
⊢ (s.bind fun a ↦ (X - C a).roots) = s

case a
R : Type u
inst✝¹ : CommRing R
inst✝ : IsDomain R
s : Multiset R
⊢ 0 ∉ Multiset.map (fun a ↦ X - C a) s
Module: Mathlib.Algebra.Polynomial.Roots

Goal state before:
pp: S : Type v
T : Type w
inst✝³ : CommRing T
inst✝² : CommRing S
inst✝¹ : IsDomain S
inst✝ : Algebra T S
p : T[X]
⊢ (-p).aroots S = p.aroots S

Tactic:
rw [aroots, Polynomial.map_neg, roots_neg]

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

Goal state before:
pp: case neg
R : Type u_1
inst✝¹ : CommRing R
inst✝ : NormalizedGCDMonoid R
r : R
h0 : ¬C (normalize r) = 0
⊢ ↑{ val := C ↑(normUnit r)⁻¹, inv := C ↑(normUnit r), val_inv := ⋯, inv_val := ⋯ } = (C r).primPart

Tactic:
apply mul_left_cancel₀ h0

Goal state after:
case neg
R : Type u_1
inst✝¹ : CommRing R
inst✝ : NormalizedGCDMonoid R
r : R
h0 : ¬C (normalize r) = 0
⊢ C (normalize r) * ↑{ val := C ↑(normUnit r)⁻¹, inv := C ↑(normUnit r), val_inv := ⋯, inv_val := ⋯ } =
    C (normalize r) * (C r).primPart
Module: Mathlib.Algebra.Polynomial.Roots

Goal state before:
pp: R : Type u
inst✝¹ : CommRing R
inst✝ : IsDomain R
p : R[X]
hp : p ≠ 0
s : Multiset R
⊢ (Multiset.map (fun a ↦ X - C a) s).prod ∣ p ↔ s ≤ p.roots

Tactic:
by
  classical exact
  ⟨fun h =>
    Multiset.le_iff_count.2 fun r => by
      rw [count_roots, le_rootMultiplicity_iff hp, ← Multiset.prod_replicate, ←
        Multiset.map_replicate fun a => X - C a, ← Multiset.filter_eq]
      exact (Multiset.prod_dvd_prod_of_le <| Multiset.map_le_map <| s.filter_le _).trans h,
    fun h =>
    (Multiset.prod_dvd_prod_of_le <| Multiset.map_le_map h).trans p.prod_multiset_X_sub_C_dvd⟩

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

Goal state before:
pp: R : Type u_2
inst✝¹ : CommRing R
inst✝ : StrongNormalizedGCDMonoid R
p q : R[X]
h0 : ¬C (p * q).content = 0
⊢ (p * q).primPart = p.primPart * q.primPart

Tactic:
apply mul_left_cancel₀ h0

Goal state after:
R : Type u_2
inst✝¹ : CommRing R
inst✝ : StrongNormalizedGCDMonoid R
p q : R[X]
h0 : ¬C (p * q).content = 0
⊢ C (p * q).content * (p * q).primPart = C (p * q).content * (p.primPart * q.primPart)
Module: Mathlib.Order.DirectedInverseSystem

Goal state before:
pp: ι : Type u_6
F : ι → Type u_7
X : ι → Type u_8
inst✝² : LinearOrder ι
f : ⦃i j : ι⦄ → i ≤ j → F j → F i
inst✝¹ : SuccOrder ι
equivSucc : ⦃i : ι⦄ → ¬IsMax i → F i⁺ ≃ F i × X i
s : Set ι
inst✝ : WellFoundedLT ι
hs : IsLowerSet s
e₁ : (i : ↑s) → F ↑i ≃ piLT X ↑i
nat₁ : IsNatEquiv f e₁
compat₁ : ∀ {i : ι} (hsi : i⁺ ∈ s) (hi : ¬IsMax i) (x : F ↑⟨i⁺, hsi⟩), (e₁ ⟨i⁺, hsi⟩) x ⟨i, ⋯⟩ = ((equivSucc hi) x).2
e₂ : (i : ↑s) → F ↑i ≃ piLT X ↑i
nat₂ : IsNatEquiv f e₂
compat₂ : ∀ {i : ι} (hsi : i⁺ ∈ s) (hi : ¬IsMax i) (x : F ↑⟨i⁺, hsi⟩), (e₂ ⟨i⁺, hsi⟩) x ⟨i, ⋯⟩ = ((equivSucc hi) x).2
i✝ : ↑s
i : ι
nmax : ¬IsMax i
ih : ∀ (h : i ∈ s), e₁ ⟨i, h⟩ = e₂ ⟨i, h⟩
hi✝ : i⁺ ∈ s
x : F ↑⟨i⁺, hi✝⟩
j : ι
hj✝ : j ∈ Iio ↑⟨i⁺, hi✝⟩
hj : j < i
hi : i ∈ s
⊢ i ≤ i⁺

Tactic:
by exact le_succ i

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

Goal state before:
pp: σ : Type u
R : Type v
inst✝ : CommSemiring R
s t : Set (σ →₀ ℕ)
⊢ restrictSupport R (s + t) = restrictSupport R s * restrictSupport R t

Tactic:
apply le_antisymm
  · rw [restrictSupport_eq_span, Submodule.span_le, Set.image_subset_iff, Set.add_subset_iff]
    intro x hx y hy
    simp [show monomial (x + y) (1 : R) = monomial x 1 * monomial y 1 by simp, -monomial_mul,
      *, Submodule.mul_mem_mul]
  · rw [restrictSupport_eq_span, restrictSupport_eq_span, Submodule.span_mul_span,
      Submodule.span_le, Set.mul_subset_iff]
    simp +contextual [Set.add_mem_add]

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
x✝² x✝¹ x✝ : { P // Small.{u, u_2} ↥P }
hPR : x✝² ≤ x✝
hQR : x✝¹ ≤ x✝
⊢ ⟨↑x✝² ⊔ ↑x✝¹, ⋯⟩ ≤ x✝

Tactic:
by
    rw [← Subtype.coe_le_coe] at hPR hQR ⊢
    exact sup_le hPR hQR

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

Goal state before:
pp: R : Type u_1
inst✝⁵ : CommSemiring R
M : Type u_2
N : Type u_3
inst✝⁴ : AddCommMonoid M
inst✝³ : AddCommMonoid N
inst✝² : Module R M
inst✝¹ : Module R N
ι : Type u_6
κ : Type u_7
v : ι → M
w : κ → N
inst✝ : Module.Flat R M
hv : LinearIndependent R v
hw : LinearIndependent R w
⊢ ⇑(Finsupp.linearCombination R fun i ↦ v i.1 ⊗ₜ[R] w i.2) =
    ⇑(map (Finsupp.linearCombination R v) (Finsupp.linearCombination R w)) ∘ ⇑(finsuppTensorFinsupp' R ι κ).symm

Tactic:
rw [← LinearEquiv.coe_toLinearMap, ← LinearMap.coe_comp]

Goal state after:
R : Type u_1
inst✝⁵ : CommSemiring R
M : Type u_2
N : Type u_3
inst✝⁴ : AddCommMonoid M
inst✝³ : AddCommMonoid N
inst✝² : Module R M
inst✝¹ : Module R N
ι : Type u_6
κ : Type u_7
v : ι → M
w : κ → N
inst✝ : Module.Flat R M
hv : LinearIndependent R v
hw : LinearIndependent R w
⊢ ⇑(Finsupp.linearCombination R fun i ↦ v i.1 ⊗ₜ[R] w i.2) =
    ⇑(map (Finsupp.linearCombination R v) (Finsupp.linearCombination R w) ∘ₗ ↑(finsuppTensorFinsupp' R ι κ).symm)
Module: Mathlib.Data.Finset.Density

Goal state before:
pp: α : Type u_2
inst✝ : Fintype α
s t : Finset α
h : Disjoint s t
⊢ ↑(#(s.disjUnion t h)) / ↑(Fintype.card α) = ↑(#s) / ↑(Fintype.card α) + ↑(#t) / ↑(Fintype.card α)

Tactic:
card_disjUnion,

Goal state after:
α : Type u_2
inst✝ : Fintype α
s t : Finset α
h : Disjoint s t
⊢ ↑(#s + #t) / ↑(Fintype.card α) = ↑(#s) / ↑(Fintype.card α) + ↑(#t) / ↑(Fintype.card α)
Module: Mathlib.Data.Finset.Density

Goal state before:
pp: α : Type u_2
inst✝¹ : Fintype α
inst✝ : DecidableEq α
s t : Finset α
⊢ ↑(#(s ∪ t)) / ↑(Fintype.card α) + ↑(#(s ∩ t)) / ↑(Fintype.card α) =
    ↑(#s) / ↑(Fintype.card α) + ↑(#t) / ↑(Fintype.card α)

Tactic:
← add_div,

Goal state after:
α : Type u_2
inst✝¹ : Fintype α
inst✝ : DecidableEq α
s t : Finset α
⊢ (↑(#(s ∪ t)) + ↑(#(s ∩ t))) / ↑(Fintype.card α) = (↑(#s) + ↑(#t)) / ↑(Fintype.card α)
Module: Mathlib.Algebra.BigOperators.Group.Finset.Indicator

Goal state before:
pp: case cons
ι : Type u_1
κ : Type u_2
β : Type u_4
inst✝ : CommMonoid β
t : ι → Set κ
f : κ → β
i : ι
s : Finset ι
hi : i ∉ s
ih : (↑s).PairwiseDisjoint t → (⋃ i ∈ s, t i).mulIndicator f = fun a ↦ ∏ i ∈ s, (t i).mulIndicator f a
hs : (insert i ↑s).PairwiseDisjoint t
j : κ
⊢ (⋃ i_1 ∈ cons i s hi, t i_1).mulIndicator f j = ∏ i ∈ cons i s hi, (t i).mulIndicator f j

Tactic:
Set.pairwiseDisjoint_insert_of_notMem (Finset.mem_coe.not.2 hi)

Goal state after:
case cons
ι : Type u_1
κ : Type u_2
β : Type u_4
inst✝ : CommMonoid β
t : ι → Set κ
f : κ → β
i : ι
s : Finset ι
hi : i ∉ s
ih : (↑s).PairwiseDisjoint t → (⋃ i ∈ s, t i).mulIndicator f = fun a ↦ ∏ i ∈ s, (t i).mulIndicator f a
hs : (↑s).PairwiseDisjoint t ∧ ∀ j ∈ ↑s, Disjoint (t i) (t j)
j : κ
⊢ (⋃ i_1 ∈ cons i s hi, t i_1).mulIndicator f j = ∏ i ∈ cons i s hi, (t i).mulIndicator f j
Module: Mathlib.Data.Int.Interval

Goal state before:
pp: a b : ℤ
⊢ ↑(#(range (max a b + 1 - min a b).toNat)) = ↑((b - a).natAbs + 1)

Tactic:
card_range,

Goal state after:
a b : ℤ
⊢ ↑(max a b + 1 - min a b).toNat = ↑((b - a).natAbs + 1)
Module: Mathlib.RingTheory.IsTensorProduct

Goal state before:
pp: R : Type u_9
S : Type u_10
inst✝²⁰ : CommSemiring R
inst✝¹⁹ : CommSemiring S
inst✝¹⁸ : Algebra R S
M₁ : Type u_11
M₂ : Type u_12
M₃ : Type u_13
M₁₂ : Type u_14
M₂₃ : Type u_15
inst✝¹⁷ : AddCommMonoid M₁
inst✝¹⁶ : AddCommMonoid M₂
inst✝¹⁵ : AddCommMonoid M₃
inst✝¹⁴ : AddCommMonoid M₁₂
inst✝¹³ : AddCommMonoid M₂₃
inst✝¹² : Module R M₁
inst✝¹¹ : Module R M₂
inst✝¹⁰ : Module S M₂
inst✝⁹ : IsScalarTower R S M₂
inst✝⁸ : Module R M₃
inst✝⁷ : Module S M₃
inst✝⁶ : IsScalarTower R S M₃
inst✝⁵ : Module R M₁₂
inst✝⁴ : Module S M₁₂
inst✝³ : IsScalarTower R S M₁₂
inst✝² : Module R M₂₃
inst✝¹ : Module S M₂₃
inst✝ : IsScalarTower R S M₂₃
f : M₁ →ₗ[R] M₂ →ₗ[S] M₁₂
hf : IsTensorProduct (LinearMap.restrictScalars₁₂ R R f)
g : M₂ →ₗ[S] M₃ →ₗ[S] M₂₃
hg : IsTensorProduct g
x₁ : M₁
x₂ : M₂
x₃ : M₃
this : hf.equiv.symm ((f x₁) x₂) = x₁ ⊗ₜ[R] x₂
⊢ (assocAux f hf g hg) ((f x₁) x₂ ⊗ₜ[S] x₃) = x₁ ⊗ₜ[R] (g x₂) x₃

Tactic:
simp [IsTensorProduct.assocAux, this]

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

Goal state before:
pp: α : Type u_1
n : ℕ
f : α → ℕ
s : Finset α
a : α
ha : a ∉ s → f a ≡ 0 [MOD n]
hf : ∀ x ∈ s, x ≠ a → f x ≡ 0 [MOD n]
⊢ ∑ x ∈ s, f x ≡ f a [MOD n]

Tactic:
by
  simp only [← ZMod.natCast_eq_natCast_iff, cast_zero, cast_sum] at *
  apply Finset.sum_eq_single <;> assumption

Goal state after:
Module: Mathlib.Algebra.BigOperators.Ring.Nat

Goal state before:
pp: case refine_2
ι : Type u_1
M : Type u_2
f : ι → M
s : Finset M
hb : ∀ b ∈ s, {a | f a = b}.Finite
t : Finset M := ⋯.toFinset
ht : (f ⁻¹' ↑t).Finite
m : M
hm : m ∈ t
⊢ #({a ∈ ht.toFinset | f a = m}) = #⋯.toFinset

Tactic:
suffices {a | f a = m} ⊆ ht.toFinset from
      congr_arg (Finset.card ·) (Finset.ext_iff.mpr fun a ↦ by simpa using fun h ↦ this h)

Goal state after:
case refine_2
ι : Type u_1
M : Type u_2
f : ι → M
s : Finset M
hb : ∀ b ∈ s, {a | f a = b}.Finite
t : Finset M := ⋯.toFinset
ht : (f ⁻¹' ↑t).Finite
m : M
hm : m ∈ t
⊢ {a | f a = m} ⊆ ↑ht.toFinset
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)

pp: case refine_3
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 y : S ⊗[R] M),
    (IsTensorProduct.equiv h) (r • x) = r • (IsTensorProduct.equiv h) x →
      (IsTensorProduct.equiv h) (r • y) = r • (IsTensorProduct.equiv h) y →
        (IsTensorProduct.equiv h) (r • (x + y)) = r • (IsTensorProduct.equiv h) (x + y)

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

Goal state after:
case refine_3
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 y : S ⊗[R] M),
    (IsTensorProduct.equiv h) (r • x) = r • (IsTensorProduct.equiv h) x →
      (IsTensorProduct.equiv h) (r • y) = r • (IsTensorProduct.equiv h) y →
        (IsTensorProduct.equiv h) (r • (x + y)) = r • (IsTensorProduct.equiv h) (x + y)
Module: Mathlib.Data.Finset.Sym

Goal state before:
pp: α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : CommMonoid α
n : ℕ
k : Sym α n
s : Finset α
x : α
hx : x ∈ k
hk : ∀ a ∈ k, a ∈ s
⊢ x ∈ s

Tactic:
exact hk x hx

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

Goal state before:
pp: ι : Type u_1
M : Type u_2
inst✝¹ : LinearOrder ι
inst✝ : AddCommMonoid M
s : Finset ι
p : Sym2 ι → M
| ∑ i ∈ s.offDiag with i.1 ≤ i.2, p s(i.1, i.2)

Tactic:
← Finset.sum_subtype_eq_sum_filter

Goal state after:
ι : Type u_1
M : Type u_2
inst✝¹ : LinearOrder ι
inst✝ : AddCommMonoid M
s : Finset ι
p : Sym2 ι → M
| ∑ x ∈ Finset.subtype (fun i ↦ i.1 ≤ i.2) s.offDiag, p s((↑x).1, (↑x).2)
Module: Mathlib.Data.Sym.Sym2

Goal state before:
pp: case refl
α : Type u_1
β : Type u_2
γ : Type u_3
z : Sym2 α
f : α → β
a b a' : α
h : Rel α (a, b) (a', a')
⊢ Eq.ndrec (motive := fun x ↦ x.IsDiag → α) (fun x ↦ a) ⋯ ⋯ = a'

Tactic:
cases h <;> rfl

Goal state after:
Module: Mathlib.CategoryTheory.Iso

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
F : C ⥤ D
X Y Z : C
i : X ≅ Y
j : Y ≅ Z
⊢ F.mapIso (i ≪≫ j) = F.mapIso i ≪≫ F.mapIso j

Tactic:
by
  ext; apply Functor.map_comp

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

Goal state before:
pp: case a
C : Type u
inst✝¹ : Category.{v, u} C
P : ObjectProperty C
inst✝ : P.IsClosedUnderIsomorphisms
⊢ P.isoClosure ≤ P

pp: case a
C : Type u
inst✝¹ : Category.{v, u} C
P : ObjectProperty C
inst✝ : P.IsClosedUnderIsomorphisms
⊢ P ≤ P.isoClosure

Tactic:
· intro X ⟨Y, hY, ⟨e⟩⟩
    exact prop_of_iso P e.symm hY

Goal state after:
case a
C : Type u
inst✝¹ : Category.{v, u} C
P : ObjectProperty C
inst✝ : P.IsClosedUnderIsomorphisms
⊢ P ≤ P.isoClosure
Module: Mathlib.CategoryTheory.EssentialImage

Goal state before:
pp: C : Type u₁
D : Type u₂
inst✝¹ : Category.{v₁, u₁} C
inst✝ : Category.{v₂, u₂} D
F : C ⥤ D
h : Function.Surjective F.obj
Y : D
⊢ F.essImage Y

Tactic:
by
    obtain ⟨X, rfl⟩ := h Y
    apply obj_mem_essImage

Goal state after:
Module: Mathlib.CategoryTheory.EssentialImage

Goal state before:
pp: case refine_2
C : Type u₁
D : Type u₂
inst✝¹ : Category.{v₁, u₁} C
inst✝ : Category.{v₂, u₂} D
F : C ⥤ D
Y : D
X : C
e : F.obj X ≅ Y
⊢ ⊤.map F Y

Tactic:
exact ⟨X, by simp, ⟨e⟩⟩

Goal state after:
Module: Mathlib.CategoryTheory.Opposites

Goal state before:
pp: C : Type u₁
inst✝ : Category.{v₁, u₁} C
X✝ Y✝ : Cᵒᵖ
f : X✝ ⟶ Y✝
⊢ 𝟙 X✝ ≫ f = f

Tactic:
rw [← op_comp_unop, unop_id, comp_id, Quiver.Hom.op_unop]

Goal state after: