mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Algebra.BigOperators.Associated

Goal state before:
pp: case cons.inr.inl.refine_1
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}
hs : ∀ a ∈ s, IsUnit a ∨ Prime a
ha₂ : Prime c✝
c : M₀
hprod : c✝ * s.prod = c✝ * (c * y)
hc : x = c✝ * c
⊢ c✝ ∈ {r | IsUnit r ∨ Prime r}

Tactic:
right

Goal state after:
case cons.inr.inl.refine_1
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}
hs : ∀ a ∈ s, IsUnit a ∨ Prime a
ha₂ : Prime c✝
c : M₀
hprod : c✝ * s.prod = c✝ * (c * y)
hc : x = c✝ * c
⊢ Prime c✝
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 • w s = 0
⊢ n = 0

Tactic:
rw [smul_eq_zero, or_iff_not_imp_right] at h

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

Goal state before:
pp: case inl
α : Type u_1
inst✝² : CommMonoidWithZero α
inst✝¹ : NormalizationMonoid α
inst✝ : UniqueFactorizationMonoid α
h : Subsingleton α
⊢ Multiset.map normalize (if h : 1 = 0 then 0 else Classical.choose ⋯) = 0

Tactic:
simp [Subsingleton.elim (1 : α) 0]

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

Goal state before:
pp: R : Type u
inst✝¹ : CommRing R
inst✝ : IsDomain R
p q : R[X]
h : Associated p q
⊢ p.roots = q.roots

Tactic:
obtain ⟨u, rfl⟩ := h
  rw [eq_C_of_degree_eq_zero <| degree_coe_units u, mul_comm,
    roots_C_mul _ <| coeff_coe_units_zero_ne_zero u]

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

Goal state before:
pp: R : Type u
inst✝¹ : CommRing R
inst✝ : IsDomain R
p : R[X]
a b : R
ha : IsUnit a
f : R → R := fun x ↦ a * x + b
hf : Function.Bijective f
x : R
⊢ count (f x) (Multiset.map f (p.comp (C a * X + C b)).roots) = rootMultiplicity (f x) p

Tactic:
count_map_eq_count' f _ hf.injective,

Goal state after:
R : Type u
inst✝¹ : CommRing R
inst✝ : IsDomain R
p : R[X]
a b : R
ha : IsUnit a
f : R → R := fun x ↦ a * x + b
hf : Function.Bijective f
x : R
⊢ count x (p.comp (C a * X + C b)).roots = rootMultiplicity (f x) p
Module: Mathlib.RingTheory.UniqueFactorizationDomain.NormalizedFactors

Goal state before:
pp: α : Type u_1
inst✝² : CommMonoidWithZero α
inst✝¹ : NormalizationMonoid α
inst✝ : UniqueFactorizationMonoid α
a p : α
H : p ∈ normalizedFactors a
⊢ p ∣ a

Tactic:
by
  by_cases hcases : a = 0
  · rw [hcases]
    exact dvd_zero p
  · exact dvd_trans (Multiset.dvd_prod H) (Associated.dvd (prod_normalizedFactors hcases))

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

Goal state before:
pp: α : Type u_1
inst✝¹ : CommMonoidWithZero α
inst✝ : UniqueFactorizationMonoid α
x : α
n : ℕ
⊢ Rel Associated (factors (x ^ n)) (n • factors x)

Tactic:
match n with
  | 0 => rw [zero_nsmul, pow_zero, factors_one, rel_zero_right]
  | n + 1 =>
    by_cases h0 : x = 0
    · simp [h0, zero_pow n.succ_ne_zero, nsmul_zero]
    · rw [pow_succ', succ_nsmul']
      refine Rel.trans _ (factors_mul h0 (pow_ne_zero n h0)) ?_
      refine Rel.add ?_ <| factors_pow n
      exact rel_refl_of_refl_on fun y _ => Associated.refl _

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

Goal state before:
pp: α : Type u_1
inst✝¹ : CommMonoidWithZero α
inst✝ : UniqueFactorizationMonoid α
x y : Associates α
⊢ (if x * y = 0 then 0 else (map (Classical.choose ⋯) (normalizedFactors (x * y))).prod) =
    (if x = 0 then 0 else (map (Classical.choose ⋯) (normalizedFactors x)).prod) *
      if y = 0 then 0 else (map (Classical.choose ⋯) (normalizedFactors y)).prod

