harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/.lake/packages/batteries/Batteries/Data/String/Lemmas.lean
theorem extract (h₁ : ValidFor l (m ++ r) it₁) (h₂ : ValidFor (m.reverse ++ l) r it₂) :
    it₁.extract it₂ = ⟨m⟩

Proof state:
case refl.refl
l m r : List Char
h₁ : ValidFor l (m ++ r) { s := { data := l.reverseAux (m ++ r) }, i := { byteIdx := utf8Len l } }
h₂ :
  ValidFor (m.reverse ++ l) r
    { s := { data := (m.reverse ++ l).reverseAux r }, i := { byteIdx := utf8Len (m.reverse ++ l) } }
⊢ { data := l.reverse ++ (m ++ r) }.extract { byteIdx := utf8Len l } { byteIdx := utf8Len m + utf8Len l } =
    { data := m }

Tactic:
simpa [Nat.add_comm] using extract_of_valid l.reverse m r

Result:
no goals

Proof state:
l m r : List Char
it₁ it₂ : Iterator
h₁ : ValidFor l (m ++ r) it₁
h₂ : ValidFor (m.reverse ++ l) r it₂
⊢ it₁.extract it₂ = { data := m }

Tactic:
cases h₁.out

Result:
case refl
l m r : List Char
it₂ : Iterator
h₂ : ValidFor (m.reverse ++ l) r it₂
h₁ : ValidFor l (m ++ r) { s := { data := l.reverseAux (m ++ r) }, i := { byteIdx := utf8Len l } }
⊢ { s := { data := l.reverseAux (m ++ r) }, i := { byteIdx := utf8Len l } }.extract it₂ = { data := m }

Proof state:
case refl.refl
l m r : List Char
h₁ : ValidFor l (m ++ r) { s := { data := l.reverseAux (m ++ r) }, i := { byteIdx := utf8Len l } }
h₂ :
  ValidFor (m.reverse ++ l) r
    { s := { data := (m.reverse ++ l).reverseAux r }, i := { byteIdx := utf8Len (m.reverse ++ l) } }
⊢ { s := { data := l.reverseAux (m ++ r) }, i := { byteIdx := utf8Len l } }.extract
      { s := { data := (m.reverse ++ l).reverseAux r }, i := { byteIdx := utf8Len (m.reverse ++ l) } } =
    { data := m }

Tactic:
simp only [Iterator.extract, List.reverseAux_eq, List.reverse_append, List.reverse_reverse,
  List.append_assoc, ne_eq, not_true_eq_false, decide_false, utf8Len_append, utf8Len_reverse,
  gt_iff_lt, pos_lt_eq, Nat.not_lt.2 (Nat.le_add_left ..), Bool.or_self, Bool.false_eq_true,
  ↓reduceIte]

Result:
case refl.refl
l m r : List Char
h₁ : ValidFor l (m ++ r) { s := { data := l.reverseAux (m ++ r) }, i := { byteIdx := utf8Len l } }
h₂ :
  ValidFor (m.reverse ++ l) r
    { s := { data := (m.reverse ++ l).reverseAux r }, i := { byteIdx := utf8Len (m.reverse ++ l) } }
⊢ { data := l.reverse ++ (m ++ r) }.extract { byteIdx := utf8Len l } { byteIdx := utf8Len m + utf8Len l } =
    { data := m }

Proof state:
case refl
l m r : List Char
it₂ : Iterator
h₂ : ValidFor (m.reverse ++ l) r it₂
h₁ : ValidFor l (m ++ r) { s := { data := l.reverseAux (m ++ r) }, i := { byteIdx := utf8Len l } }
⊢ { s := { data := l.reverseAux (m ++ r) }, i := { byteIdx := utf8Len l } }.extract it₂ = { data := m }

Tactic:
cases h₂.out

Result:
case refl.refl
l m r : List Char
h₁ : ValidFor l (m ++ r) { s := { data := l.reverseAux (m ++ r) }, i := { byteIdx := utf8Len l } }
h₂ :
  ValidFor (m.reverse ++ l) r
    { s := { data := (m.reverse ++ l).reverseAux r }, i := { byteIdx := utf8Len (m.reverse ++ l) } }
⊢ { s := { data := l.reverseAux (m ++ r) }, i := { byteIdx := utf8Len l } }.extract
      { s := { data := (m.reverse ++ l).reverseAux r }, i := { byteIdx := utf8Len (m.reverse ++ l) } } =
    { data := m }
