harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/Algebra/BigOperators/Finprod.lean
theorem MonoidHom.map_finprod_mem' {f : α → M} (g : M →* N) (h₀ : (s ∩ mulSupport f).Finite) :
    g (∏ᶠ j ∈ s, f j) = ∏ᶠ i ∈ s, g (f i)

Proof state:
α : Type u_1
M : Type u_5
N : Type u_6
inst✝¹ : CommMonoid M
inst✝ : CommMonoid N
s : Set α
f : α → M
g : M →* N
h₀ : (s ∩ mulSupport f).Finite
⊢ ∏ᶠ (i : α), g (∏ᶠ (_ : i ∈ s), f i) = ∏ᶠ (i : α) (_ : i ∈ s), g (f i)

Tactic:
simp only [g.map_finprod_Prop]

Result:
no goals

Proof state:
α : Type u_1
M : Type u_5
N : Type u_6
inst✝¹ : CommMonoid M
inst✝ : CommMonoid N
s : Set α
f : α → M
g : M →* N
h₀ : (s ∩ mulSupport f).Finite
⊢ (mulSupport fun j => ∏ᶠ (_ : j ∈ s), f j).Finite

Tactic:
simpa only [finprod_eq_mulIndicator_apply, mulSupport_mulIndicator]

Result:
no goals

Proof state:
α : Type u_1
M : Type u_5
N : Type u_6
inst✝¹ : CommMonoid M
inst✝ : CommMonoid N
s : Set α
f : α → M
g : M →* N
h₀ : (s ∩ mulSupport f).Finite
⊢ g (∏ᶠ (j : α) (_ : j ∈ s), f j) = ∏ᶠ (i : α) (_ : i ∈ s), g (f i)

Tactic:
rw [g.map_finprod]

Result:
α : Type u_1
M : Type u_5
N : Type u_6
inst✝¹ : CommMonoid M
inst✝ : CommMonoid N
s : Set α
f : α → M
g : M →* N
h₀ : (s ∩ mulSupport f).Finite
⊢ ∏ᶠ (i : α), g (∏ᶠ (_ : i ∈ s), f i) = ∏ᶠ (i : α) (_ : i ∈ s), g (f i)

α : Type u_1
M : Type u_5
N : Type u_6
inst✝¹ : CommMonoid M
inst✝ : CommMonoid N
s : Set α
f : α → M
g : M →* N
h₀ : (s ∩ mulSupport f).Finite
⊢ (mulSupport fun j => ∏ᶠ (_ : j ∈ s), f j).Finite
-- Mathlib/Analysis/MeanInequalitiesPow.lean
lemma rpow_add_rpow_le_add {p : ℝ} {a b : ℝ} (ha : 0 ≤ a) (hb : 0 ≤ b) (hp1 : 1 ≤ p) :
    (a ^ p + b ^ p) ^ (1 / p) ≤ a + b

Proof state:
case intro.intro
p : ℝ
hp1 : 1 ≤ p
a b : ℝ≥0
⊢ (↑a ^ p + ↑b ^ p) ^ (1 / p) ≤ ↑a + ↑b

Tactic:
exact_mod_cast NNReal.rpow_add_rpow_le_add a b hp1

Result:
no goals

Proof state:
case intro
p b : ℝ
hb : 0 ≤ b
hp1 : 1 ≤ p
a : ℝ≥0
⊢ (↑a ^ p + b ^ p) ^ (1 / p) ≤ ↑a + b

Tactic:
lift b to NNReal using hb

Result:
case intro.intro
p : ℝ
hp1 : 1 ≤ p
a b : ℝ≥0
⊢ (↑a ^ p + ↑b ^ p) ^ (1 / p) ≤ ↑a + ↑b

Proof state:
p a b : ℝ
ha : 0 ≤ a
hb : 0 ≤ b
hp1 : 1 ≤ p
⊢ (a ^ p + b ^ p) ^ (1 / p) ≤ a + b

Tactic:
lift a to NNReal using ha

Result:
case intro
p b : ℝ
hb : 0 ≤ b
hp1 : 1 ≤ p
a : ℝ≥0
⊢ (↑a ^ p + b ^ p) ^ (1 / p) ≤ ↑a + b
-- Mathlib/Algebra/QuaternionBasis.lean
theorem j_mul_k : q.j * q.k = (c₂ * c₃) • 1 - c₃ • q.i

Proof state:
R : Type u_1
A : Type u_2
inst✝² : CommRing R
inst✝¹ : Ring A
inst✝ : Algebra R A
c₁ c₂ c₃ : R
q : Basis A c₁ c₂ c₃
⊢ q.j * q.k = (c₂ * c₃) • 1 - c₃ • q.i

Tactic:
rw [← i_mul_j, ← mul_assoc, j_mul_i, sub_mul, smul_mul_assoc, j_mul_j, ← smul_assoc, k_mul_j]

Result:
R : Type u_1
A : Type u_2
inst✝² : CommRing R
inst✝¹ : Ring A
inst✝ : Algebra R A
c₁ c₂ c₃ : R
q : Basis A c₁ c₂ c₃
⊢ (c₂ • c₃) • 1 - c₃ • q.i = (c₂ * c₃) • 1 - c₃ • q.i

Proof state:
R : Type u_1
A : Type u_2
inst✝² : CommRing R
inst✝¹ : Ring A
inst✝ : Algebra R A
c₁ c₂ c₃ : R
q : Basis A c₁ c₂ c₃
⊢ (c₂ • c₃) • 1 - c₃ • q.i = (c₂ * c₃) • 1 - c₃ • q.i

Tactic:
rfl

Result:
no goals
-- Mathlib/Algebra/Homology/HomotopyCategory/HomComplex.lean
@[simp]
protected lemma comp_smul {n₁ n₂ n₁₂ : ℤ} (z₁ : Cochain F G n₁) (k : R) (z₂ : Cochain G K n₂)
    (h : n₁ + n₂ = n₁₂ ) : z₁.comp (k • z₂) h = k • (z₁.comp z₂ h)

Proof state:
case h
C : Type u
inst✝³ : Category.{v, u} C
inst✝² : Preadditive C
R : Type u_1
inst✝¹ : Ring R
inst✝ : Linear R C
F G K : CochainComplex C ℤ
n₁ n₂ n₁₂ : ℤ
z₁ : Cochain F G n₁
k : R
z₂ : Cochain G K n₂
h : n₁ + n₂ = n₁₂
p q : ℤ
hpq : p + n₁₂ = q
⊢ (z₁.comp (k • z₂) h).v p q hpq = (k • z₁.comp z₂ h).v p q hpq

Tactic:
simp only [comp_v _ _ h p _ q rfl (by omega), smul_v, Linear.comp_smul]

Result:
no goals

Proof state:
C : Type u
inst✝³ : Category.{v, u} C
inst✝² : Preadditive C
R : Type u_1
inst✝¹ : Ring R
inst✝ : Linear R C
F G K : CochainComplex C ℤ
n₁ n₂ n₁₂ : ℤ
z₁ : Cochain F G n₁
k : R
z₂ : Cochain G K n₂
h : n₁ + n₂ = n₁₂
p q : ℤ
hpq : p + n₁₂ = q
⊢ p + n₁ + n₂ = q

Tactic:
omega

Result:
no goals

Proof state:
C : Type u
inst✝³ : Category.{v, u} C
inst✝² : Preadditive C
R : Type u_1
inst✝¹ : Ring R
inst✝ : Linear R C
F G K : CochainComplex C ℤ
n₁ n₂ n₁₂ : ℤ
z₁ : Cochain F G n₁
k : R
z₂ : Cochain G K n₂
h : n₁ + n₂ = n₁₂
⊢ z₁.comp (k • z₂) h = k • z₁.comp z₂ h

Tactic:
ext p q hpq

Result:
case h
C : Type u
inst✝³ : Category.{v, u} C
inst✝² : Preadditive C
R : Type u_1
inst✝¹ : Ring R
inst✝ : Linear R C
F G K : CochainComplex C ℤ
n₁ n₂ n₁₂ : ℤ
z₁ : Cochain F G n₁
k : R
z₂ : Cochain G K n₂
h : n₁ + n₂ = n₁₂
p q : ℤ
hpq : p + n₁₂ = q
⊢ (z₁.comp (k • z₂) h).v p q hpq = (k • z₁.comp z₂ h).v p q hpq
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Fin/Fold.lean
theorem foldl_loop_eq (f : α → Fin n → α) (x) : foldl.loop n f x n = x

Proof state:
α : Sort u_1
n : Nat
f : α → Fin n → α
x : α
⊢ foldl.loop n f x n = x

Tactic:
rw [foldl.loop, dif_neg (Nat.lt_irrefl _)]

Result:
no goals
-- Mathlib/Probability/Process/Stopping.lean
theorem condExp_stopping_time_ae_eq_restrict_eq_of_countable_range [SigmaFiniteFiltration μ ℱ]
    (hτ : IsStoppingTime ℱ τ) (h_countable : (Set.range τ).Countable)
    [SigmaFinite (μ.trim (hτ.measurableSpace_le_of_countable_range h_countable))] (i : ι) :
    μ[f|hτ.measurableSpace] =ᵐ[μ.restrict {x | τ x = i}] μ[f|ℱ i]

Proof state:
Ω : Type u_1
ι : Type u_3
m : MeasurableSpace Ω
inst✝⁵ : LinearOrder ι
μ : Measure Ω
ℱ : Filtration ι m
τ : Ω → ι
E : Type u_4
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace ℝ E
inst✝² : CompleteSpace E
f : Ω → E
inst✝¹ : SigmaFiniteFiltration μ ℱ
hτ : IsStoppingTime ℱ τ
h_countable : (Set.range τ).Countable
inst✝ : SigmaFinite (μ.trim ⋯)
i : ι
⊢ μ[f|hτ.measurableSpace] =ᶠ[ae (μ.restrict {x | τ x = i})] μ[f|↑ℱ i]

Tactic:
refine condExp_ae_eq_restrict_of_measurableSpace_eq_on
  (hτ.measurableSpace_le_of_countable_range h_countable) (ℱ.le i)
  (hτ.measurableSet_eq_of_countable_range' h_countable i) fun t => ?_

Result:
Ω : Type u_1
ι : Type u_3
m : MeasurableSpace Ω
inst✝⁵ : LinearOrder ι
μ : Measure Ω
ℱ : Filtration ι m
τ : Ω → ι
E : Type u_4
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace ℝ E
inst✝² : CompleteSpace E
f : Ω → E
inst✝¹ : SigmaFiniteFiltration μ ℱ
hτ : IsStoppingTime ℱ τ
h_countable : (Set.range τ).Countable
inst✝ : SigmaFinite (μ.trim ⋯)
i : ι
t : Set Ω
⊢ MeasurableSet ({x | τ x = i} ∩ t) ↔ MeasurableSet ({x | τ x = i} ∩ t)

Proof state:
Ω : Type u_1
ι : Type u_3
m : MeasurableSpace Ω
inst✝⁵ : LinearOrder ι
μ : Measure Ω
ℱ : Filtration ι m
τ : Ω → ι
E : Type u_4
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace ℝ E
inst✝² : CompleteSpace E
f : Ω → E
inst✝¹ : SigmaFiniteFiltration μ ℱ
hτ : IsStoppingTime ℱ τ
h_countable : (Set.range τ).Countable
inst✝ : SigmaFinite (μ.trim ⋯)
i : ι
t : Set Ω
⊢ MeasurableSet ({x | τ x = i} ∩ t) ↔ MeasurableSet ({x | τ x = i} ∩ t)

Tactic:
rw [Set.inter_comm _ t, IsStoppingTime.measurableSet_inter_eq_iff]

Result:
no goals
-- Mathlib/NumberTheory/Cyclotomic/Rat.lean
theorem discr_prime_pow' [IsCyclotomicExtension {p ^ k} ℚ K] (hζ : IsPrimitiveRoot ζ ↑(p ^ k)) :
    discr ℚ (hζ.subOnePowerBasis ℚ).basis =
      (-1) ^ ((p ^ k : ℕ).totient / 2) * p ^ ((p : ℕ) ^ (k - 1) * ((p - 1) * k - 1))

Proof state:
p : ℕ+
k : ℕ
K : Type u
inst✝² : Field K
ζ : K
hp : Fact (Nat.Prime ↑p)
inst✝¹ : CharZero K
inst✝ : IsCyclotomicExtension {p ^ k} ℚ K
hζ : IsPrimitiveRoot ζ ↑(p ^ k)
⊢ Algebra.discr ℚ ⇑(IsPrimitiveRoot.subOnePowerBasis ℚ hζ).basis =
    (-1) ^ (φ (↑p ^ k) / 2) * ↑↑p ^ (↑p ^ (k - 1) * ((↑p - 1) * k - 1))

Tactic:
rw [← discr_prime_pow hζ (cyclotomic.irreducible_rat (p ^ k).pos)]

Result:
p : ℕ+
k : ℕ
K : Type u
inst✝² : Field K
ζ : K
hp : Fact (Nat.Prime ↑p)
inst✝¹ : CharZero K
inst✝ : IsCyclotomicExtension {p ^ k} ℚ K
hζ : IsPrimitiveRoot ζ ↑(p ^ k)
⊢ Algebra.discr ℚ ⇑(IsPrimitiveRoot.subOnePowerBasis ℚ hζ).basis =
    Algebra.discr ℚ ⇑(IsPrimitiveRoot.powerBasis ℚ hζ).basis

Proof state:
p : ℕ+
k : ℕ
K : Type u
inst✝² : Field K
ζ : K
hp : Fact (Nat.Prime ↑p)
inst✝¹ : CharZero K
inst✝ : IsCyclotomicExtension {p ^ k} ℚ K
hζ : IsPrimitiveRoot ζ ↑(p ^ k)
⊢ Algebra.discr ℚ ⇑(IsPrimitiveRoot.subOnePowerBasis ℚ hζ).basis =
    Algebra.discr ℚ ⇑(IsPrimitiveRoot.powerBasis ℚ hζ).basis

Tactic:
exact hζ.discr_zeta_eq_discr_zeta_sub_one.symm

Result:
no goals
-- Mathlib/Algebra/Order/GroupWithZero/Unbundled.lean
/-- See also `pow_right_strictMono'`. -/
lemma pow_right_strictMono₀ (h : 1 < a) : StrictMono (a ^ ·) :=
  have : 0 < a := zero_le_one.trans_lt h
  strictMono_nat_of_lt_succ fun n => by
    simpa only [one_mul, pow_succ'] using mul_lt_mul h (le_refl (a ^ n)) (pow_pos this _) this.le

Proof state:
M₀ : Type u_1
inst✝⁴ : MonoidWithZero M₀
inst✝³ : PartialOrder M₀
a : M₀
inst✝² : ZeroLEOneClass M₀
inst✝¹ : PosMulStrictMono M₀
inst✝ : MulPosStrictMono M₀
h : 1 < a
this : 0 < a
n : ℕ
⊢ a ^ n < a ^ (n + 1)

Tactic:
simpa only [one_mul, pow_succ'] using mul_lt_mul h (le_refl (a ^ n)) (pow_pos this _) this.le

Result:
no goals
-- Mathlib/Algebra/Polynomial/Taylor.lean
theorem taylor_injective {R} [CommRing R] (r : R) : Function.Injective (taylor r)

Proof state:
R : Type u_2
inst✝ : CommRing R
r : R
⊢ Function.Injective ⇑(taylor r)

Tactic:
intro f g h

Result:
R : Type u_2
inst✝ : CommRing R
r : R
f g : R[X]
h : (taylor r) f = (taylor r) g
⊢ f = g

Proof state:
R : Type u_2
inst✝ : CommRing R
r : R
f g : R[X]
h : (taylor (-r)) ((taylor r) f) = (taylor (-r)) ((taylor r) g)
⊢ f = g

Tactic:
simpa only [taylor_apply, comp_assoc, add_comp, X_comp, C_comp, C_neg, neg_add_cancel_right,
  comp_X] using h

Result:
no goals

Proof state:
R : Type u_2
inst✝ : CommRing R
r : R
f g : R[X]
h : (taylor r) f = (taylor r) g
⊢ f = g

Tactic:
apply_fun taylor (-r) at h

Result:
R : Type u_2
inst✝ : CommRing R
r : R
f g : R[X]
h : (taylor (-r)) ((taylor r) f) = (taylor (-r)) ((taylor r) g)
⊢ f = g
-- Mathlib/Analysis/Calculus/DSlope.lean
theorem continuousAt_dslope_of_ne (h : b ≠ a) : ContinuousAt (dslope f a) b ↔ ContinuousAt f b

Proof state:
𝕜 : Type u_1
E : Type u_2
inst✝² : NontriviallyNormedField 𝕜
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
f : 𝕜 → E
a b : 𝕜
h : b ≠ a
⊢ ContinuousAt (dslope f a) b ↔ ContinuousAt f b

Tactic:
simp only [← continuousWithinAt_univ, continuousWithinAt_dslope_of_ne h]

Result:
no goals
-- Mathlib/Tactic/NormNum/Pow.lean
theorem isRat_zpow_pos {α : Type*} [DivisionRing α] {a : α} {b : ℤ} {nb : ℕ}
    {num : ℤ} {den : ℕ}
    (pb : IsNat b nb) (pe' : IsRat (a^nb) num den) :
    IsRat (a^b) num den

Proof state:
α : Type u_1
inst✝ : DivisionRing α
a : α
b : ℤ
nb : ℕ
num : ℤ
den : ℕ
pb : IsNat b nb
pe' : IsRat (a ^ nb) num den
⊢ IsRat (a ^ b) num den

Tactic:
rwa [pb.out, zpow_natCast]

Result:
no goals
-- Mathlib/Algebra/Category/Grp/Basic.lean
theorem MonoidHom.id_commGrp_comp {G : Type u} [Monoid G] {H : CommGrp.{u}} (f : G →* H) :
    MonoidHom.comp (CommGrp.Hom.hom (𝟙 H)) f = f

Proof state:
G : Type u
inst✝ : Monoid G
H : CommGrp
f : G →* ↑H
⊢ (CommGrp.Hom.hom (𝟙 H)).comp f = f

Tactic:
simp

Result:
no goals
-- Mathlib/CategoryTheory/Monoidal/Mon_.lean
theorem Mon_tensor_mul_one (M N : Mon_ C) :
    (M.X ⊗ N.X) ◁ ((λ_ (𝟙_ C)).inv ≫ (M.one ⊗ N.one)) ≫
        tensorμ M.X N.X M.X N.X ≫ (M.mul ⊗ N.mul) =
      (ρ_ (M.X ⊗ N.X)).hom

Proof state:
C : Type u₁
inst✝² : Category.{v₁, u₁} C
inst✝¹ : MonoidalCategory C
inst✝ : BraidedCategory C
M N : Mon_ C
⊢ (M.X ⊗ N.X) ◁ ((λ_ (𝟙_ C)).inv ≫ (M.one ⊗ N.one)) ≫ tensorμ M.X N.X M.X N.X ≫ (M.mul ⊗ N.mul) = (ρ_ (M.X ⊗ N.X)).hom

Tactic:
simp only [MonoidalCategory.whiskerLeft_comp_assoc]

Result:
C : Type u₁
inst✝² : Category.{v₁, u₁} C
inst✝¹ : MonoidalCategory C
inst✝ : BraidedCategory C
M N : Mon_ C
⊢ (M.X ⊗ N.X) ◁ (λ_ (𝟙_ C)).inv ≫ (M.X ⊗ N.X) ◁ (M.one ⊗ N.one) ≫ tensorμ M.X N.X M.X N.X ≫ (M.mul ⊗ N.mul) =
    (ρ_ (M.X ⊗ N.X)).hom

Proof state:
C : Type u₁
inst✝² : Category.{v₁, u₁} C
inst✝¹ : MonoidalCategory C
inst✝ : BraidedCategory C
M N : Mon_ C
⊢ (M.X ⊗ N.X) ◁ (λ_ (𝟙_ C)).inv ≫ (M.X ⊗ N.X) ◁ (M.one ⊗ N.one) ≫ tensorμ M.X N.X M.X N.X ≫ (M.mul ⊗ N.mul) =
    (ρ_ (M.X ⊗ N.X)).hom

Tactic:
slice_lhs 2 3 => rw [tensorμ_natural_right]

Result:
C : Type u₁
inst✝² : Category.{v₁, u₁} C
inst✝¹ : MonoidalCategory C
inst✝ : BraidedCategory C
M N : Mon_ C
⊢ (M.X ⊗ N.X) ◁ (λ_ (𝟙_ C)).inv ≫ (tensorμ M.X N.X (𝟙_ C) (𝟙_ C) ≫ (M.X ◁ M.one ⊗ N.X ◁ N.one)) ≫ (M.mul ⊗ N.mul) =
    (ρ_ (M.X ⊗ N.X)).hom

Proof state:
C : Type u₁
inst✝² : Category.{v₁, u₁} C
inst✝¹ : MonoidalCategory C
inst✝ : BraidedCategory C
M N : Mon_ C
⊢ (M.X ⊗ N.X) ◁ (λ_ (𝟙_ C)).inv ≫ (tensorμ M.X N.X (𝟙_ C) (𝟙_ C) ≫ (M.X ◁ M.one ⊗ N.X ◁ N.one)) ≫ (M.mul ⊗ N.mul) =
    (ρ_ (M.X ⊗ N.X)).hom

Tactic:
slice_lhs 3 4 => rw [← tensor_comp, mul_one M, mul_one N]

Result:
C : Type u₁
inst✝² : Category.{v₁, u₁} C
inst✝¹ : MonoidalCategory C
inst✝ : BraidedCategory C
M N : Mon_ C
⊢ (M.X ⊗ N.X) ◁ (λ_ (𝟙_ C)).inv ≫ tensorμ M.X N.X (𝟙_ C) (𝟙_ C) ≫ ((ρ_ M.X).hom ⊗ (ρ_ N.X).hom) = (ρ_ (M.X ⊗ N.X)).hom

Proof state:
C : Type u₁
inst✝² : Category.{v₁, u₁} C
inst✝¹ : MonoidalCategory C
inst✝ : BraidedCategory C
M N : Mon_ C
⊢ (ρ_ (M.X ⊗ N.X)).hom = (M.X ⊗ N.X) ◁ (λ_ (𝟙_ C)).inv ≫ tensorμ M.X N.X (𝟙_ C) (𝟙_ C) ≫ ((ρ_ M.X).hom ⊗ (ρ_ N.X).hom)

Tactic:
exact tensor_right_unitality M.X N.X

Result:
no goals

Proof state:
C : Type u₁
inst✝² : Category.{v₁, u₁} C
inst✝¹ : MonoidalCategory C
inst✝ : BraidedCategory C
M N : Mon_ C
⊢ (M.X ⊗ N.X) ◁ (λ_ (𝟙_ C)).inv ≫ tensorμ M.X N.X (𝟙_ C) (𝟙_ C) ≫ ((ρ_ M.X).hom ⊗ (ρ_ N.X).hom) = (ρ_ (M.X ⊗ N.X)).hom

Tactic:
symm

Result:
C : Type u₁
inst✝² : Category.{v₁, u₁} C
inst✝¹ : MonoidalCategory C
inst✝ : BraidedCategory C
M N : Mon_ C
⊢ (ρ_ (M.X ⊗ N.X)).hom = (M.X ⊗ N.X) ◁ (λ_ (𝟙_ C)).inv ≫ tensorμ M.X N.X (𝟙_ C) (𝟙_ C) ≫ ((ρ_ M.X).hom ⊗ (ρ_ N.X).hom)
-- Mathlib/Analysis/Analytic/IsolatedZeros.lean
theorem eventually_eq_or_eventually_ne (hf : AnalyticAt 𝕜 f z₀) (hg : AnalyticAt 𝕜 g z₀) :
    (∀ᶠ z in 𝓝 z₀, f z = g z) ∨ ∀ᶠ z in 𝓝[≠] z₀, f z ≠ g z

Proof state:
𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
f g : 𝕜 → E
z₀ : 𝕜
hf : AnalyticAt 𝕜 f z₀
hg : AnalyticAt 𝕜 g z₀
⊢ (∀ᶠ (z : 𝕜) in 𝓝 z₀, f z = g z) ∨ ∀ᶠ (z : 𝕜) in 𝓝[≠] z₀, f z ≠ g z

Tactic:
simpa [sub_eq_zero] using (hf.sub hg).eventually_eq_zero_or_eventually_ne_zero

Result:
no goals
-- Mathlib/Probability/Distributions/Uniform.lean
theorem mem_support_uniformOfFinset_iff (a : α) : a ∈ (uniformOfFinset s hs).support ↔ a ∈ s

Proof state:
α : Type u_1
s : Finset α
hs : s.Nonempty
a : α
⊢ a ∈ (uniformOfFinset s hs).support ↔ a ∈ s

Tactic:
simp

Result:
no goals
-- Mathlib/RingTheory/Jacobson/Radical.lean
theorem jacobson_quotient_jacobson : jacobson (R ⧸ jacobson R) = ⊥ :=
  (jacobson_quotient_of_le le_rfl).trans <| SetLike.ext' <| by
    apply SetLike.ext'_iff.mp (jacobson R).mkQ_map_self

Proof state:
R : Type u_1
inst✝ : Ring R
⊢ ↑(Submodule.map (Ideal.Quotient.mk (jacobson R)).toSemilinearMap (jacobson R)) = ↑⊥

Tactic:
apply SetLike.ext'_iff.mp (jacobson R).mkQ_map_self

Result:
no goals
-- Mathlib/Topology/Order/LowerUpperTopology.lean
protected lemma _root_.sInfHom.continuous (f : sInfHom α β) : Continuous f

Proof state:
case h.e'_3
α : Type u_1
β : Type u_2
inst✝⁵ : CompleteLattice α
inst✝⁴ : CompleteLattice β
inst✝³ : TopologicalSpace α
inst✝² : IsLower α
inst✝¹ : TopologicalSpace β
inst✝ : IsLower β
f : sInfHom α β
b : β
a : α
ha : a ∈ Ici (sInf (⇑f ⁻¹' Ici b))
⊢ b ≤ sInf (⇑f '' (⇑f ⁻¹' Ici b))

Tactic:
simp

Result:
no goals

Proof state:
α : Type u_1
β : Type u_2
inst✝⁵ : CompleteLattice α
inst✝⁴ : CompleteLattice β
inst✝³ : TopologicalSpace α
inst✝² : IsLower α
inst✝¹ : TopologicalSpace β
inst✝ : IsLower β
f : sInfHom α β
b : β
⊢ IsClosed (⇑f ⁻¹' Ici b)

Tactic:
convert isClosed_Ici (a := sInf <| f ⁻¹' Ici b)

Result:
case h.e'_3
α : Type u_1
β : Type u_2
inst✝⁵ : CompleteLattice α
inst✝⁴ : CompleteLattice β
inst✝³ : TopologicalSpace α
inst✝² : IsLower α
inst✝¹ : TopologicalSpace β
inst✝ : IsLower β
f : sInfHom α β
b : β
⊢ ⇑f ⁻¹' Ici b = Ici (sInf (⇑f ⁻¹' Ici b))

Proof state:
α : Type u_1
β : Type u_2
inst✝⁵ : CompleteLattice α
inst✝⁴ : CompleteLattice β
inst✝³ : TopologicalSpace α
inst✝² : IsLower α
inst✝¹ : TopologicalSpace β
inst✝ : IsLower β
f : sInfHom α β
⊢ Continuous ⇑f

Tactic:
refine IsLower.continuous_iff_Ici.2 fun b => ?_

Result:
α : Type u_1
β : Type u_2
inst✝⁵ : CompleteLattice α
inst✝⁴ : CompleteLattice β
inst✝³ : TopologicalSpace α
inst✝² : IsLower α
inst✝¹ : TopologicalSpace β
inst✝ : IsLower β
f : sInfHom α β
b : β
⊢ IsClosed (⇑f ⁻¹' Ici b)

Proof state:
case h.e'_3
α : Type u_1
β : Type u_2
inst✝⁵ : CompleteLattice α
inst✝⁴ : CompleteLattice β
inst✝³ : TopologicalSpace α
inst✝² : IsLower α
inst✝¹ : TopologicalSpace β
inst✝ : IsLower β
f : sInfHom α β
b : β
a : α
ha : a ∈ Ici (sInf (⇑f ⁻¹' Ici b))
⊢ b ≤ ↑f (sInf (⇑f ⁻¹' Ici b))

Tactic:
refine LE.le.trans ?_ (map_sInf f _).ge

Result:
case h.e'_3
α : Type u_1
β : Type u_2
inst✝⁵ : CompleteLattice α
inst✝⁴ : CompleteLattice β
inst✝³ : TopologicalSpace α
inst✝² : IsLower α
inst✝¹ : TopologicalSpace β
inst✝ : IsLower β
f : sInfHom α β
b : β
a : α
ha : a ∈ Ici (sInf (⇑f ⁻¹' Ici b))
⊢ b ≤ sInf (⇑f '' (⇑f ⁻¹' Ici b))

Proof state:
case h.e'_3
α : Type u_1
β : Type u_2
inst✝⁵ : CompleteLattice α
inst✝⁴ : CompleteLattice β
inst✝³ : TopologicalSpace α
inst✝² : IsLower α
inst✝¹ : TopologicalSpace β
inst✝ : IsLower β
f : sInfHom α β
b : β
⊢ ⇑f ⁻¹' Ici b = Ici (sInf (⇑f ⁻¹' Ici b))

Tactic:
refine Subset.antisymm (fun a => sInf_le) fun a ha => le_trans ?_ <|
  OrderHomClass.mono (f : α →o β) ha

Result:
case h.e'_3
α : Type u_1
β : Type u_2
inst✝⁵ : CompleteLattice α
inst✝⁴ : CompleteLattice β
inst✝³ : TopologicalSpace α
inst✝² : IsLower α
inst✝¹ : TopologicalSpace β
inst✝ : IsLower β
f : sInfHom α β
b : β
a : α
ha : a ∈ Ici (sInf (⇑f ⁻¹' Ici b))
⊢ b ≤ ↑f (sInf (⇑f ⁻¹' Ici b))
-- Mathlib/CategoryTheory/Limits/EpiMono.lean
lemma epi_iff_isPushout : Epi f ↔ IsPushout f f (𝟙 Y) (𝟙 Y)

Proof state:
case mpr
C : Type u_1
inst✝ : Category.{u_2, u_1} C
X Y : C
f : X ⟶ Y
⊢ IsPushout f f (𝟙 Y) (𝟙 Y) → Epi f

Tactic:
intro hf

Result:
case mpr
C : Type u_1
inst✝ : Category.{u_2, u_1} C
X Y : C
f : X ⟶ Y
hf : IsPushout f f (𝟙 Y) (𝟙 Y)
⊢ Epi f

Proof state:
C : Type u_1
inst✝ : Category.{u_2, u_1} C
X Y : C
f : X ⟶ Y
⊢ Epi f ↔ IsPushout f f (𝟙 Y) (𝟙 Y)

Tactic:
constructor

Result:
case mp
C : Type u_1
inst✝ : Category.{u_2, u_1} C
X Y : C
f : X ⟶ Y
⊢ Epi f → IsPushout f f (𝟙 Y) (𝟙 Y)

case mpr
C : Type u_1
inst✝ : Category.{u_2, u_1} C
X Y : C
f : X ⟶ Y
⊢ IsPushout f f (𝟙 Y) (𝟙 Y) → Epi f

Proof state:
case mpr
C : Type u_1
inst✝ : Category.{u_2, u_1} C
X Y : C
f : X ⟶ Y
hf : IsPushout f f (𝟙 Y) (𝟙 Y)
⊢ Epi f

Tactic:
exact (epi_iff_inl_eq_inr hf.isColimit).2 rfl

Result:
no goals

Proof state:
case mp
C : Type u_1
inst✝ : Category.{u_2, u_1} C
X Y : C
f : X ⟶ Y
⊢ Epi f → IsPushout f f (𝟙 Y) (𝟙 Y)

Tactic:
intro

Result:
case mp
C : Type u_1
inst✝ : Category.{u_2, u_1} C
X Y : C
f : X ⟶ Y
a✝ : Epi f
⊢ IsPushout f f (𝟙 Y) (𝟙 Y)

Proof state:
case mp
C : Type u_1
inst✝ : Category.{u_2, u_1} C
X Y : C
f : X ⟶ Y
a✝ : Epi f
⊢ IsPushout f f (𝟙 Y) (𝟙 Y)

Tactic:
exact IsPushout.of_isColimit (PushoutCocone.isColimitMkIdId f)

Result:
no goals
-- Mathlib/AlgebraicGeometry/EllipticCurve/Jacobian.lean
lemma addY_smul (P Q : Fin 3 → R) (u v : R) :
    W'.addY (u • P) (v • Q) = ((u * v) ^ 2) ^ 3 * W'.addY P Q

Proof state:
R : Type r
inst✝ : CommRing R
W' : Jacobian R
P Q : Fin 3 → R
u v : R
⊢ -(((u * v) ^ 2) ^ 3 * W'.negAddY P Q) - W'.a₁ * (((u * v) ^ 2) ^ 2 * W'.addX P Q) * ((u * v) ^ 2 * addZ P Q) -
      W'.a₃ * ((u * v) ^ 2 * addZ P Q) ^ 3 =
    ((u * v) ^ 2) ^ 3 * (-W'.negAddY P Q - W'.a₁ * W'.addX P Q * addZ P Q - W'.a₃ * addZ P Q ^ 3)

Tactic:
ring1

Result:
no goals

Proof state:
R : Type r
inst✝ : CommRing R
W' : Jacobian R
P Q : Fin 3 → R
u v : R
⊢ W'.addY (u • P) (v • Q) = ((u * v) ^ 2) ^ 3 * W'.addY P Q

Tactic:
simp only [addY, negY_eq, negAddY_smul, addX_smul, addZ_smul]

Result:
R : Type r
inst✝ : CommRing R
W' : Jacobian R
P Q : Fin 3 → R
u v : R
⊢ -(((u * v) ^ 2) ^ 3 * W'.negAddY P Q) - W'.a₁ * (((u * v) ^ 2) ^ 2 * W'.addX P Q) * ((u * v) ^ 2 * addZ P Q) -
      W'.a₃ * ((u * v) ^ 2 * addZ P Q) ^ 3 =
    ((u * v) ^ 2) ^ 3 * (-W'.negAddY P Q - W'.a₁ * W'.addX P Q * addZ P Q - W'.a₃ * addZ P Q ^ 3)
-- Mathlib/Algebra/BigOperators/Finprod.lean
theorem finprod_eq_prod_plift_of_mulSupport_toFinset_subset {f : α → M}
    (hf : (mulSupport (f ∘ PLift.down)).Finite) {s : Finset (PLift α)} (hs : hf.toFinset ⊆ s) :
    ∏ᶠ i, f i = ∏ i ∈ s, f i.down

Proof state:
M : Type u_2
α : Sort u_4
inst✝ : CommMonoid M
f : α → M
hf : (mulSupport (f ∘ PLift.down)).Finite
s : Finset (PLift α)
hs : hf.toFinset ⊆ s
⊢ ∏ᶠ (i : α), f i = ∏ i ∈ s, f i.down

Tactic:
rw [finprod, dif_pos]

Result:
M : Type u_2
α : Sort u_4
inst✝ : CommMonoid M
f : α → M
hf : (mulSupport (f ∘ PLift.down)).Finite
s : Finset (PLift α)
hs : hf.toFinset ⊆ s
⊢ ∏ i ∈ Finite.toFinset ?hc, f i.down = ∏ i ∈ s, f i.down

case hc
M : Type u_2
α : Sort u_4
inst✝ : CommMonoid M
f : α → M
hf : (mulSupport (f ∘ PLift.down)).Finite
s : Finset (PLift α)
hs : hf.toFinset ⊆ s
⊢ (mulSupport ((fun i => f i) ∘ PLift.down)).Finite

Proof state:
M : Type u_2
α : Sort u_4
inst✝ : CommMonoid M
f : α → M
hf : (mulSupport (f ∘ PLift.down)).Finite
s : Finset (PLift α)
hs : hf.toFinset ⊆ s
⊢ ∏ i ∈ Finite.toFinset ?hc, f i.down = ∏ i ∈ s, f i.down

case hc
M : Type u_2
α : Sort u_4
inst✝ : CommMonoid M
f : α → M
hf : (mulSupport (f ∘ PLift.down)).Finite
s : Finset (PLift α)
hs : hf.toFinset ⊆ s
⊢ (mulSupport ((fun i => f i) ∘ PLift.down)).Finite

Tactic:
refine Finset.prod_subset hs fun x _ hxf => ?_

Result:
M : Type u_2
α : Sort u_4
inst✝ : CommMonoid M
f : α → M
hf : (mulSupport (f ∘ PLift.down)).Finite
s : Finset (PLift α)
hs : hf.toFinset ⊆ s
x : PLift α
x✝ : x ∈ s
hxf : x ∉ hf.toFinset
⊢ f x.down = 1

Proof state:
M : Type u_2
α : Sort u_4
inst✝ : CommMonoid M
f : α → M
hf : (mulSupport (f ∘ PLift.down)).Finite
s : Finset (PLift α)
hs : hf.toFinset ⊆ s
x : PLift α
x✝ : x ∈ s
hxf : x ∉ hf.toFinset
⊢ f x.down = 1

Tactic:
rwa [hf.mem_toFinset, nmem_mulSupport] at hxf

Result:
no goals
-- Mathlib/Analysis/BoundedVariation.lean
theorem ae_differentiableWithinAt_of_mem_real {f : ℝ → ℝ} {s : Set ℝ}
    (h : LocallyBoundedVariationOn f s) : ∀ᵐ x, x ∈ s → DifferentiableWithinAt ℝ f s x

Proof state:
case intro.intro.intro.intro
s : Set ℝ
p q : ℝ → ℝ
hp : MonotoneOn p s
hq : MonotoneOn q s
h : LocallyBoundedVariationOn (p - q) s
⊢ ∀ᵐ (x : ℝ), x ∈ s → DifferentiableWithinAt ℝ (p - q) s x

Tactic:
filter_upwards [hp.ae_differentiableWithinAt_of_mem, hq.ae_differentiableWithinAt_of_mem] with
  x hxp hxq xs

Result:
case h
s : Set ℝ
p q : ℝ → ℝ
hp : MonotoneOn p s
hq : MonotoneOn q s
h : LocallyBoundedVariationOn (p - q) s
x : ℝ
hxp : x ∈ s → DifferentiableWithinAt ℝ p s x
hxq : x ∈ s → DifferentiableWithinAt ℝ q s x
xs : x ∈ s
⊢ DifferentiableWithinAt ℝ (p - q) s x

Proof state:
f : ℝ → ℝ
s : Set ℝ
h : LocallyBoundedVariationOn f s
⊢ ∀ᵐ (x : ℝ), x ∈ s → DifferentiableWithinAt ℝ f s x

Tactic:
obtain ⟨p, q, hp, hq, rfl⟩ : ∃ p q, MonotoneOn p s ∧ MonotoneOn q s ∧ f = p - q :=
  h.exists_monotoneOn_sub_monotoneOn

Result:
case intro.intro.intro.intro
s : Set ℝ
p q : ℝ → ℝ
hp : MonotoneOn p s
hq : MonotoneOn q s
h : LocallyBoundedVariationOn (p - q) s
⊢ ∀ᵐ (x : ℝ), x ∈ s → DifferentiableWithinAt ℝ (p - q) s x

Proof state:
case h
s : Set ℝ
p q : ℝ → ℝ
hp : MonotoneOn p s
hq : MonotoneOn q s
h : LocallyBoundedVariationOn (p - q) s
x : ℝ
hxp : x ∈ s → DifferentiableWithinAt ℝ p s x
hxq : x ∈ s → DifferentiableWithinAt ℝ q s x
xs : x ∈ s
⊢ DifferentiableWithinAt ℝ (p - q) s x

Tactic:
exact (hxp xs).sub (hxq xs)

Result:
no goals
-- Mathlib/Data/Complex/Trigonometric.lean
theorem cos_neg : cos (-x) = cos x

Proof state:
x : ℂ
⊢ cos (-x) = cos x

Tactic:
simp [cos, sub_eq_add_neg, exp_neg, add_comm]

Result:
no goals