Tactic:
by_cases hx : x = 0

Goal state after:
case pos
α : Type u_1
inst✝¹ : CommMonoidWithZero α
inst✝ : UniqueFactorizationMonoid α
x y : Associates α
hx : x = 0
⊢ (if x * y = 0 then 0 else (map (Classical.choose ⋯) (normalizedFactors (x * y))).prod) =
    (if x = 0 then 0 else (map (Classical.choose ⋯) (normalizedFactors x)).prod) *
      if y = 0 then 0 else (map (Classical.choose ⋯) (normalizedFactors y)).prod

case neg
α : Type u_1
inst✝¹ : CommMonoidWithZero α
inst✝ : UniqueFactorizationMonoid α
x y : Associates α
hx : ¬x = 0
⊢ (if x * y = 0 then 0 else (map (Classical.choose ⋯) (normalizedFactors (x * y))).prod) =
    (if x = 0 then 0 else (map (Classical.choose ⋯) (normalizedFactors x)).prod) *
      if y = 0 then 0 else (map (Classical.choose ⋯) (normalizedFactors y)).prod
Module: Mathlib.Algebra.Polynomial.Roots

Goal state before:
pp: case neg
R : Type u
n : ℕ
inst✝⁵ : CommRing R
inst✝⁴ : IsDomain R
S : Type u_1
F : Type u_2
inst✝³ : CommRing S
inst✝² : IsDomain S
inst✝¹ : FunLike F R S
inst✝ : MonoidHomClass F R S
a x : R
hx : x ∈ nthRootsFinset n a
f : F
hn : ¬n = 0
⊢ f x ∈ nthRootsFinset n (f a)

Tactic:
· rw [mem_nthRootsFinset <| Nat.pos_of_ne_zero hn, ← map_pow, (mem_nthRootsFinset
      (Nat.pos_of_ne_zero hn) a).1 hx]

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

Goal state before:
pp: α : Type u_1
inst✝¹ : CommMonoidWithZero α
inst✝ : UniqueFactorizationMonoid α
x : Associates α
⊢ Associates.mk (if x = 0 then 0 else (map (Classical.choose ⋯) (normalizedFactors x)).prod) = x

Tactic:
by_cases hx : x = 0

Goal state after:
case pos
α : Type u_1
inst✝¹ : CommMonoidWithZero α
inst✝ : UniqueFactorizationMonoid α
x : Associates α
hx : x = 0
⊢ Associates.mk (if x = 0 then 0 else (map (Classical.choose ⋯) (normalizedFactors x)).prod) = x

case neg
α : Type u_1
inst✝¹ : CommMonoidWithZero α
inst✝ : UniqueFactorizationMonoid α
x : Associates α
hx : ¬x = 0
⊢ Associates.mk (if x = 0 then 0 else (map (Classical.choose ⋯) (normalizedFactors x)).prod) = x
Module: Mathlib.RingTheory.UniqueFactorizationDomain.Basic

Goal state before:
pp: case refine_2
R : Type u_2
inst✝¹ : CommMonoidWithZero R
inst✝ : UniqueFactorizationMonoid R
a✝ a : R
⊢ IsUnit a → a ≠ 0 → ∀ (b : R), ∃ a' b' c', IsRelPrime a' b' ∧ c' * a' = a ∧ c' * b' = b

Tactic:
a_unit

Goal state after:
case refine_2
R : Type u_2
inst✝¹ : CommMonoidWithZero R
inst✝ : UniqueFactorizationMonoid R
a✝ a : R
a_unit : IsUnit a
⊢ a ≠ 0 → ∀ (b : R), ∃ a' b' c', IsRelPrime a' b' ∧ c' * a' = a ∧ c' * b' = b
Module: Mathlib.Algebra.Polynomial.Roots

Goal state before:
pp: R : Type u
S : Type v
inst✝³ : CommRing R
inst✝² : IsDomain R
inst✝¹ : CommRing S
p : S[X]
inst✝ : Algebra S R
h : Function.Injective ⇑(algebraMap S R)
x : R
hp : p ≠ 0
⊢ x ∈ p.rootSet R ↔ (aeval x) p = 0

Tactic:
exact Multiset.mem_toFinset.trans (mem_roots_map_of_injective h hp)

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