-- Mathlib/AlgebraicTopology/DoldKan/Homotopies.lean
theorem hσ'_eq {q n a m : ℕ} (ha : n = a + q) (hnm : c.Rel m n) :
    (hσ' q n m hnm : X _⦋n⦌ ⟶ X _⦋m⦌) =
      ((-1 : ℤ) ^ a • X.σ ⟨a, Nat.lt_succ_iff.mpr (Nat.le.intro (Eq.symm ha))⟩) ≫
        eqToHom (by congr)

Proof state:
C : Type u_1
inst✝¹ : Category.{?u.6488, u_1} C
inst✝ : Preadditive C
X : SimplicialObject C
q n a m : ℕ
ha : n = a + q
hnm : c.Rel m n
⊢ X _⦋n + 1⦌ = K[X].X m

Tactic:
congr

Result:
no goals

Proof state:
case pos
C : Type u_1
inst✝¹ : Category.{u_2, u_1} C
inst✝ : Preadditive C
X : SimplicialObject C
q n a m : ℕ
ha : n = a + q
hnm : c.Rel m n
h✝ : n < q
⊢ 0 ≫ eqToHom ⋯ = ((-1) ^ a • X.σ ⟨a, ⋯⟩) ≫ eqToHom ⋯

Tactic:
omega

Result:
no goals

Proof state:
case neg
C : Type u_1
inst✝¹ : Category.{u_2, u_1} C
inst✝ : Preadditive C
X : SimplicialObject C
q n a m : ℕ
ha : n = a + q
hnm : c.Rel m n
h✝ : ¬n < q
⊢ ((-1) ^ (n - q) • X.σ ⟨n - q, ⋯⟩) ≫ eqToHom ⋯ = ((-1) ^ a • X.σ ⟨a, ⋯⟩) ≫ eqToHom ⋯

Tactic:
have h' := tsub_eq_of_eq_add ha

Result:
case neg
C : Type u_1
inst✝¹ : Category.{u_2, u_1} C
inst✝ : Preadditive C
X : SimplicialObject C
q n a m : ℕ
ha : n = a + q
hnm : c.Rel m n
h✝ : ¬n < q
h' : n - q = a
⊢ ((-1) ^ (n - q) • X.σ ⟨n - q, ⋯⟩) ≫ eqToHom ⋯ = ((-1) ^ a • X.σ ⟨a, ⋯⟩) ≫ eqToHom ⋯

Proof state:
C : Type u_1
inst✝¹ : Category.{u_2, u_1} C
inst✝ : Preadditive C
X : SimplicialObject C
q n a m : ℕ
ha : n = a + q
hnm : c.Rel m n
⊢ (if n < q then 0 else (-1) ^ (n - q) • X.σ ⟨n - q, ⋯⟩) ≫ eqToHom ⋯ = ((-1) ^ a • X.σ ⟨a, ⋯⟩) ≫ eqToHom ⋯

Tactic:
split_ifs

Result:
case pos
C : Type u_1
inst✝¹ : Category.{u_2, u_1} C
inst✝ : Preadditive C
X : SimplicialObject C
q n a m : ℕ
ha : n = a + q
hnm : c.Rel m n
h✝ : n < q
⊢ 0 ≫ eqToHom ⋯ = ((-1) ^ a • X.σ ⟨a, ⋯⟩) ≫ eqToHom ⋯

case neg
C : Type u_1
inst✝¹ : Category.{u_2, u_1} C
inst✝ : Preadditive C
X : SimplicialObject C
q n a m : ℕ
ha : n = a + q
hnm : c.Rel m n
h✝ : ¬n < q
⊢ ((-1) ^ (n - q) • X.σ ⟨n - q, ⋯⟩) ≫ eqToHom ⋯ = ((-1) ^ a • X.σ ⟨a, ⋯⟩) ≫ eqToHom ⋯

Proof state:
case neg
C : Type u_1
inst✝¹ : Category.{u_2, u_1} C
inst✝ : Preadditive C
X : SimplicialObject C
q n a m : ℕ
ha : n = a + q
hnm : c.Rel m n
h✝ : ¬n < q
h' : n - q = a
⊢ ((-1) ^ (n - q) • X.σ ⟨n - q, ⋯⟩) ≫ eqToHom ⋯ = ((-1) ^ a • X.σ ⟨a, ⋯⟩) ≫ eqToHom ⋯

Tactic:
congr

Result:
no goals

Proof state:
C : Type u_1
inst✝¹ : Category.{u_2, u_1} C
inst✝ : Preadditive C
X : SimplicialObject C
q n a m : ℕ
ha : n = a + q
hnm : c.Rel m n
⊢ hσ' q n m hnm = ((-1) ^ a • X.σ ⟨a, ⋯⟩) ≫ eqToHom ⋯

Tactic:
simp only [hσ', hσ]

Result:
C : Type u_1
inst✝¹ : Category.{u_2, u_1} C
inst✝ : Preadditive C
X : SimplicialObject C
q n a m : ℕ
ha : n = a + q
hnm : c.Rel m n
⊢ (if n < q then 0 else (-1) ^ (n - q) • X.σ ⟨n - q, ⋯⟩) ≫ eqToHom ⋯ = ((-1) ^ a • X.σ ⟨a, ⋯⟩) ≫ eqToHom ⋯
-- Mathlib/ModelTheory/Equivalence.lean
theorem trans {φ ψ θ : L.BoundedFormula α n}
    (h1 : φ ⇔[T] ψ) (h2 : ψ ⇔[T] θ) :
    φ ⇔[T] θ := fun M v xs => by
  have h1' := h1 M v xs
  have h2' := h2 M v xs
  rw [BoundedFormula.realize_iff] at *
  exact ⟨h2'.1 ∘ h1'.1, h1'.2 ∘ h2'.2⟩

Proof state:
L : Language
T : L.Theory
α : Type w
n : ℕ
φ ψ θ : L.BoundedFormula α n
h1 : φ ⇔[T] ψ
h2 : ψ ⇔[T] θ
M : T.ModelType
v : α → ↑M
xs : Fin n → ↑M
h1' : (φ ⇔ ψ).Realize v xs
h2' : (ψ ⇔ θ).Realize v xs
⊢ (φ ⇔ θ).Realize v xs

Tactic:
rw [BoundedFormula.realize_iff] at *

Result:
L : Language
T : L.Theory
α : Type w
n : ℕ
φ ψ θ : L.BoundedFormula α n
h1 : φ ⇔[T] ψ
h2 : ψ ⇔[T] θ
M : T.ModelType
v : α → ↑M
xs : Fin n → ↑M
h1' : φ.Realize v xs ↔ ψ.Realize v xs
h2' : ψ.Realize v xs ↔ θ.Realize v xs
⊢ φ.Realize v xs ↔ θ.Realize v xs

Proof state:
L : Language
T : L.Theory
α : Type w
n : ℕ
φ ψ θ : L.BoundedFormula α n
h1 : φ ⇔[T] ψ
h2 : ψ ⇔[T] θ
M : T.ModelType
v : α → ↑M
xs : Fin n → ↑M
⊢ (φ ⇔ θ).Realize v xs

Tactic:
have h1' := h1 M v xs

Result:
L : Language
T : L.Theory
α : Type w
n : ℕ
φ ψ θ : L.BoundedFormula α n
h1 : φ ⇔[T] ψ
h2 : ψ ⇔[T] θ
M : T.ModelType
v : α → ↑M
xs : Fin n → ↑M
h1' : (φ ⇔ ψ).Realize v xs
⊢ (φ ⇔ θ).Realize v xs

Proof state:
L : Language
T : L.Theory
α : Type w
n : ℕ
φ ψ θ : L.BoundedFormula α n
h1 : φ ⇔[T] ψ
h2 : ψ ⇔[T] θ
M : T.ModelType
v : α → ↑M
xs : Fin n → ↑M
h1' : φ.Realize v xs ↔ ψ.Realize v xs
h2' : ψ.Realize v xs ↔ θ.Realize v xs
⊢ φ.Realize v xs ↔ θ.Realize v xs

Tactic:
exact ⟨h2'.1 ∘ h1'.1, h1'.2 ∘ h2'.2⟩

Result:
no goals

Proof state:
L : Language
T : L.Theory
α : Type w
n : ℕ
φ ψ θ : L.BoundedFormula α n
h1 : φ ⇔[T] ψ
h2 : ψ ⇔[T] θ
M : T.ModelType
v : α → ↑M
xs : Fin n → ↑M
h1' : (φ ⇔ ψ).Realize v xs
⊢ (φ ⇔ θ).Realize v xs

Tactic:
have h2' := h2 M v xs

Result:
L : Language
T : L.Theory
α : Type w
n : ℕ
φ ψ θ : L.BoundedFormula α n
h1 : φ ⇔[T] ψ
h2 : ψ ⇔[T] θ
M : T.ModelType
v : α → ↑M
xs : Fin n → ↑M
h1' : (φ ⇔ ψ).Realize v xs
h2' : (ψ ⇔ θ).Realize v xs
⊢ (φ ⇔ θ).Realize v xs
-- Mathlib/RingTheory/Polynomial/Hermite/Basic.lean
theorem coeff_hermite (n k : ℕ) :
    coeff (hermite n) k =
      if Even (n + k) then (-1 : ℤ) ^ ((n - k) / 2) * (n - k - 1)‼ * Nat.choose n k else 0

Proof state:
case pos
n k : ℕ
h : Even (n + k)
⊢ (hermite n).coeff k = (-1) ^ ((n - k) / 2) * ↑(n - k - 1)‼ * ↑(n.choose k)

Tactic:
exact coeff_hermite_of_even_add h

Result:
no goals

Proof state:
case neg
n k : ℕ
h : ¬Even (n + k)
⊢ (hermite n).coeff k = 0

Tactic:
exact coeff_hermite_of_odd_add (Nat.not_even_iff_odd.1 h)

Result:
no goals

Proof state:
n k : ℕ
⊢ (hermite n).coeff k = if Even (n + k) then (-1) ^ ((n - k) / 2) * ↑(n - k - 1)‼ * ↑(n.choose k) else 0

Tactic:
split_ifs with h

Result:
case pos
n k : ℕ
h : Even (n + k)
⊢ (hermite n).coeff k = (-1) ^ ((n - k) / 2) * ↑(n - k - 1)‼ * ↑(n.choose k)

case neg
n k : ℕ
h : ¬Even (n + k)
⊢ (hermite n).coeff k = 0
-- Mathlib/LinearAlgebra/SModEq.lean
lemma nsmul (hxy : x ≡ y [SMOD U]) (n : ℕ) : n • x ≡ n • y [SMOD U]

Proof state:
R : Type u_1
inst✝² : Ring R
M : Type u_3
inst✝¹ : AddCommGroup M
inst✝ : Module R M
U : Submodule R M
x y : M
hxy : x ≡ y [SMOD U]
n : ℕ
⊢ n • x ≡ n • y [SMOD U]

Tactic:
rw [SModEq.def] at hxy ⊢

Result:
R : Type u_1
inst✝² : Ring R
M : Type u_3
inst✝¹ : AddCommGroup M
inst✝ : Module R M
U : Submodule R M
x y : M
hxy : Submodule.Quotient.mk x = Submodule.Quotient.mk y
n : ℕ
⊢ Submodule.Quotient.mk (n • x) = Submodule.Quotient.mk (n • y)

Proof state:
R : Type u_1
inst✝² : Ring R
M : Type u_3
inst✝¹ : AddCommGroup M
inst✝ : Module R M
U : Submodule R M
x y : M
hxy : Submodule.Quotient.mk x = Submodule.Quotient.mk y
n : ℕ
⊢ Submodule.Quotient.mk (n • x) = Submodule.Quotient.mk (n • y)

Tactic:
simp_rw [Quotient.mk_smul, hxy]

Result:
no goals
-- Mathlib/Analysis/SpecialFunctions/Log/Basic.lean
theorem exp_log_eq_abs (hx : x ≠ 0) : exp (log x) = |x|

Proof state:
x : ℝ
hx : x ≠ 0
⊢ rexp (log x) = |x|

Tactic:
rw [log_of_ne_zero hx, ← coe_expOrderIso_apply, OrderIso.apply_symm_apply, Subtype.coe_mk]

Result:
no goals
-- Mathlib/Analysis/Calculus/ContDiff/Defs.lean
theorem contDiffWithinAt_omega_iff_analyticWithinAt [CompleteSpace F] :
    ContDiffWithinAt 𝕜 ω f s x ↔ AnalyticWithinAt 𝕜 f s x

Proof state:
case intro.intro.intro.intro
𝕜 : Type u
inst✝⁵ : NontriviallyNormedField 𝕜
E : Type uE
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace 𝕜 E
F : Type uF
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace 𝕜 F
s : Set E
f : E → F
x : E
inst✝ : CompleteSpace F
h : AnalyticWithinAt 𝕜 f s x
u : Set E
hu : u ∈ 𝓝[insert x s] x
p : E → FormalMultilinearSeries 𝕜 E F
hp : HasFTaylorSeriesUpToOn ω f p u
h'p : ∀ (i : ℕ), AnalyticOn 𝕜 (fun x => p x i) u
⊢ ContDiffWithinAt 𝕜 ω f s x

Tactic:
exact ⟨u, hu, p, hp.of_le le_top, fun i ↦ h'p i⟩

Result:
no goals

Proof state:
𝕜 : Type u
inst✝⁵ : NontriviallyNormedField 𝕜
E : Type uE
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace 𝕜 E
F : Type uF
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace 𝕜 F
s : Set E
f : E → F
x : E
inst✝ : CompleteSpace F
h : AnalyticWithinAt 𝕜 f s x
⊢ ContDiffWithinAt 𝕜 ω f s x

Tactic:
obtain ⟨u, hu, p, hp, h'p⟩ := h.exists_hasFTaylorSeriesUpToOn ω

Result:
case intro.intro.intro.intro
𝕜 : Type u
inst✝⁵ : NontriviallyNormedField 𝕜
E : Type uE
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace 𝕜 E
F : Type uF
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace 𝕜 F
s : Set E
f : E → F
x : E
inst✝ : CompleteSpace F
h : AnalyticWithinAt 𝕜 f s x
u : Set E
hu : u ∈ 𝓝[insert x s] x
p : E → FormalMultilinearSeries 𝕜 E F
hp : HasFTaylorSeriesUpToOn ω f p u
h'p : ∀ (i : ℕ), AnalyticOn 𝕜 (fun x => p x i) u
⊢ ContDiffWithinAt 𝕜 ω f s x

Proof state:
𝕜 : Type u
inst✝⁵ : NontriviallyNormedField 𝕜
E : Type uE
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace 𝕜 E
F : Type uF
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace 𝕜 F
s : Set E
f : E → F
x : E
inst✝ : CompleteSpace F
⊢ ContDiffWithinAt 𝕜 ω f s x ↔ AnalyticWithinAt 𝕜 f s x

Tactic:
refine ⟨fun h ↦ h.analyticWithinAt, fun h ↦ ?_⟩

Result:
𝕜 : Type u
inst✝⁵ : NontriviallyNormedField 𝕜
E : Type uE
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace 𝕜 E
F : Type uF
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace 𝕜 F
s : Set E
f : E → F
x : E
inst✝ : CompleteSpace F
h : AnalyticWithinAt 𝕜 f s x
⊢ ContDiffWithinAt 𝕜 ω f s x
-- Mathlib/Analysis/Calculus/BumpFunction/Normed.lean
theorem support_normed_eq : Function.support (f.normed μ) = Metric.ball c f.rOut

Proof state:
E : Type u_1
inst✝⁷ : NormedAddCommGroup E
inst✝⁶ : NormedSpace ℝ E
inst✝⁵ : HasContDiffBump E
inst✝⁴ : MeasurableSpace E
c : E
f : ContDiffBump c
μ : Measure E
inst✝³ : BorelSpace E
inst✝² : FiniteDimensional ℝ E
inst✝¹ : IsLocallyFiniteMeasure μ
inst✝ : μ.IsOpenPosMeasure
⊢ support (f.normed μ) = ball c f.rOut

Tactic:
unfold ContDiffBump.normed

Result:
E : Type u_1
inst✝⁷ : NormedAddCommGroup E
inst✝⁶ : NormedSpace ℝ E
inst✝⁵ : HasContDiffBump E
inst✝⁴ : MeasurableSpace E
c : E
f : ContDiffBump c
μ : Measure E
inst✝³ : BorelSpace E
inst✝² : FiniteDimensional ℝ E
inst✝¹ : IsLocallyFiniteMeasure μ
inst✝ : μ.IsOpenPosMeasure
⊢ (support fun x => ↑f x / ∫ (x : E), ↑f x ∂μ) = ball c f.rOut

Proof state:
E : Type u_1
inst✝⁷ : NormedAddCommGroup E
inst✝⁶ : NormedSpace ℝ E
inst✝⁵ : HasContDiffBump E
inst✝⁴ : MeasurableSpace E
c : E
f : ContDiffBump c
μ : Measure E
inst✝³ : BorelSpace E
inst✝² : FiniteDimensional ℝ E
inst✝¹ : IsLocallyFiniteMeasure μ
inst✝ : μ.IsOpenPosMeasure
⊢ (support fun x => ↑f x / ∫ (x : E), ↑f x ∂μ) = ball c f.rOut

Tactic:
rw [support_div, f.support_eq, support_const f.integral_pos.ne', inter_univ]

Result:
no goals
-- Mathlib/Algebra/BigOperators/Group/Finset/Basic.lean
theorem prod_cancels_of_partition_cancels (R : Setoid α) [DecidableRel R]
    (h : ∀ x ∈ s, ∏ a ∈ s with R a x, f a = 1) : ∏ x ∈ s, f x = 1

Proof state:
α : Type u_3
β : Type u_4
s : Finset α
f : α → β
inst✝¹ : CommMonoid β
R : Setoid α
inst✝ : DecidableRel ⇑R
h : ∀ x ∈ s, ∏ a ∈ filter (fun a => R a x) s, f a = 1
⊢ ∏ x ∈ s, f x = 1

Tactic:
rw [prod_partition R, ← Finset.prod_eq_one]

Result:
α : Type u_3
β : Type u_4
s : Finset α
f : α → β
inst✝¹ : CommMonoid β
R : Setoid α
inst✝ : DecidableRel ⇑R
h : ∀ x ∈ s, ∏ a ∈ filter (fun a => R a x) s, f a = 1
⊢ ∀ x ∈ image (Quotient.mk R) s, ∏ y ∈ filter (fun y => ⟦y⟧ = x) s, f y = 1

Proof state:
α : Type u_3
β : Type u_4
s : Finset α
f : α → β
inst✝¹ : CommMonoid β
R : Setoid α
inst✝ : DecidableRel ⇑R
h : ∀ x ∈ s, ∏ a ∈ filter (fun a => R a x) s, f a = 1
⊢ ∀ x ∈ image (Quotient.mk R) s, ∏ y ∈ filter (fun y => ⟦y⟧ = x) s, f y = 1

Tactic:
intro xbar xbar_in_s

Result:
α : Type u_3
β : Type u_4
s : Finset α
f : α → β
inst✝¹ : CommMonoid β
R : Setoid α
inst✝ : DecidableRel ⇑R
h : ∀ x ∈ s, ∏ a ∈ filter (fun a => R a x) s, f a = 1
xbar : Quotient R
xbar_in_s : xbar ∈ image (Quotient.mk R) s
⊢ ∏ y ∈ filter (fun y => ⟦y⟧ = xbar) s, f y = 1

Proof state:
case intro.intro
α : Type u_3
β : Type u_4
s : Finset α
f : α → β
inst✝¹ : CommMonoid β
R : Setoid α
inst✝ : DecidableRel ⇑R
h : ∀ x ∈ s, ∏ a ∈ filter (fun a => R a x) s, f a = 1
x : α
x_in_s : x ∈ s
xbar_in_s : ⟦x⟧ ∈ image (Quotient.mk R) s
⊢ ∏ y ∈ filter (fun y => ⟦y⟧ = ⟦x⟧) s, f y = 1

Tactic:
simp only [← Quotient.eq] at h

Result:
case intro.intro
α : Type u_3
β : Type u_4
s : Finset α
f : α → β
inst✝¹ : CommMonoid β
R : Setoid α
inst✝ : DecidableRel ⇑R
x : α
x_in_s : x ∈ s
xbar_in_s : ⟦x⟧ ∈ image (Quotient.mk R) s
h : ∀ x ∈ s, ∏ x ∈ filter (fun a => ⟦a⟧ = ⟦x⟧) s, f x = 1
⊢ ∏ y ∈ filter (fun y => ⟦y⟧ = ⟦x⟧) s, f y = 1

Proof state:
case intro.intro
α : Type u_3
β : Type u_4
s : Finset α
f : α → β
inst✝¹ : CommMonoid β
R : Setoid α
inst✝ : DecidableRel ⇑R
x : α
x_in_s : x ∈ s
xbar_in_s : ⟦x⟧ ∈ image (Quotient.mk R) s
h : ∀ x ∈ s, ∏ x ∈ filter (fun a => ⟦a⟧ = ⟦x⟧) s, f x = 1
⊢ ∏ y ∈ filter (fun y => ⟦y⟧ = ⟦x⟧) s, f y = 1

Tactic:
exact h x x_in_s

Result:
no goals

Proof state:
α : Type u_3
β : Type u_4
s : Finset α
f : α → β
inst✝¹ : CommMonoid β
R : Setoid α
inst✝ : DecidableRel ⇑R
h : ∀ x ∈ s, ∏ a ∈ filter (fun a => R a x) s, f a = 1
xbar : Quotient R
xbar_in_s : xbar ∈ image (Quotient.mk R) s
⊢ ∏ y ∈ filter (fun y => ⟦y⟧ = xbar) s, f y = 1

Tactic:
obtain ⟨x, x_in_s, rfl⟩ := mem_image.mp xbar_in_s

Result:
case intro.intro
α : Type u_3
β : Type u_4
s : Finset α
f : α → β
inst✝¹ : CommMonoid β
R : Setoid α
inst✝ : DecidableRel ⇑R
h : ∀ x ∈ s, ∏ a ∈ filter (fun a => R a x) s, f a = 1
x : α
x_in_s : x ∈ s
xbar_in_s : ⟦x⟧ ∈ image (Quotient.mk R) s
⊢ ∏ y ∈ filter (fun y => ⟦y⟧ = ⟦x⟧) s, f y = 1
-- Mathlib/Topology/DiscreteQuotient.lean
theorem ofLE_map (cond : LEComap f A B) (h : B ≤ B') (a : A) :
    ofLE h (map f cond a) = map f (cond.mono le_rfl h) a

Proof state:
case mk
X : Type u_2
Y : Type u_3
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
f : C(X, Y)
A : DiscreteQuotient X
B B' : DiscreteQuotient Y
cond : LEComap f A B
h : B ≤ B'
a : Quotient A.toSetoid
a✝ : X
⊢ ofLE h (map f cond (Quot.mk (⇑A.toSetoid) a✝)) = map f ⋯ (Quot.mk (⇑A.toSetoid) a✝)

Tactic:
rfl

Result:
no goals

Proof state:
X : Type u_2
Y : Type u_3
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
f : C(X, Y)
A : DiscreteQuotient X
B B' : DiscreteQuotient Y
cond : LEComap f A B
h : B ≤ B'
a : Quotient A.toSetoid
⊢ ofLE h (map f cond a) = map f ⋯ a

Tactic:
rcases a with ⟨⟩

Result:
case mk
X : Type u_2
Y : Type u_3
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
f : C(X, Y)
A : DiscreteQuotient X
B B' : DiscreteQuotient Y
cond : LEComap f A B
h : B ≤ B'
a : Quotient A.toSetoid
a✝ : X
⊢ ofLE h (map f cond (Quot.mk (⇑A.toSetoid) a✝)) = map f ⋯ (Quot.mk (⇑A.toSetoid) a✝)
-- Mathlib/Probability/Independence/Kernel.lean
@[to_additive]
lemma iIndepFun.indepFun_div_left (hf_indep : iIndepFun (fun _ ↦ m) f κ μ)
    (hf_meas : ∀ i, Measurable (f i)) (i j k : ι) (hik : i ≠ k) (hjk : j ≠ k) :
    IndepFun (f i / f j) (f k) κ μ

Proof state:
α : Type u_1
Ω : Type u_2
ι : Type u_3
_mα : MeasurableSpace α
_mΩ : MeasurableSpace Ω
κ : Kernel α Ω
μ : Measure α
β : Type u_8
m : MeasurableSpace β
inst✝¹ : Div β
inst✝ : MeasurableDiv₂ β
f : ι → Ω → β
hf_indep : iIndepFun (fun x => m) f κ μ
hf_meas : ∀ (i : ι), Measurable (f i)
i j k : ι
hik : i ≠ k
hjk : j ≠ k
this : IndepFun (fun ω => (f i ω, f j ω)) (f k) κ μ
⊢ IndepFun (f i / f j) (f k) κ μ

Tactic:
simpa using this.comp (measurable_fst.div measurable_snd) measurable_id

Result:
no goals

Proof state:
α : Type u_1
Ω : Type u_2
ι : Type u_3
_mα : MeasurableSpace α
_mΩ : MeasurableSpace Ω
κ : Kernel α Ω
μ : Measure α
β : Type u_8
m : MeasurableSpace β
inst✝¹ : Div β
inst✝ : MeasurableDiv₂ β
f : ι → Ω → β
hf_indep : iIndepFun (fun x => m) f κ μ
hf_meas : ∀ (i : ι), Measurable (f i)
i j k : ι
hik : i ≠ k
hjk : j ≠ k
⊢ IndepFun (f i / f j) (f k) κ μ

Tactic:
have : IndepFun (fun ω => (f i ω, f j ω)) (f k) κ μ :=
  hf_indep.indepFun_prod_mk hf_meas i j k hik hjk

Result:
α : Type u_1
Ω : Type u_2
ι : Type u_3
_mα : MeasurableSpace α
_mΩ : MeasurableSpace Ω
κ : Kernel α Ω
μ : Measure α
β : Type u_8
m : MeasurableSpace β
inst✝¹ : Div β
inst✝ : MeasurableDiv₂ β
f : ι → Ω → β
hf_indep : iIndepFun (fun x => m) f κ μ
hf_meas : ∀ (i : ι), Measurable (f i)
i j k : ι
hik : i ≠ k
hjk : j ≠ k
this : IndepFun (fun ω => (f i ω, f j ω)) (f k) κ μ
⊢ IndepFun (f i / f j) (f k) κ μ
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Int/DivModLemmas.lean
theorem neg_mul_tmod_left (a b : Int) : (-(a * b)).tmod b = 0

Proof state:
a b : Int
⊢ b ∣ a * b

Tactic:
exact Int.dvd_mul_left a b

Result:
no goals

Proof state:
a b : Int
⊢ (-(a * b)).tmod b = 0

Tactic:
rw [← dvd_iff_tmod_eq_zero, Int.dvd_neg]

Result:
a b : Int
⊢ b ∣ a * b
-- Mathlib/RingTheory/HahnSeries/Addition.lean
theorem order_smul_not_lt [Zero Γ] (r : R) (x : HahnSeries Γ V) (h : r • x ≠ 0) :
    ¬ (r • x).order < x.order

Proof state:
Γ : Type u_1
R : Type u_3
inst✝³ : PartialOrder Γ
V : Type u_8
inst✝² : Zero V
inst✝¹ : SMulZeroClass R V
inst✝ : Zero Γ
r : R
x : HahnSeries Γ V
h : r • x ≠ 0
hx : x ≠ 0
⊢ ¬(r • x).order < x.order

Tactic:
simp_all only [order, dite_false]

Result:
Γ : Type u_1
R : Type u_3
inst✝³ : PartialOrder Γ
V : Type u_8
inst✝² : Zero V
inst✝¹ : SMulZeroClass R V
inst✝ : Zero Γ
r : R
x : HahnSeries Γ V
h : r • x ≠ 0
hx : x ≠ 0
⊢ ¬⋯.min ⋯ < ⋯.min ⋯

Proof state:
Γ : Type u_1
R : Type u_3
inst✝³ : PartialOrder Γ
V : Type u_8
inst✝² : Zero V
inst✝¹ : SMulZeroClass R V
inst✝ : Zero Γ
r : R
x : HahnSeries Γ V
h : r • x ≠ 0
⊢ ¬(r • x).order < x.order

Tactic:
have hx : x ≠ 0 := right_ne_zero_of_smul h

Result:
Γ : Type u_1
R : Type u_3
inst✝³ : PartialOrder Γ
V : Type u_8
inst✝² : Zero V
inst✝¹ : SMulZeroClass R V
inst✝ : Zero Γ
r : R
x : HahnSeries Γ V
h : r • x ≠ 0
hx : x ≠ 0
⊢ ¬(r • x).order < x.order

Proof state:
Γ : Type u_1
R : Type u_3
inst✝³ : PartialOrder Γ
V : Type u_8
inst✝² : Zero V
inst✝¹ : SMulZeroClass R V
inst✝ : Zero Γ
r : R
x : HahnSeries Γ V
h : r • x ≠ 0
hx : x ≠ 0
⊢ ¬⋯.min ⋯ < ⋯.min ⋯

Tactic:
exact Set.IsWF.min_of_subset_not_lt_min (Function.support_smul_subset_right (fun _ => r) x.coeff)

Result:
no goals
-- Mathlib/Algebra/Order/Group/Pointwise/Interval.lean
theorem Ico_mul_Icc_subset' (a b c d : α) : Ico a b * Icc c d ⊆ Ico (a * c) (b * d)

Proof state:
α : Type u_1
inst✝³ : Mul α
inst✝² : PartialOrder α
inst✝¹ : MulLeftStrictMono α
inst✝ : MulRightStrictMono α
a b c d : α
⊢ Ico a b * Icc c d ⊆ Ico (a * c) (b * d)

Tactic:
have := mulLeftMono_of_mulLeftStrictMono α

Result:
α : Type u_1
inst✝³ : Mul α
inst✝² : PartialOrder α
inst✝¹ : MulLeftStrictMono α
inst✝ : MulRightStrictMono α
a b c d : α
this : MulLeftMono α
⊢ Ico a b * Icc c d ⊆ Ico (a * c) (b * d)

Proof state:
α : Type u_1
inst✝³ : Mul α
inst✝² : PartialOrder α
inst✝¹ : MulLeftStrictMono α
inst✝ : MulRightStrictMono α
a b c d : α
this : MulLeftMono α
⊢ Ico a b * Icc c d ⊆ Ico (a * c) (b * d)

Tactic:
have := mulRightMono_of_mulRightStrictMono α

Result:
α : Type u_1
inst✝³ : Mul α
inst✝² : PartialOrder α
inst✝¹ : MulLeftStrictMono α
inst✝ : MulRightStrictMono α
a b c d : α
this✝ : MulLeftMono α
this : MulRightMono α
⊢ Ico a b * Icc c d ⊆ Ico (a * c) (b * d)

Proof state:
α : Type u_1
inst✝³ : Mul α
inst✝² : PartialOrder α
inst✝¹ : MulLeftStrictMono α
inst✝ : MulRightStrictMono α
a b c d : α
this✝ : MulLeftMono α
this : MulRightMono α
⊢ Ico a b * Icc c d ⊆ Ico (a * c) (b * d)

Tactic:
rintro x ⟨y, ⟨hya, hyb⟩, z, ⟨hzc, hzd⟩, rfl⟩

Result:
case intro.intro.intro.intro.intro.intro
α : Type u_1
inst✝³ : Mul α
inst✝² : PartialOrder α
inst✝¹ : MulLeftStrictMono α
inst✝ : MulRightStrictMono α
a b c d : α
this✝ : MulLeftMono α
this : MulRightMono α
y : α
hya : a ≤ y
hyb : y < b
z : α
hzc : c ≤ z
hzd : z ≤ d
⊢ (fun x1 x2 => x1 * x2) y z ∈ Ico (a * c) (b * d)

Proof state:
case intro.intro.intro.intro.intro.intro
α : Type u_1
inst✝³ : Mul α
inst✝² : PartialOrder α
inst✝¹ : MulLeftStrictMono α
inst✝ : MulRightStrictMono α
a b c d : α
this✝ : MulLeftMono α
this : MulRightMono α
y : α
hya : a ≤ y
hyb : y < b
z : α
hzc : c ≤ z
hzd : z ≤ d
⊢ (fun x1 x2 => x1 * x2) y z ∈ Ico (a * c) (b * d)

Tactic:
exact ⟨mul_le_mul' hya hzc, mul_lt_mul_of_lt_of_le hyb hzd⟩

Result:
no goals
-- Mathlib/AlgebraicGeometry/EllipticCurve/Jacobian.lean
lemma baseChange_negAddY (P Q : Fin 3 → A) : (W'.baseChange B).toJacobian.negAddY (f ∘ P) (f ∘ Q) =
    f ((W'.baseChange A).toJacobian.negAddY P Q)

Proof state:
R : Type r
inst✝¹⁰ : CommRing R
W' : Jacobian R
S : Type s
inst✝⁹ : CommRing S
inst✝⁸ : Algebra R S
A : Type u
inst✝⁷ : CommRing A
inst✝⁶ : Algebra R A
inst✝⁵ : Algebra S A
inst✝⁴ : IsScalarTower R S A
B : Type v
inst✝³ : CommRing B
inst✝² : Algebra R B
inst✝¹ : Algebra S B
inst✝ : IsScalarTower R S B
f : A →ₐ[S] B
P Q : Fin 3 → A
⊢ (baseChange W' B).toJacobian.negAddY (⇑f ∘ P) (⇑f ∘ Q) = f ((baseChange W' A).toJacobian.negAddY P Q)

Tactic:
rw [← RingHom.coe_coe, ← map_negAddY, map_baseChange]

Result:
no goals