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

Goal state before:
pp: case h
R : Type u
inst✝ : Semiring R
f : R[X]
n : ℕ
hn : (∀ d < n, f.coeff d = 0) → X ^ n ∣ f
hd : ∀ d < n + 1, f.coeff d = 0
g : R[X]
hgf : f = X ^ n * g
this : 0 = g.coeff 0
k : R[X]
hgk : g = X * k
⊢ f = X ^ n * (X * k)

Tactic:
← hgk

Goal state after:
case h
R : Type u
inst✝ : Semiring R
f : R[X]
n : ℕ
hn : (∀ d < n, f.coeff d = 0) → X ^ n ∣ f
hd : ∀ d < n + 1, f.coeff d = 0
g : R[X]
hgf : f = X ^ n * g
this : 0 = g.coeff 0
k : R[X]
hgk : g = X * k
⊢ f = X ^ n * g
Module: Mathlib.Algebra.Polynomial.Derivative

Goal state before:
pp: R : Type u
inst✝ : Semiring R
p : R[X]
n : ℕ
h : n ∈ (derivative p).support
h1 : p.coeff (n + 1) = 0
⊢ (derivative p).coeff n = 0

Tactic:
rw [coeff_derivative, h1, zero_mul]

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

Goal state before:
pp: case neg
R : Type u
inst✝ : Ring R
r a : R
h✝ : Nontrivial R
hr : ¬C r = 0
h : (C r).natDegree < (X - C a).natDegree
⊢ multiplicity (X - C a) (C r) = 0

Tactic:
simp_rw [multiplicity_eq_zero.mpr ((monic_X_sub_C a).not_dvd_of_natDegree_lt hr h)]

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

Goal state before:
pp: case h.right.a
α : Type u_1
s : ℕ → Set α
⊢ ⨅ i, 𝓟 (s i) ≤ ⨅ i, 𝓟 (⋂ m, ⋂ (_ : m ≤ i), s m)

Tactic:
rw [le_iInf_iff]

Goal state after:
case h.right.a
α : Type u_1
s : ℕ → Set α
⊢ ∀ (i : ℕ), ⨅ i, 𝓟 (s i) ≤ 𝓟 (⋂ m, ⋂ (_ : m ≤ i), s m)
Module: Mathlib.Order.Filter.CountablyGenerated

Goal state before:
pp: case a
α : Type u_1
s : ℕ → Set α
⊢ ⨅ i, 𝓟 (⋂ m, ⋂ (_ : m ≤ i), s m) ≤ ⨅ i, 𝓟 (s i)

Tactic:
rw [le_iInf_iff]

Goal state after:
case a
α : Type u_1
s : ℕ → Set α
⊢ ∀ (i : ℕ), ⨅ i, 𝓟 (⋂ m, ⋂ (_ : m ≤ i), s m) ≤ 𝓟 (s i)
Module: Mathlib.Order.Filter.Finite

Goal state before:
pp: α : Type u
β : Type v
s : Finset α
f : α → Filter β
t : Set β
⊢ t ∈ ⨅ x, f ↑x ↔ ∃ p, (∀ a ∈ s, p a ∈ f a) ∧ t = ⋂ x, p ↑x

Tactic:
refine ⟨fun h => ?_, ?_⟩

Goal state after:
case refine_1
α : Type u
β : Type v
s : Finset α
f : α → Filter β
t : Set β
h : t ∈ ⨅ x, f ↑x
⊢ ∃ p, (∀ a ∈ s, p a ∈ f a) ∧ t = ⋂ x, p ↑x

case refine_2
α : Type u
β : Type v
s : Finset α
f : α → Filter β
t : Set β
⊢ (∃ p, (∀ a ∈ s, p a ∈ f a) ∧ t = ⋂ x, p ↑x) → t ∈ ⨅ x, f ↑x
Module: Mathlib.Order.Filter.Pi

Goal state before:
pp: ι : Type u_1
α : ι → Type u_2
f₁ f₂ : (i : ι) → Filter (α i)
inst✝ : ∀ (i : ι), (f₁ i).NeBot
⊢ pi f₁ = pi f₂ ↔ f₁ = f₂

Tactic:
refine ⟨fun h => ?_, congr_arg pi⟩

Goal state after:
ι : Type u_1
α : ι → Type u_2
f₁ f₂ : (i : ι) → Filter (α i)
inst✝ : ∀ (i : ι), (f₁ i).NeBot
h : pi f₁ = pi f₂
⊢ f₁ = f₂
Module: Mathlib.Order.Filter.Cofinite

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

Tactic:
simpa using hs.compl_mem_cofinite

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

Goal state before:
pp: case pos
α : Type u_4
β : Type u_5
inst✝ : LinearOrder β
s : Set α
hs : s.Nonempty
f : α → β
hf : Tendsto f cofinite atTop
y : α
hys : y ∈ s
x : β
hx : f y < x
this : {y | ¬x ≤ f y}.Finite
⊢ ∃ a₀ ∈ s, ∀ a ∈ s, f a₀ ≤ f a

Tactic:
simp only [not_le] at this

Goal state after:
case pos
α : Type u_4
β : Type u_5
inst✝ : LinearOrder β
s : Set α
hs : s.Nonempty
f : α → β
hf : Tendsto f cofinite atTop
y : α
hys : y ∈ s
x : β
hx : f y < x
this : {y | f y < x}.Finite
⊢ ∃ a₀ ∈ s, ∀ a ∈ s, f a₀ ≤ f a
Module: Mathlib.Algebra.BigOperators.Associated

Goal state before:
pp: case cons.inl
M₀ : Type u_3
inst✝¹ : CommMonoidWithZero M₀
inst✝ : IsCancelMulZero M₀
c : M₀
s : Multiset M₀
hind :
  ∀ (x y : M₀),
    x * y ∈ closure {r | IsUnit r ∨ Prime r} →
      (∀ y ∈ s, IsUnit y ∨ Prime y) → s.prod = x * y → x ∈ closure {r | IsUnit r ∨ Prime r}
x y : M₀
hxy : x * y ∈ closure {r | IsUnit r ∨ Prime r}
hprod : c * s.prod = x * y
hs : ∀ a ∈ s, IsUnit a ∨ Prime a
ha₁ : IsUnit c
⊢ x ∈ closure {r | IsUnit r ∨ Prime r}

Tactic:
rcases ha₁.exists_right_inv with ⟨k, hk⟩
      refine hind x (y * k) ?_ hs ?_
      · simp only [← mul_assoc, ← hprod, ← Multiset.prod_cons, mul_comm]
        refine multiset_prod_mem _ _ (Multiset.forall_mem_cons.2 ⟨subset_closure ?_,
          Multiset.forall_mem_cons.2 ⟨subset_closure ?_, fun t ht => subset_closure (hs t ht)⟩⟩)
        · left; exact .of_mul_eq_one_right _ hk
        · left; exact ha₁
      · rw [← mul_one s.prod, ← hk, ← mul_assoc, ← mul_assoc, mul_eq_mul_right_iff, mul_comm]
        left; exact hprod

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

Goal state before:
pp: case zero
R : Type u
inst✝¹ : CommRing R
inst✝ : IsDomain R
p : R[X]
⊢ (p ^ 0).roots = 0 • p.roots

Tactic:
rw [pow_zero, roots_one, zero_smul, empty_eq_zero]

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

Goal state before:
pp: case neg.refine_1
R : Type u_2
inst✝¹ : CommRing R
inst✝ : StrongNormalizedGCDMonoid R
r : R
p : R[X]
h0 : ¬r = 0
a✝ : ℕ
⊢ a✝ ∈ (C r * p).support ↔ a✝ ∈ p.support

Tactic:
simp [h0, mem_support_iff]

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

Goal state before:
pp: case neg.refine_2
R : Type u_2
inst✝¹ : CommRing R
inst✝ : StrongNormalizedGCDMonoid R
r : R
p : R[X]
h0 : ¬r = 0
x✝ : ℕ
⊢ (C r * p).coeff x✝ = r * p.coeff x✝

Tactic:
simp [h0, mem_support_iff]

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

Goal state before:
pp: case neg.refine_1
R : Type u_1
inst✝¹ : CommRing R
inst✝ : NormalizedGCDMonoid R
r : R
p : R[X]
h0 : ¬r = 0
a✝ : ℕ
⊢ a✝ ∈ (C r * p).support ↔ a✝ ∈ p.support

Tactic:
simp [h0, mem_support_iff]

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

Goal state before:
pp: case neg.refine_2
R : Type u_1
inst✝¹ : CommRing R
inst✝ : NormalizedGCDMonoid R
r : R
p : R[X]
h0 : ¬r = 0
x✝ : ℕ
⊢ (C r * p).coeff x✝ = r * p.coeff x✝

Tactic:
simp [h0, mem_support_iff]

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

Goal state before:
pp: case ha
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
⊢ (algebraMap T S) a ≠ 0

Tactic:
rwa [map_ne_zero_iff]

Goal state after:
case ha.hf
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
⊢ Function.Injective ⇑(algebraMap T S)
Module: Mathlib.Algebra.Polynomial.Roots

Goal state before:
pp: S : Type v
T : Type w
inst✝³ : CommRing T
p : T[X]
inst✝² : CommRing S
inst✝¹ : IsDomain S
inst✝ : Algebra T S
a : S
h : a ∈ rootSet 0 S
hf : p = 0
⊢ False

Tactic:
rootSet_zero

Goal state after:
S : Type v
T : Type w
inst✝³ : CommRing T
p : T[X]
inst✝² : CommRing S
inst✝¹ : IsDomain S
inst✝ : Algebra T S
a : S
h : a ∈ ∅
hf : p = 0
⊢ False
Module: Mathlib.Algebra.Polynomial.Roots

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

Tactic:
by
  obtain ⟨q, he⟩ := p.prod_multiset_X_sub_C_dvd
  use q, he.symm
  obtain rfl | hq := eq_or_ne q 0
  · rw [mul_zero] at he
    subst he
    simp
  constructor
  · conv_rhs => rw [he]
    rw [(monic_multisetProd_X_sub_C p.roots).natDegree_mul' hq,
      natDegree_multiset_prod_X_sub_C_eq_card]
  · replace he := congr_arg roots he.symm
    rw [roots_mul, roots_multiset_prod_X_sub_C] at he
    exacts [add_eq_left.1 he, mul_ne_zero (monic_multisetProd_X_sub_C p.roots).ne_zero hq]

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✝ : DecidableEq B
p : A[X]
f : A →+* B
hf : Function.Injective ⇑f
b : B
hp0 : p = 0
⊢ count b (Multiset.map (⇑f) p.roots) ≤ rootMultiplicity b (map f p)

pp: case neg
A : Type u_1
B : Type u_2
inst✝³ : CommRing A
inst✝² : CommRing B
inst✝¹ : IsDomain A
inst✝ : DecidableEq B
p : A[X]
f : A →+* B
hf : Function.Injective ⇑f
b : B
hp0 : ¬p = 0
⊢ count b (Multiset.map (⇑f) p.roots) ≤ rootMultiplicity b (map f p)

Tactic:
· simp only [hp0, roots_zero, Multiset.map_zero, Multiset.count_zero, Polynomial.map_zero,
      rootMultiplicity_zero, le_refl]

Goal state after:
case neg
A : Type u_1
B : Type u_2
inst✝³ : CommRing A
inst✝² : CommRing B
inst✝¹ : IsDomain A
inst✝ : DecidableEq B
p : A[X]
f : A →+* B
hf : Function.Injective ⇑f
b : B
hp0 : ¬p = 0
⊢ count b (Multiset.map (⇑f) p.roots) ≤ rootMultiplicity b (map f p)
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
⊢ False

Tactic:
have s0 : s ≠ 0 := by
      contrapose rs
      simp [rs]

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
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
⊢ False
Module: Mathlib.RingTheory.Polynomial.UniqueFactorization

Goal state before:
pp: case pos
R : Type u_1
inst✝² : CommSemiring R
inst✝¹ : NoZeroDivisors R
inst✝ : WfDvdMonoid R
f a : R[X]
ane0 : a ≠ 0
c : R[X]
not_unit_c : ¬IsUnit c
hac : a * c = 0
⊢ Prod.Lex (fun x1 x2 ↦ x1 < x2) DvdNotUnit (↑a.degree, a.leadingCoeff) (⊤, (a * c).leadingCoeff)

Tactic:
rw [hac, Polynomial.leadingCoeff_zero]
        apply Prod.Lex.left
        exact WithTop.coe_lt_top _

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

Goal state before:
pp: α : Type u_1
inst✝⁴ : CommMonoidWithZero α
inst✝³ : UniqueFactorizationMonoid α
inst✝² : DecidableEq (Associates α)
inst✝¹ : (p : Associates α) → Decidable (Irreducible p)
inst✝ : Nontrivial α
a : Associates α
ha : a ≠ 0
p : Associates α
hp : Irreducible p
k : ℕ
⊢ k ∣ p.count (a ^ k).factors

Tactic:
rw [count_pow ha hp]
  apply dvd_mul_right

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

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

Tactic:
refine Nat.find_le ⟨1, ?_⟩
    rw [mul_one]
    symm
    exact eq_pow_count_factors_of_dvd_pow hp h

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

Goal state before:
pp: R : Type u_3
S : Type u_4
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
A B : Subalgebra R S
hle : A ≤ B
x : S
h : IsAlgebraic (↥A) x
this✝ : Algebra ↥A ↥B := (Subalgebra.inclusion hle).toAlgebra
this : IsScalarTower (↥A) (↥B) S
⊢ IsAlgebraic (↥B) x

Tactic:
exact h.extendScalars (Subalgebra.inclusion_injective hle)

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

Goal state before:
pp: R : Type u_1
inst✝⁷ : CommSemiring R
ι : Type u_2
inst✝⁶ : DecidableEq ι
inst✝⁵ : Preorder ι
G : ι → Type u_3
inst✝⁴ : (i : ι) → AddCommMonoid (G i)
inst✝³ : (i : ι) → Module R (G i)
f : (i j : ι) → i ≤ j → G i →ₗ[R] G j
M : Type u_4
inst✝² : AddCommMonoid M
inst✝¹ : Module R M
inst✝ : DirectedSystem G fun x1 x2 x3 ↦ ⇑(f x1 x2 x3)
x✝⁴ x✝³ x✝² : ι
x✝¹ : x✝² ≤ x✝³
x✝ : x✝³ ≤ x✝⁴
x : G x✝² ⊗[R] M
⊢ (LinearMap.rTensor M (f x✝³ x✝⁴ x✝)) ((LinearMap.rTensor M (f x✝² x✝³ x✝¹)) x) = (LinearMap.rTensor M (f x✝² x✝⁴ ⋯)) x

Tactic:
by
    convert! ← (LinearMap.rTensor_comp_apply M _ _ x).symm; ext; apply DirectedSystem.map_map' f

Goal state after:
Module: Mathlib.Order.DirectedInverseSystem

Goal state before:
pp: case inl
ι : 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
k : ι
hk : k ∈ Iic i⁺
lt_succ : ∀ {j : ι}, j ≤ i → j < i⁺
hj : i⁺ ∈ Iic i⁺
h : k ≤ i⁺
x : F i⁺
⊢ (piEquivSucc equiv e hi ⟨k, hk⟩) (f h x) = piLTProj h ((piEquivSucc equiv e hi ⟨i⁺, hj⟩) x)

Tactic:
obtain rfl | hk := le_succ_iff_eq_or_le.mp hk
    · simp [InverseSystem.map_self]
    · funext l
      rw [piEquivSucc, piSplitLE_lt (lt_succ hk),
        ← InverseSystem.map_map (f := f) hk (le_succ i), ← H, piLTProj, nat le_rfl]
      simp [piSplitLE_lt (l.2.trans_le hk)]

Goal state after:
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✝⁶ : Flat R M
N : Type u_1
N' : Type u_2
N'' : Type u_3
inst✝⁵ : AddCommGroup N
inst✝⁴ : AddCommGroup N'
inst✝³ : AddCommGroup N''
inst✝² : Module R N
inst✝¹ : Module R N'
inst✝ : Module R N''
f : N →ₗ[R] N'
g : N' →ₗ[R] N''
exact : Function.Exact ⇑f ⇑g
⊢ Function.Exact ⇑(lTensor M f) ⇑(lTensor M g)

Tactic:
by
  let π : N' →ₗ[R] N' ⧸ LinearMap.range f := Submodule.mkQ _
  let ι : N' ⧸ LinearMap.range f →ₗ[R] N'' :=
    Submodule.subtype _ ∘ₗ (LinearMap.quotKerEquivRange g).toLinearMap ∘ₗ
      Submodule.quotEquivOfEq (LinearMap.range f) (LinearMap.ker g)
        (LinearMap.exact_iff.mp exact).symm
  suffices exact1 : Function.Exact (f.lTensor M) (π.lTensor M) by
    rw [show g = ι.comp π from rfl, lTensor_comp]
    exact exact1.comp_injective _ (lTensor_preserves_injective_linearMap ι <| by
      simpa [ι, -Subtype.val_injective] using Subtype.val_injective) (map_zero _)
  exact _root_.lTensor_exact _ (fun x ↦ by simp [π]) Quotient.mk''_surjective

Goal state after:
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).dens = s.dens + t.dens

Tactic:
dens,

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

Goal state before:
pp: case inr
α : Type u_2
β : Type u_3
inst✝¹ : Fintype α
s : Finset α
inst✝ : Fintype β
f : α ↪ β
h✝ : Nonempty α
⊢ (map f s).dens ≤ s.dens

Tactic:
dens,

Goal state after:
case inr
α : Type u_2
β : Type u_3
inst✝¹ : Fintype α
s : Finset α
inst✝ : Fintype β
f : α ↪ β
h✝ : Nonempty α
⊢ ↑(#(map f s)) / ↑(Fintype.card β) ≤ ↑(#s) / ↑(Fintype.card α)
Module: Mathlib.Data.Finset.Density

Goal state before:
pp: case inr
α : Type u_2
inst✝ : Fintype α
s : Finset α
h✝ : Nonempty α
⊢ ↑(Fintype.card α) * s.dens = ↑(#s)

Tactic:
dens,

Goal state after:
case inr
α : Type u_2
inst✝ : Fintype α
s : Finset α
h✝ : Nonempty α
⊢ ↑(Fintype.card α) * (↑(#s) / ↑(Fintype.card α)) = ↑(#s)
Module: Mathlib.Data.Finset.Density

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

Tactic:
dens,

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

Goal state before:
pp: α : Type u_2
inst✝¹ : Fintype α
s t : Finset α
inst✝ : DecidableEq α
h : #s = #t
⊢ (t \ s).dens + s.dens = (t \ s).dens + t.dens

Tactic:
dens,

Goal state after:
α : Type u_2
inst✝¹ : Fintype α
s t : Finset α
inst✝ : DecidableEq α
h : #s = #t
⊢ ↑(#(t \ s)) / ↑(Fintype.card α) + ↑(#s) / ↑(Fintype.card α) =
    ↑(#(t \ s)) / ↑(Fintype.card α) + ↑(#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 : (↑s).PairwiseDisjoint t ∧ ∀ j ∈ ↑s, Disjoint (t i) (t j)
j : κ
⊢ (t i ∪ ⋃ x ∈ s, t x).mulIndicator f j = (t i).mulIndicator f j * ∏ x ∈ s, (t x).mulIndicator f j

Tactic:
mulIndicator_union_of_notMem_inter,

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 : κ
⊢ (t i).mulIndicator f j * (⋃ x ∈ s, t x).mulIndicator f j = (t i).mulIndicator f j * ∏ x ∈ s, (t x).mulIndicator f j

case cons.h
ι : 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 : κ
⊢ j ∉ t i ∩ ⋃ x ∈ s, t x
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 : ι) → Group (G i)
inst✝² : Group C
inst✝¹ : ∀ (i j : ι) (h : i ≤ j), MonoidHomClass (T h) (G i) (G j)
inst✝ : ∀ (i : ι), MonoidHomClass (H i) (G i) C
g : (i : ι) → H i
h : ∀ (i j : ι) (h : i ≤ j) (x : G i), (g i) x = (g j) ((f i j h) x)
x✝ : DirectLimit G f
z : ℤ
i : ι
x : G i
⊢ DirectLimit.lift f (fun x ↦ ⇑(g x)) h (⟦⟨i, x⟩⟧ ^ z) = DirectLimit.lift f (fun x ↦ ⇑(g x)) h ⟦⟨i, x⟩⟧ ^ z

Tactic:
by simp_rw [zpow_def, lift_def, map_zpow (g i)]

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

Goal state before:
pp: ι : Type u_1
κ : Type u_2
M : Type u_4
inst✝¹ : AddCommMonoid M
inst✝ : Module ℚ≥0 M
s : Finset ι
f : ι → M
t : Finset κ
g : κ → M
i : ι → κ
j : κ → ι
hi : ∀ a ∈ s, i a ∈ t
hj : ∀ a ∈ t, j a ∈ s
left_inv : ∀ a ∈ s, j (i a) = a
right_inv : ∀ a ∈ t, i (j a) = a
h : ∀ a ∈ s, f a = g (i a)
⊢ 𝔼 i ∈ s, f i = 𝔼 i ∈ t, g i

Tactic:
by
  simp_rw [expect, card_nbij' i j hi hj left_inv right_inv,
    sum_nbij' i j hi hj left_inv right_inv h]

Goal state after:
Module: Mathlib.Data.Int.Interval

Goal state before:
pp: a b : ℤ
h : a ≤ b + 1
⊢ ↑(#(Icc a b)) = b + 1 - a

Tactic:
rw [card_Icc, toNat_sub_of_le h]

Goal state after:
Module: Mathlib.RingTheory.IsTensorProduct

Goal state before:
pp: R : Type u_1
inst✝⁶ : CommSemiring R
M₁ : Type u_2
M₂ : Type u_3
M : Type u_4
inst✝⁵ : AddCommMonoid M₁
inst✝⁴ : AddCommMonoid M₂
inst✝³ : AddCommMonoid M
inst✝² : Module R M₁
inst✝¹ : Module R M₂
inst✝ : Module R M
f : M₁ →ₗ[R] M₂ →ₗ[R] M
h : IsTensorProduct f
motive : M → Prop
m : M
zero : motive 0
tmul : ∀ (x : M₁) (y : M₂), motive ((f x) y)
add : ∀ (x y : M), motive x → motive y → motive (x + y)
⊢ motive m

Tactic:
rw [← h.equiv.right_inv m]
  generalize h.equiv.invFun m = y
  change motive (TensorProduct.lift f y)
  induction y with
  | zero => rwa [map_zero]
  | tmul _ _ =>
    rw [TensorProduct.lift.tmul]
    apply tmul
  | add _ _ _ _ =>
    rw [map_add]
    apply add <;> assumption

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 β
inst✝ : DecidableEq α
ha : a ∉ s
f : Finset α → β
⊢ Disjoint s.powerset (image (insert a) s.powerset)

Tactic:
aesop (add simp [disjoint_left, insert_subset_iff])

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

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝ : CommMonoid β
n : ℕ
s : Finset α
f : ℕ → β
⊢ ?m.20 ^ #(powersetCard n s) = f n ^ (#s).choose n

pp: α : Type u_1
β : Type u_2
inst✝ : CommMonoid β
n : ℕ
s : Finset α
f : ℕ → β
⊢ ∀ a ∈ powersetCard n s, f #a = ?m.20

pp: α : Type u_1
β : Type u_2
inst✝ : CommMonoid β
n : ℕ
s : Finset α
f : ℕ → β
⊢ β

Tactic:
card_powersetCard

Goal state after:
α : Type u_1
β : Type u_2
inst✝ : CommMonoid β
n : ℕ
s : Finset α
f : ℕ → β
⊢ ?m.20 ^ (#s).choose n = f n ^ (#s).choose n

α : Type u_1
β : Type u_2
inst✝ : CommMonoid β
n : ℕ
s : Finset α
f : ℕ → β
⊢ ∀ a ∈ powersetCard n s, f #a = ?m.20

α : Type u_1
β : Type u_2
inst✝ : CommMonoid β
n : ℕ
s : Finset α
f : ℕ → β
⊢ β
Module: Mathlib.RingTheory.IsTensorProduct

Goal state before:
pp: 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
⊢ (IsTensorProduct.equiv h) (r • x) = r • (IsTensorProduct.equiv h) x

Tactic:
refine TensorProduct.induction_on x ?_ ?_ ?_

Goal state after:
case refine_1
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
⊢ (IsTensorProduct.equiv h) (r • 0) = r • (IsTensorProduct.equiv h) 0

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)

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.List.Sym

Goal state before:
pp: α : Type u_1
xs : List α
z : Sym2 α
⊢ z ∈ xs.sym2 ↔ ∀ y ∈ z, y ∈ xs

Tactic:
refine z.ind (fun a b => ?_)
  simp [mk_mem_sym2_iff]

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
a b : α
⊢ a = b ∨ x = b ∧ a = x → a = b

Tactic:
rintro (rfl | ⟨rfl, rfl⟩)

Goal state after:
case inl
α : Type u_1
x : α
xs : List α
ih : xs.sym2.Nodup
h : x ∉ xs ∧ xs.Nodup
a : α
⊢ a = a

case inr
α : Type u_1
xs : List α
ih : xs.sym2.Nodup
a : α
h : a ∉ xs ∧ xs.Nodup
⊢ a = a
Module: Mathlib.Data.List.Sym

Goal state before:
pp: α : Type u_1
β : Type u_3
f : α → β
n✝ : ℕ
xs✝ : List α
n : ℕ
x : α
xs : List α
⊢ map (fun p ↦ f x ::ₛ p) (map (Sym.map f) (List.sym n (x :: xs))) ++ List.sym (n + 1) (map f xs) =
    map (Sym.map f) (List.sym (n + 1) (x :: xs))

Tactic:
sym_map f (n + 1) xs

Goal state after:
α : Type u_1
β : Type u_3
f : α → β
n✝ : ℕ
xs✝ : List α
n : ℕ
x : α
xs : List α
⊢ map (fun p ↦ f x ::ₛ p) (map (Sym.map f) (List.sym n (x :: xs))) ++ map (Sym.map f) (List.sym (n + 1) xs) =
    map (Sym.map f) (List.sym (n + 1) (x :: xs))