Goal state before:
pp: R : Type u
inst✝ : CommRing R
p : R[X]
t : R
m : ℕ := rootMultiplicity t p
hm : m = rootMultiplicity t p
⊢ eval t ↑m ! * eval t ((⇑derivative)^[0] (p /ₘ (X - C t) ^ m)) = m ! • eval t (p /ₘ (X - C t) ^ m)

Tactic:
eval_natCast,

Goal state after:
R : Type u
inst✝ : CommRing R
p : R[X]
t : R
m : ℕ := rootMultiplicity t p
hm : m = rootMultiplicity t p
⊢ ↑m ! * eval t ((⇑derivative)^[0] (p /ₘ (X - C t) ^ m)) = m ! • eval t (p /ₘ (X - C t) ^ m)
Module: Mathlib.RingTheory.UniqueFactorizationDomain.Basic

Goal state before:
pp: case refine_3
R : Type u_2
inst✝¹ : CommMonoidWithZero R
inst✝ : UniqueFactorizationMonoid R
a : R
⊢ ∀ (a p : R),
    a ≠ 0 →
      Prime p →
        (a ≠ 0 → ∀ (b : R), ∃ a' b' c', IsRelPrime a' b' ∧ c' * a' = a ∧ c' * b' = b) →
          p * a ≠ 0 → ∀ (b : R), ∃ a' b' c', IsRelPrime a' b' ∧ c' * a' = p * a ∧ c' * b' = b

Tactic:
· intro a p a_ne_zero p_prime ih_a pa_ne_zero b
    by_cases h : p ∣ b
    · rcases h with ⟨b, rfl⟩
      obtain ⟨a', b', c', no_factor, ha', hb'⟩ := ih_a a_ne_zero b
      refine ⟨a', b', p * c', @no_factor, ?_, ?_⟩
      · rw [mul_assoc, ha']
      · rw [mul_assoc, hb']
    · obtain ⟨a', b', c', coprime, rfl, rfl⟩ := ih_a a_ne_zero b
      refine ⟨p * a', b', c', ?_, mul_left_comm _ _ _, rfl⟩
      intro q q_dvd_pa' q_dvd_b'
      rcases p_prime.left_dvd_or_dvd_right_of_dvd_mul q_dvd_pa' with p_dvd_q | q_dvd_a'
      · have : p ∣ c' * b' := dvd_mul_of_dvd_right (p_dvd_q.trans q_dvd_b') _
        contradiction
      exact coprime q_dvd_a' q_dvd_b'

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

Goal state before:
pp: R : Type u
inst✝¹ : CommRing R
inst✝ : IsDomain R
a p : R[X]
hp : p.Monic
hap : a ∣ p
⊢ a.leadingCoeff ∣ 1

Tactic:
simpa only [hp.leadingCoeff] using leadingCoeff_dvd_leadingCoeff hap

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

Goal state before:
pp: case inr
α : Type u_1
inst✝¹ : CommMonoidWithZero α
inst✝ : UniqueFactorizationMonoid α
a p : Associates α
hm : p ∈ a.factors
ha0 : a ≠ 0
⊢ p ∣ a

Tactic:
obtain ⟨a0, nza, ha'⟩ := exists_non_zero_rep ha0

Goal state after:
case inr
α : Type u_1
inst✝¹ : CommMonoidWithZero α
inst✝ : UniqueFactorizationMonoid α
a p : Associates α
hm : p ∈ a.factors
ha0 : a ≠ 0
a0 : α
nza : a0 ≠ 0
ha' : Associates.mk a0 = a
⊢ p ∣ a
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
⊢ s ≠ 0

Tactic:
contrapose 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
ps : p ∣ s
qs : q ∣ s
rs : s = 0
⊢ r ∣ s
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
inst✝¹ : DecidableEq R
inst✝ : DecidableEq k
f : R →+* k
x y : R[X]
x✝ : x ≠ 0
ih : EuclideanDomain.gcd (map f (y % x)) (map f x) = map f (EuclideanDomain.gcd (y % x) x)
⊢ EuclideanDomain.gcd (map f x) (map f y) = map f (EuclideanDomain.gcd x y)

Tactic:
by rw [gcd_val, ← map_mod, ih, ← gcd_val]

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

Goal state before:
pp: K : Type u_1
inst✝ : CommRing K
f : K[X]
a : K
⊢ f /ₘ (X - C a) + (X - C a) * derivative (f /ₘ (X - C a)) = derivative f

Tactic:
have key := by apply congrArg derivative <| X_sub_C_mul_divByMonic_eq_sub_modByMonic f a
  simpa only [derivative_mul, derivative_sub, derivative_X, derivative_C, sub_zero, one_mul,
    modByMonic_X_sub_C_eq_C_eval] using key

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

Goal state before:
pp: F : Type u_1
inst✝ : DivisionSemiring F
f : F[X]
h : Irreducible f
H : f.natDegree = 0
x : F
hf : C x = f
⊢ False

Tactic:
by_cases hx : x = 0

Goal state after:
case pos
F : Type u_1
inst✝ : DivisionSemiring F
f : F[X]
h : Irreducible f
H : f.natDegree = 0
x : F
hf : C x = f
hx : x = 0
⊢ False

case neg
F : Type u_1
inst✝ : DivisionSemiring F
f : F[X]
h : Irreducible f
H : f.natDegree = 0
x : F
hf : C x = f
hx : ¬x = 0
⊢ False
Module: Mathlib.RingTheory.Algebraic.Basic

Goal state before:
pp: R : Type u
inst✝ : CommRing R
f : R[X]
hf : f.natDegree ≠ 0
hf' : f.leadingCoeff ∈ R⁰
⊢ Transcendental R f

Tactic:
by
  simpa using (transcendental_X R).aeval f hf hf'

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

Goal state before:
pp: R : Type u
inst✝² : CommRing R
K : Type u_2
inst✝¹ : Field K
inst✝ : Algebra R K
x : K
⊢ IsAlgebraic R x⁻¹ ↔ IsAlgebraic R x

Tactic:
by_cases hx : x = 0

Goal state after:
case pos
R : Type u
inst✝² : CommRing R
K : Type u_2
inst✝¹ : Field K
inst✝ : Algebra R K
x : K
hx : x = 0
⊢ IsAlgebraic R x⁻¹ ↔ IsAlgebraic R x

case neg
R : Type u
inst✝² : CommRing R
K : Type u_2
inst✝¹ : Field K
inst✝ : Algebra R K
x : K
hx : ¬x = 0
⊢ IsAlgebraic R x⁻¹ ↔ IsAlgebraic R x
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
i : ι
g : G i
m : M
⊢ (toDirectLimit f M) ((of R ι G f i) g ⊗ₜ[R] m) =
    (of R ι (fun x ↦ G x ⊗[R] M) (fun i j h ↦ LinearMap.rTensor M (f i j h)) i) (g ⊗ₜ[R] m)

Tactic:
by
  rw [toDirectLimit, lift.tmul, lift_of]
  rfl

Goal state after:
Module: Mathlib.Order.DirectedInverseSystem

Goal state before:
pp: case refine_2
ι : 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 : ι
lim : IsSuccPrelimit i
ih : ∀ b < i, ∀ (h : b ∈ s), e₁ ⟨b, h⟩ = e₂ ⟨b, h⟩
hi : i ∈ s
x : F ↑⟨i, hi⟩
j : ↑(Iio ↑⟨i, hi⟩)
k : ι
hjk : ↑j < k
hki : k < i
hk : k ∈ s
⊢ (e₁ ⟨k, hk⟩) (f ⋯ x) ⟨↑j, hjk⟩ = (e₂ ⟨k, hk⟩) (f ⋯ x) ⟨↑j, hjk⟩

Tactic:
ih _ hki

Goal state after:
case refine_2
ι : 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 : ι
lim : IsSuccPrelimit i
ih : ∀ b < i, ∀ (h : b ∈ s), e₁ ⟨b, h⟩ = e₂ ⟨b, h⟩
hi : i ∈ s
x : F ↑⟨i, hi⟩
j : ↑(Iio ↑⟨i, hi⟩)
k : ι
hjk : ↑j < k
hki : k < i
hk : k ∈ s
⊢ (e₂ ⟨k, hk⟩) (f ⋯ x) ⟨↑j, hjk⟩ = (e₂ ⟨k, hk⟩) (f ⋯ x) ⟨↑j, hjk⟩
Module: Mathlib.Order.DirectedInverseSystem

Goal state before:
pp: ι✝ : Type u_1
inst✝³ : Preorder ι✝
F₁ : ι✝ → Type u_2
F₂ : ι✝ → Type u_3
F✝ : ι✝ → Type u_4
X✝ : ι✝ → Type u_5
f✝ : ⦃i j : ι✝⦄ → i ≤ j → F✝ j → F✝ i
i✝ j✝ : ι✝
h✝ : i✝ ≤ j✝
ι : Type u_6
F : ι → Type u_7
X : ι → Type u_8
i : ι
inst✝² : LinearOrder ι
f : ⦃i j : ι⦄ → i ≤ j → F j → F i
inst✝¹ : SuccOrder ι
equivSucc : failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
s t : Set ι
inst✝ : WellFoundedLT ι
hi : IsSuccPrelimit i
e : (j : ↑(Iio i)) → PEquivOn f equivSucc (Iic ↑j)
j k : ι
hj : j ∈ Iio i
hk : k ∈ Iio i
h : k ≤ j
⊢ ∀ (x : F j),
    ((piLTLim hi).symm ⟨fun j ↦ ((e j).restrict ⋯).equiv, ⋯⟩ ⟨k, hk⟩) (f h x) =
      piLTProj h (((piLTLim hi).symm ⟨fun j ↦ ((e j).restrict ⋯).equiv, ⋯⟩ ⟨j, hj⟩) x)

Tactic:
by rw [piLTLim_symm_apply]; exacts [(e _).nat _ _ _, h.trans_lt (hi.mid _).2.1]

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

Goal state before:
pp: R : Type u_1
inst✝⁶ : CommSemiring R
N : Type u_3
P : Type u_4
Q : Type u_5
inst✝⁵ : AddCommMonoid N
inst✝⁴ : AddCommMonoid P
inst✝³ : AddCommMonoid Q
inst✝² : Module R N
inst✝¹ : Module R P
inst✝ : Module R Q
g : N →ₗ[R] P
hg : Function.Surjective ⇑g
⊢ Function.Surjective ⇑(rTensor Q g)

Tactic:
intro z
  induction z with
  | zero => exact ⟨0, map_zero _⟩
  | tmul p q =>
    obtain ⟨n, rfl⟩ := hg p
    exact ⟨n ⊗ₜ[R] q, rfl⟩
  | add x y hx hy =>
    obtain ⟨x, rfl⟩ := hx
    obtain ⟨y, rfl⟩ := hy
    exact ⟨x + y, map_add _ _ _⟩

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

Goal state before:
pp: case tmul
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 : M
y : N
⊢ ∃ S, x ⊗ₜ[R] y = (Multiset.map (fun i ↦ i.1 ⊗ₜ[R] i.2) S).sum

Tactic:
exact ⟨{(x, y)}, by simp⟩

Goal state after:
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
⊢ Injective ⇑(rTensor M f)

Tactic:
refine rTensor_injective_of_fg fun N P Nfg Pfg le ↦ ?_

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 : N.FG
Pfg : P.FG
le : N ≤ comap f P
⊢ Injective ⇑(rTensor M (f.restrict le))
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 : Module.Finite R ↥N
Pfg : Module.Finite R ↥P
le : N ≤ comap f P
this✝ : Small.{max u ?u.66, u_2} ↥P
se : ↥P ≃ₗ[R] Shrink.{max u ?u.66, u_2} ↥P := (Shrink.linearEquiv R ↥P).symm
this : Module.Finite R (Shrink.{max u ?u.66, u_2} ↥P)
⊢ Injective ⇑(rTensor M (f.restrict le))

Tactic:
rw [rTensor_injective_iff_subtype (fun _ _ ↦ (Subtype.ext <| hf <| Subtype.ext_iff.mp ·)) se]

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
this✝ : Small.{max u ?u.66, u_2} ↥P
se : ↥P ≃ₗ[R] Shrink.{max u ?u.66, u_2} ↥P := (Shrink.linearEquiv R ↥P).symm
this : Module.Finite R (Shrink.{max u ?u.66, u_2} ↥P)
⊢ Injective ⇑(rTensor M (↑se ∘ₗ f.restrict le).range.subtype)
Module: Mathlib.Data.Finset.Density

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

Tactic:
mul_div_cancel₀

Goal state after:
case inr
α : Type u_2
inst✝ : Fintype α
s : Finset α
h✝ : Nonempty α
⊢ ↑(#s) = ↑(#s)

case inr.hb
α : Type u_2
inst✝ : Fintype α
s : Finset α
h✝ : Nonempty α
⊢ ↑(Fintype.card α) ≠ 0
Module: Mathlib.Order.Interval.Finset.Gaps

Goal state before:
pp: case inr
α : Type u_1
inst✝ : LinearOrder α
F : Finset (α × α)
k : ℕ
h : #F = k
j : ℕ
a b : α
hFab : ∀ ⦃z : α × α⦄, z ∈ F → a ≤ z.1 ∧ z.1 ≤ z.2 ∧ z.2 ≤ b
this : ∀ j < k + 1, a ≤ (F.intervalGapsWithin h a b ↑j).1
hj : ¬j < k + 1
⊢ a ≤ (F.intervalGapsWithin h a b ↑j).1

Tactic:
grind [cast_val_eq_self]

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

Goal state before:
pp: ι : Type u_1
M : Type u_4
inst✝³ : CommSemiring M
inst✝² : Module ℚ≥0 M
inst✝¹ : IsScalarTower ℚ≥0 M M
inst✝ : SMulCommClass ℚ≥0 M M
s : Finset ι
f : ι → M
n : ℕ
⊢ (𝔼 i ∈ s, f i) ^ n = 𝔼 p ∈ Fintype.piFinset fun x ↦ s, ∏ i, f (p i)

Tactic:
by
  rw [expect, smul_pow, sum_pow', expect, Fintype.card_piFinset_const, inv_pow, Nat.cast_pow]

Goal state after:
Module: Mathlib.Order.Interval.Finset.Gaps

Goal state before:
pp: case inr
α : Type u_1
inst✝ : LinearOrder α
F : Finset (α × α)
k : ℕ
h : #F = k
j : ℕ
a b : α
hFab : ∀ ⦃z : α × α⦄, z ∈ F → a ≤ z.1 ∧ z.1 ≤ z.2 ∧ z.2 ≤ b
this : ∀ j < k + 1, (F.intervalGapsWithin h a b ↑j).2 ≤ b
hj : ¬j < k + 1
⊢ (F.intervalGapsWithin h a b ↑j).2 ≤ b

Tactic:
grind [cast_val_eq_self]

Goal state after:
Module: Mathlib.Algebra.Colimit.DirectLimit

Goal state before:
pp: R : Type u_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✝³ : CommSemiring R
inst✝² : (i : ι) → Semiring (G i)
inst✝¹ : (i : ι) → Algebra R (G i)
inst✝ : ∀ (i j : ι) (h : i ≤ j), AlgHomClass (T h) R (G i) (G j)
r : R
i : ι
x✝ : G i
⊢ ⟦⟨i, r • x✝⟩⟧ = ⟦⟨i, (algebraMap R (G i)) r * x✝⟩⟧

Tactic:
Algebra.smul_def'

Goal state after:
R : Type u_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✝³ : CommSemiring R
inst✝² : (i : ι) → Semiring (G i)
inst✝¹ : (i : ι) → Algebra R (G i)
inst✝ : ∀ (i j : ι) (h : i ≤ j), AlgHomClass (T h) R (G i) (G j)
r : R
i : ι
x✝ : G i
⊢ ⟦⟨i, (algebraMap R (G i)) r * x✝⟩⟧ = ⟦⟨i, (algebraMap R (G i)) r * x✝⟩⟧
Module: Mathlib.Order.Interval.Finset.Gaps

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

Tactic:
grind [cast_val_eq_self]

Goal state after:
Module: Mathlib.Order.Interval.Finset.Gaps

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

Tactic:
grind [cast_val_eq_self]

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

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

Tactic:
← mul_pow,

Goal state after:
case succ
α : Type u_1
inst✝ : CommGroup α
f : ℤ → α
hf : Function.Even f
N : ℕ
ih : ∏ m ∈ Icc (-↑N) ↑N, f m = (∏ m ∈ range (N + 1), f ↑m) ^ 2 / f 0
⊢ ((∏ m ∈ range (N + 1), f ↑m) * f (↑N + 1)) ^ 2 / f 0 = ((∏ x ∈ range (N + 1), f ↑x) * f ↑(N + 1)) ^ 2 / f 0
Module: Mathlib.Algebra.BigOperators.Group.Finset.Powerset

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

Tactic:
rw [prod_eq_pow_card, card_powersetCard]; rintro a ha; rw [(mem_powersetCard.1 ha).2]

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

Goal state before:
pp: n : ℤ
l : List ℤ
h : ∀ x ∈ l, x ≡ 0 [ZMOD n]
⊢ l.sum ≡ 0 [ZMOD n]

Tactic:
by
  simpa using listSum_map_zero h

Goal state after: