harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/Topology/Instances/ENNReal/Lemmas.lean
theorem hasSum_iff_tendsto_nat_of_nonneg {f : ℕ → ℝ} (hf : ∀ i, 0 ≤ f i) (r : ℝ) :
    HasSum f r ↔ Tendsto (fun n : ℕ => ∑ i ∈ Finset.range n, f i) atTop (𝓝 r)

Proof state:
case intro
r : ℝ
f : ℕ → ℝ≥0
⊢ (∃ (hx : 0 ≤ r), Tendsto (fun a => ∑ i ∈ a, f i) atTop (𝓝 ⟨r, hx⟩)) ↔
    ∃ (hx : 0 ≤ r), Tendsto (fun a => ∑ i ∈ Finset.range a, f i) atTop (𝓝 ⟨r, hx⟩)

Tactic:
exact exists_congr fun hr => NNReal.hasSum_iff_tendsto_nat

Result:
no goals

Proof state:
f : ℕ → ℝ
hf : ∀ (i : ℕ), 0 ≤ f i
r : ℝ
⊢ HasSum f r ↔ Tendsto (fun n => ∑ i ∈ Finset.range n, f i) atTop (𝓝 r)

Tactic:
lift f to ℕ → ℝ≥0 using hf

Result:
case intro
r : ℝ
f : ℕ → ℝ≥0
⊢ HasSum (fun i => ↑(f i)) r ↔ Tendsto (fun n => ∑ i ∈ Finset.range n, (fun i => ↑(f i)) i) atTop (𝓝 r)

Proof state:
case intro
r : ℝ
f : ℕ → ℝ≥0
⊢ HasSum (fun i => ↑(f i)) r ↔ Tendsto (fun n => ∑ i ∈ Finset.range n, (fun i => ↑(f i)) i) atTop (𝓝 r)

Tactic:
simp only [HasSum, ← NNReal.coe_sum, NNReal.tendsto_coe']

Result:
case intro
r : ℝ
f : ℕ → ℝ≥0
⊢ (∃ (hx : 0 ≤ r), Tendsto (fun a => ∑ i ∈ a, f i) atTop (𝓝 ⟨r, hx⟩)) ↔
    ∃ (hx : 0 ≤ r), Tendsto (fun a => ∑ i ∈ Finset.range a, f i) atTop (𝓝 ⟨r, hx⟩)
-- Mathlib/Probability/Kernel/Basic.lean
theorem lintegral_deterministic' {f : β → ℝ≥0∞} {g : α → β} {a : α} (hg : Measurable g)
    (hf : Measurable f) : ∫⁻ x, f x ∂deterministic g hg a = f (g a)

Proof state:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
f : β → ℝ≥0∞
g : α → β
a : α
hg : Measurable g
hf : Measurable f
⊢ ∫⁻ (x : β), f x ∂(deterministic g hg) a = f (g a)

Tactic:
rw [deterministic_apply, lintegral_dirac' _ hf]

Result:
no goals
-- Mathlib/Data/Complex/Trigonometric.lean
theorem ofReal_cosh_ofReal_re (x : ℝ) : ((cosh x).re : ℂ) = cosh x :=
  conj_eq_iff_re.1 <| by rw [← cosh_conj, conj_ofReal]

Proof state:
x : ℝ
⊢ (starRingEnd ℂ) (cosh ↑x) = cosh ↑x

Tactic:
rw [← cosh_conj, conj_ofReal]

Result:
no goals
-- Mathlib/SetTheory/Surreal/Multiplication.lean
lemma P3_neg : P3 x₁ x₂ y₁ y₂ ↔ P3 (-x₂) (-x₁) y₁ y₂

Proof state:
x₁ x₂ y₁ y₂ : PGame
⊢ ⟦x₁ * y₂⟧ + ⟦x₂ * y₁⟧ < ⟦x₁ * y₁⟧ + ⟦x₂ * y₂⟧ ↔ -⟦x₂ * y₂⟧ + -⟦x₁ * y₁⟧ < -⟦x₂ * y₁⟧ + -⟦x₁ * y₂⟧

Tactic:
rw [← _root_.neg_lt_neg_iff]

Result:
x₁ x₂ y₁ y₂ : PGame
⊢ -(⟦x₁ * y₁⟧ + ⟦x₂ * y₂⟧) < -(⟦x₁ * y₂⟧ + ⟦x₂ * y₁⟧) ↔ -⟦x₂ * y₂⟧ + -⟦x₁ * y₁⟧ < -⟦x₂ * y₁⟧ + -⟦x₁ * y₂⟧

Proof state:
x₁ x₂ y₁ y₂ : PGame
⊢ P3 x₁ x₂ y₁ y₂ ↔ P3 (-x₂) (-x₁) y₁ y₂

Tactic:
simp_rw [P3, quot_neg_mul]

Result:
x₁ x₂ y₁ y₂ : PGame
⊢ ⟦x₁ * y₂⟧ + ⟦x₂ * y₁⟧ < ⟦x₁ * y₁⟧ + ⟦x₂ * y₂⟧ ↔ -⟦x₂ * y₂⟧ + -⟦x₁ * y₁⟧ < -⟦x₂ * y₁⟧ + -⟦x₁ * y₂⟧

Proof state:
x₁ x₂ y₁ y₂ : PGame
⊢ -(⟦x₁ * y₁⟧ + ⟦x₂ * y₂⟧) < -(⟦x₁ * y₂⟧ + ⟦x₂ * y₁⟧) ↔ -⟦x₂ * y₂⟧ + -⟦x₁ * y₁⟧ < -⟦x₂ * y₁⟧ + -⟦x₁ * y₂⟧

Tactic:
abel_nf

Result:
no goals
-- Mathlib/AlgebraicTopology/DoldKan/Projections.lean
theorem P_f_0_eq (q : ℕ) : ((P q).f 0 : X _⦋0⦌ ⟶ X _⦋0⦌) = 𝟙 _

Proof state:
case zero
C : Type u_1
inst✝¹ : Category.{u_2, u_1} C
inst✝ : Preadditive C
X : SimplicialObject C
⊢ (P 0).f 0 = 𝟙 (K[X].X 0)

Tactic:
rfl

Result:
no goals

Proof state:
C : Type u_1
inst✝¹ : Category.{u_2, u_1} C
inst✝ : Preadditive C
X : SimplicialObject C
q : ℕ
⊢ (P q).f 0 = 𝟙 (K[X].X 0)

Tactic:
induction' q with q hq

Result:
case zero
C : Type u_1
inst✝¹ : Category.{u_2, u_1} C
inst✝ : Preadditive C
X : SimplicialObject C
⊢ (P 0).f 0 = 𝟙 (K[X].X 0)

case succ
C : Type u_1
inst✝¹ : Category.{u_2, u_1} C
inst✝ : Preadditive C
X : SimplicialObject C
q : ℕ
hq : (P q).f 0 = 𝟙 (K[X].X 0)
⊢ (P (q + 1)).f 0 = 𝟙 (K[X].X 0)

Proof state:
case succ
C : Type u_1
inst✝¹ : Category.{u_2, u_1} C
inst✝ : Preadditive C
X : SimplicialObject C
q : ℕ
hq : (P q).f 0 = 𝟙 (K[X].X 0)
⊢ (P (q + 1)).f 0 = 𝟙 (K[X].X 0)

Tactic:
simp only [P_succ, HomologicalComplex.add_f_apply, HomologicalComplex.comp_f,
  HomologicalComplex.id_f, id_comp, hq, Hσ_eq_zero, add_zero]

Result:
no goals
-- Mathlib/MeasureTheory/Integral/MeanInequalities.lean
theorem ae_eq_zero_of_lintegral_rpow_eq_zero {p : ℝ} (hp0 : 0 ≤ p) {f : α → ℝ≥0∞}
    (hf : AEMeasurable f μ) (hf_zero : ∫⁻ a, f a ^ p ∂μ = 0) : f =ᵐ[μ] 0

Proof state:
case h
α : Type u_1
inst✝ : MeasurableSpace α
μ : Measure α
p : ℝ
hp0 : 0 ≤ p
f : α → ℝ≥0∞
hf : AEMeasurable f μ
hf_zero : (fun x => f x ^ p) =ᶠ[ae μ] 0
x : α
⊢ ¬f x = 0 → ¬f x ^ p = 0

Tactic:
exact fun hx => (rpow_pos_of_nonneg (pos_iff_ne_zero.2 hx) hp0).ne'

Result:
no goals

Proof state:
α : Type u_1
inst✝ : MeasurableSpace α
μ : Measure α
p : ℝ
hp0 : 0 ≤ p
f : α → ℝ≥0∞
hf : AEMeasurable f μ
hf_zero : ∫⁻ (a : α), f a ^ p ∂μ = 0
⊢ f =ᶠ[ae μ] 0

Tactic:
rw [lintegral_eq_zero_iff' (hf.pow_const p)] at hf_zero

Result:
α : Type u_1
inst✝ : MeasurableSpace α
μ : Measure α
p : ℝ
hp0 : 0 ≤ p
f : α → ℝ≥0∞
hf : AEMeasurable f μ
hf_zero : (fun x => f x ^ p) =ᶠ[ae μ] 0
⊢ f =ᶠ[ae μ] 0

Proof state:
α : Type u_1
inst✝ : MeasurableSpace α
μ : Measure α
p : ℝ
hp0 : 0 ≤ p
f : α → ℝ≥0∞
hf : AEMeasurable f μ
hf_zero : (fun x => f x ^ p) =ᶠ[ae μ] 0
⊢ f =ᶠ[ae μ] 0

Tactic:
filter_upwards [hf_zero] with x

Result:
case h
α : Type u_1
inst✝ : MeasurableSpace α
μ : Measure α
p : ℝ
hp0 : 0 ≤ p
f : α → ℝ≥0∞
hf : AEMeasurable f μ
hf_zero : (fun x => f x ^ p) =ᶠ[ae μ] 0
x : α
⊢ f x ^ p = 0 x → f x = 0 x

Proof state:
case h
α : Type u_1
inst✝ : MeasurableSpace α
μ : Measure α
p : ℝ
hp0 : 0 ≤ p
f : α → ℝ≥0∞
hf : AEMeasurable f μ
hf_zero : (fun x => f x ^ p) =ᶠ[ae μ] 0
x : α
⊢ f x ^ p = 0 x → f x = 0 x

Tactic:
rw [Pi.zero_apply, ← not_imp_not]

Result:
case h
α : Type u_1
inst✝ : MeasurableSpace α
μ : Measure α
p : ℝ
hp0 : 0 ≤ p
f : α → ℝ≥0∞
hf : AEMeasurable f μ
hf_zero : (fun x => f x ^ p) =ᶠ[ae μ] 0
x : α
⊢ ¬f x = 0 → ¬f x ^ p = 0
-- Mathlib/Logic/Equiv/PartialEquiv.lean
theorem iff_preimage_eq : e.IsImage s t ↔ e.source ∩ e ⁻¹' t = e.source ∩ s

Proof state:
α : Type u_1
β : Type u_2
e : PartialEquiv α β
s : Set α
t : Set β
⊢ e.IsImage s t ↔ e.source ∩ ↑e ⁻¹' t = e.source ∩ s

Tactic:
simp only [IsImage, Set.ext_iff, mem_inter_iff, mem_preimage, and_congr_right_iff]

Result:
no goals
-- Mathlib/Probability/Kernel/Composition/Prod.lean
lemma prodAssoc_prod (κ : Kernel α β) [IsSFiniteKernel κ] (η : Kernel α γ) [IsSFiniteKernel η]
    (ξ : Kernel α δ) [IsSFiniteKernel ξ] :
    ((κ ×ₖ ξ) ×ₖ η).map MeasurableEquiv.prodAssoc = κ ×ₖ (ξ ×ₖ η)

Proof state:
case h
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
γ : Type u_4
δ : Type u_5
mγ : MeasurableSpace γ
mδ : MeasurableSpace δ
κ : Kernel α β
inst✝² : IsSFiniteKernel κ
η : Kernel α γ
inst✝¹ : IsSFiniteKernel η
ξ : Kernel α δ
inst✝ : IsSFiniteKernel ξ
a : α
⊢ ((κ ×ₖ ξ ×ₖ η).map ⇑MeasurableEquiv.prodAssoc) a = (κ ×ₖ (ξ ×ₖ η)) a

Tactic:
rw [map_apply _ (by fun_prop), prod_apply, prod_apply, Measure.prodAssoc_prod, prod_apply,
  prod_apply]

Result:
no goals

Proof state:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
γ : Type u_4
δ : Type u_5
mγ : MeasurableSpace γ
mδ : MeasurableSpace δ
κ : Kernel α β
inst✝² : IsSFiniteKernel κ
η : Kernel α γ
inst✝¹ : IsSFiniteKernel η
ξ : Kernel α δ
inst✝ : IsSFiniteKernel ξ
⊢ (κ ×ₖ ξ ×ₖ η).map ⇑MeasurableEquiv.prodAssoc = κ ×ₖ (ξ ×ₖ η)

Tactic:
ext1 a

Result:
case h
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
γ : Type u_4
δ : Type u_5
mγ : MeasurableSpace γ
mδ : MeasurableSpace δ
κ : Kernel α β
inst✝² : IsSFiniteKernel κ
η : Kernel α γ
inst✝¹ : IsSFiniteKernel η
ξ : Kernel α δ
inst✝ : IsSFiniteKernel ξ
a : α
⊢ ((κ ×ₖ ξ ×ₖ η).map ⇑MeasurableEquiv.prodAssoc) a = (κ ×ₖ (ξ ×ₖ η)) a

Proof state:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
γ : Type u_4
δ : Type u_5
mγ : MeasurableSpace γ
mδ : MeasurableSpace δ
κ : Kernel α β
inst✝² : IsSFiniteKernel κ
η : Kernel α γ
inst✝¹ : IsSFiniteKernel η
ξ : Kernel α δ
inst✝ : IsSFiniteKernel ξ
a : α
⊢ Measurable ⇑MeasurableEquiv.prodAssoc

Tactic:
fun_prop

Result:
no goals
-- Mathlib/Topology/MetricSpace/PiNat.lean
theorem cylinder_zero (x : ∀ n, E n) : cylinder x 0 = univ

Proof state:
E : ℕ → Type u_1
x : (n : ℕ) → E n
⊢ cylinder x 0 = univ

Tactic:
simp [cylinder_eq_pi]

Result:
no goals
-- Mathlib/Topology/Path.lean
theorem reparam_id (γ : Path x y) : γ.reparam id continuous_id rfl rfl = γ

Proof state:
case a.h
X : Type u_1
inst✝ : TopologicalSpace X
x y : X
γ : Path x y
x✝ : ↑I
⊢ (γ.reparam id ⋯ ⋯ ⋯) x✝ = γ x✝

Tactic:
rfl

Result:
no goals

Proof state:
X : Type u_1
inst✝ : TopologicalSpace X
x y : X
γ : Path x y
⊢ γ.reparam id ⋯ ⋯ ⋯ = γ

Tactic:
ext

Result:
case a.h
X : Type u_1
inst✝ : TopologicalSpace X
x y : X
γ : Path x y
x✝ : ↑I
⊢ (γ.reparam id ⋯ ⋯ ⋯) x✝ = γ x✝
-- Mathlib/Algebra/Homology/HomotopyCategory/HomComplex.lean
@[simp]
lemma units_smul_comp {n₁ n₂ n₁₂ : ℤ} (k : Rˣ) (z₁ : Cochain F G n₁) (z₂ : Cochain G K n₂)
    (h : n₁ + n₂ = n₁₂) : (k • z₁).comp z₂ h = k • (z₁.comp z₂ h)

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₁₂ : ℤ
k : Rˣ
z₁ : Cochain F G n₁
z₂ : Cochain G K n₂
h : n₁ + n₂ = n₁₂
⊢ (k • z₁).comp z₂ h = k • z₁.comp z₂ h

Tactic:
apply Cochain.smul_comp

Result:
no goals
-- Mathlib/Combinatorics/SimpleGraph/Density.lean
theorem edgeDensity_add_edgeDensity_compl (hs : s.Nonempty) (ht : t.Nonempty) :
    edgeDensity r s t + edgeDensity (fun x y ↦ ¬r x y) s t = 1

Proof state:
α : Type u_4
β : Type u_5
r : α → β → Prop
inst✝ : (a : α) → DecidablePred (r a)
s : Finset α
t : Finset β
hs : s.Nonempty
ht : t.Nonempty
⊢ edgeDensity r s t + edgeDensity (fun x y => ¬r x y) s t = 1

Tactic:
rw [edgeDensity, edgeDensity, div_add_div_same, div_eq_one_iff_eq]

Result:
α : Type u_4
β : Type u_5
r : α → β → Prop
inst✝ : (a : α) → DecidablePred (r a)
s : Finset α
t : Finset β
hs : s.Nonempty
ht : t.Nonempty
⊢ ↑(#(interedges r s t)) + ↑(#(interedges (fun x y => ¬r x y) s t)) = ↑(#s) * ↑(#t)

α : Type u_4
β : Type u_5
r : α → β → Prop
inst✝ : (a : α) → DecidablePred (r a)
s : Finset α
t : Finset β
hs : s.Nonempty
ht : t.Nonempty
⊢ ↑(#s) * ↑(#t) ≠ 0

Proof state:
α : Type u_4
β : Type u_5
r : α → β → Prop
inst✝ : (a : α) → DecidablePred (r a)
s : Finset α
t : Finset β
hs : s.Nonempty
ht : t.Nonempty
⊢ ↑(#(interedges r s t)) + ↑(#(interedges (fun x y => ¬r x y) s t)) = ↑(#s) * ↑(#t)

Tactic:
exact mod_cast card_interedges_add_card_interedges_compl r s t

Result:
no goals

Proof state:
α : Type u_4
β : Type u_5
r : α → β → Prop
inst✝ : (a : α) → DecidablePred (r a)
s : Finset α
t : Finset β
hs : s.Nonempty
ht : t.Nonempty
⊢ ↑(#s) * ↑(#t) ≠ 0

Tactic:
exact mod_cast (mul_pos hs.card_pos ht.card_pos).ne'

Result:
no goals
-- Mathlib/RingTheory/IsAdjoinRoot.lean
theorem eval₂_repr_eq_eval₂_of_map_eq (h : IsAdjoinRoot S f) (z : S) (w : R[X])
    (hzw : h.map w = z) : (h.repr z).eval₂ i x = w.eval₂ i x

Proof state:
R : Type u
S : Type v
inst✝³ : CommRing R
inst✝² : Ring S
f : R[X]
inst✝¹ : Algebra R S
T : Type u_1
inst✝ : CommRing T
i : R →+* T
x : T
hx : eval₂ i x f = 0
h : IsAdjoinRoot S f
z : S
w : R[X]
hzw : f ∣ h.repr z - w
⊢ eval₂ i x (h.repr z) = eval₂ i x w

Tactic:
obtain ⟨y, hy⟩ := hzw

Result:
case intro
R : Type u
S : Type v
inst✝³ : CommRing R
inst✝² : Ring S
f : R[X]
inst✝¹ : Algebra R S
T : Type u_1
inst✝ : CommRing T
i : R →+* T
x : T
hx : eval₂ i x f = 0
h : IsAdjoinRoot S f
z : S
w y : R[X]
hy : h.repr z - w = f * y
⊢ eval₂ i x (h.repr z) = eval₂ i x w

Proof state:
R : Type u
S : Type v
inst✝³ : CommRing R
inst✝² : Ring S
f : R[X]
inst✝¹ : Algebra R S
T : Type u_1
inst✝ : CommRing T
i : R →+* T
x : T
hx : eval₂ i x f = 0
h : IsAdjoinRoot S f
z : S
w : R[X]
hzw : h.map w = z
⊢ eval₂ i x (h.repr z) = eval₂ i x w

Tactic:
rw [eq_comm, ← sub_eq_zero, ← h.map_repr z, ← map_sub, h.map_eq_zero_iff] at hzw

Result:
R : Type u
S : Type v
inst✝³ : CommRing R
inst✝² : Ring S
f : R[X]
inst✝¹ : Algebra R S
T : Type u_1
inst✝ : CommRing T
i : R →+* T
x : T
hx : eval₂ i x f = 0
h : IsAdjoinRoot S f
z : S
w : R[X]
hzw : f ∣ h.repr z - w
⊢ eval₂ i x (h.repr z) = eval₂ i x w

Proof state:
case intro
R : Type u
S : Type v
inst✝³ : CommRing R
inst✝² : Ring S
f : R[X]
inst✝¹ : Algebra R S
T : Type u_1
inst✝ : CommRing T
i : R →+* T
x : T
hx : eval₂ i x f = 0
h : IsAdjoinRoot S f
z : S
w y : R[X]
hy : h.repr z - w = f * y
⊢ eval₂ i x (h.repr z) = eval₂ i x w

Tactic:
rw [← sub_eq_zero, ← eval₂_sub, hy, eval₂_mul, hx, zero_mul]

Result:
no goals
-- Mathlib/RingTheory/FractionalIdeal/Operations.lean
theorem map_div (I J : FractionalIdeal R₁⁰ K) (h : K ≃ₐ[R₁] K') :
    (I / J).map (h : K →ₐ[R₁] K') = I.map h / J.map h

Proof state:
case pos
R₁ : Type u_3
inst✝⁷ : CommRing R₁
K : Type u_4
inst✝⁶ : Field K
inst✝⁵ : Algebra R₁ K
inst✝⁴ : IsFractionRing R₁ K
inst✝³ : IsDomain R₁
K' : Type u_5
inst✝² : Field K'
inst✝¹ : Algebra R₁ K'
inst✝ : IsFractionRing R₁ K'
I J : FractionalIdeal R₁⁰ K
h : K ≃ₐ[R₁] K'
H : J = 0
⊢ map (↑h) (I / J) = map (↑h) I / map (↑h) J

Tactic:
rw [H, div_zero, map_zero, div_zero]

Result:
no goals

Proof state:
case neg
R₁ : Type u_3
inst✝⁷ : CommRing R₁
K : Type u_4
inst✝⁶ : Field K
inst✝⁵ : Algebra R₁ K
inst✝⁴ : IsFractionRing R₁ K
inst✝³ : IsDomain R₁
K' : Type u_5
inst✝² : Field K'
inst✝¹ : Algebra R₁ K'
inst✝ : IsFractionRing R₁ K'
I J : FractionalIdeal R₁⁰ K
h : K ≃ₐ[R₁] K'
H : ¬J = 0
⊢ map (↑h) (I / J) = map (↑h) I / map (↑h) J

Tactic:
rw [← coeToSubmodule_inj, div_nonzero H, div_nonzero (map_ne_zero _ H)]

Result:
case neg
R₁ : Type u_3
inst✝⁷ : CommRing R₁
K : Type u_4
inst✝⁶ : Field K
inst✝⁵ : Algebra R₁ K
inst✝⁴ : IsFractionRing R₁ K
inst✝³ : IsDomain R₁
K' : Type u_5
inst✝² : Field K'
inst✝¹ : Algebra R₁ K'
inst✝ : IsFractionRing R₁ K'
I J : FractionalIdeal R₁⁰ K
h : K ≃ₐ[R₁] K'
H : ¬J = 0
⊢ ↑(map ↑h ⟨↑I / ↑J, ⋯⟩) = ↑⟨↑(map (↑h) I) / ↑(map (↑h) J), ⋯⟩

Proof state:
case neg
R₁ : Type u_3
inst✝⁷ : CommRing R₁
K : Type u_4
inst✝⁶ : Field K
inst✝⁵ : Algebra R₁ K
inst✝⁴ : IsFractionRing R₁ K
inst✝³ : IsDomain R₁
K' : Type u_5
inst✝² : Field K'
inst✝¹ : Algebra R₁ K'
inst✝ : IsFractionRing R₁ K'
I J : FractionalIdeal R₁⁰ K
h : K ≃ₐ[R₁] K'
H : ¬J = 0
⊢ ↑(map ↑h ⟨↑I / ↑J, ⋯⟩) = ↑⟨↑(map (↑h) I) / ↑(map (↑h) J), ⋯⟩

Tactic:
simp [Submodule.map_div]

Result:
no goals

Proof state:
R₁ : Type u_3
inst✝⁷ : CommRing R₁
K : Type u_4
inst✝⁶ : Field K
inst✝⁵ : Algebra R₁ K
inst✝⁴ : IsFractionRing R₁ K
inst✝³ : IsDomain R₁
K' : Type u_5
inst✝² : Field K'
inst✝¹ : Algebra R₁ K'
inst✝ : IsFractionRing R₁ K'
I J : FractionalIdeal R₁⁰ K
h : K ≃ₐ[R₁] K'
⊢ map (↑h) (I / J) = map (↑h) I / map (↑h) J

Tactic:
by_cases H : J = 0

Result:
case pos
R₁ : Type u_3
inst✝⁷ : CommRing R₁
K : Type u_4
inst✝⁶ : Field K
inst✝⁵ : Algebra R₁ K
inst✝⁴ : IsFractionRing R₁ K
inst✝³ : IsDomain R₁
K' : Type u_5
inst✝² : Field K'
inst✝¹ : Algebra R₁ K'
inst✝ : IsFractionRing R₁ K'
I J : FractionalIdeal R₁⁰ K
h : K ≃ₐ[R₁] K'
H : J = 0
⊢ map (↑h) (I / J) = map (↑h) I / map (↑h) J

case neg
R₁ : Type u_3
inst✝⁷ : CommRing R₁
K : Type u_4
inst✝⁶ : Field K
inst✝⁵ : Algebra R₁ K
inst✝⁴ : IsFractionRing R₁ K
inst✝³ : IsDomain R₁
K' : Type u_5
inst✝² : Field K'
inst✝¹ : Algebra R₁ K'
inst✝ : IsFractionRing R₁ K'
I J : FractionalIdeal R₁⁰ K
h : K ≃ₐ[R₁] K'
H : ¬J = 0
⊢ map (↑h) (I / J) = map (↑h) I / map (↑h) J
-- Mathlib/MeasureTheory/Function/LpSpace/Basic.lean
theorem edist_toLp_toLp (f g : α → E) (hf : MemLp f p μ) (hg : MemLp g p μ) :
    edist (hf.toLp f) (hg.toLp g) = eLpNorm (f - g) p μ

Proof state:
α : Type u_1
E : Type u_4
m0 : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
inst✝ : NormedAddCommGroup E
f g : α → E
hf : MemLp f p μ
hg : MemLp g p μ
⊢ eLpNorm (↑↑(MemLp.toLp f hf) - ↑↑(MemLp.toLp g hg)) p μ = eLpNorm (f - g) p μ

Tactic:
exact eLpNorm_congr_ae (hf.coeFn_toLp.sub hg.coeFn_toLp)

Result:
no goals

Proof state:
α : Type u_1
E : Type u_4
m0 : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
inst✝ : NormedAddCommGroup E
f g : α → E
hf : MemLp f p μ
hg : MemLp g p μ
⊢ edist (MemLp.toLp f hf) (MemLp.toLp g hg) = eLpNorm (f - g) p μ

Tactic:
rw [edist_def]

Result:
α : Type u_1
E : Type u_4
m0 : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
inst✝ : NormedAddCommGroup E
f g : α → E
hf : MemLp f p μ
hg : MemLp g p μ
⊢ eLpNorm (↑↑(MemLp.toLp f hf) - ↑↑(MemLp.toLp g hg)) p μ = eLpNorm (f - g) p μ
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Vector/MapIdx.lean
theorem mem_mapFinIdx {b : β} {l : Vector α n} {f : (i : Nat) → α → (h : i < n) → β} :
    b ∈ l.mapFinIdx f ↔ ∃ (i : Nat) (h : i < n), f i l[i] h = b

Proof state:
β : Type u_1
α : Type u_2
n : Nat
b : β
l : Vector α n
f : (i : Nat) → α → i < n → β
⊢ b ∈ l.mapFinIdx f ↔ ∃ i h, f i l[i] h = b

Tactic:
rcases l with ⟨l, rfl⟩

Result:
case mk
β : Type u_1
α : Type u_2
b : β
l : Array α
f : (i : Nat) → α → i < l.size → β
⊢ b ∈ { toArray := l, size_toArray := ⋯ }.mapFinIdx f ↔ ∃ i h, f i { toArray := l, size_toArray := ⋯ }[i] h = b

Proof state:
case mk
β : Type u_1
α : Type u_2
b : β
l : Array α
f : (i : Nat) → α → i < l.size → β
⊢ b ∈ { toArray := l, size_toArray := ⋯ }.mapFinIdx f ↔ ∃ i h, f i { toArray := l, size_toArray := ⋯ }[i] h = b

Tactic:
simp

Result:
no goals
-- Mathlib/Analysis/SpecialFunctions/Complex/Circle.lean
lemma coe_toCircle (θ : Angle) : (θ.toCircle : ℂ) = θ.cos + θ.sin * I

Proof state:
θ : Angle
⊢ ↑θ.toCircle = ↑θ.cos + ↑θ.sin * I

Tactic:
induction θ using Real.Angle.induction_on

Result:
case h
x✝ : ℝ
⊢ ↑(↑x✝).toCircle = ↑(↑x✝).cos + ↑(↑x✝).sin * I

Proof state:
case h
x✝ : ℝ
⊢ ↑(↑x✝).toCircle = ↑(↑x✝).cos + ↑(↑x✝).sin * I

Tactic:
simp [exp_mul_I]

Result:
no goals
-- Mathlib/GroupTheory/Finiteness.lean
theorem Monoid.fg_iff_submonoid_fg (N : Submonoid M) : Monoid.FG N ↔ N.FG

Proof state:
M : Type u_1
inst✝ : Monoid M
N : Submonoid M
⊢ FG ↥N ↔ (Submonoid.map N.subtype ⊤).FG

Tactic:
exact ⟨fun h => h.out.map N.subtype, fun h => ⟨h.map_injective N.subtype Subtype.coe_injective⟩⟩

Result:
no goals

Proof state:
M : Type u_1
inst✝ : Monoid M
N : Submonoid M
⊢ FG ↥N ↔ N.FG

Tactic:
conv_rhs => rw [← N.mrange_subtype, MonoidHom.mrange_eq_map]

Result:
M : Type u_1
inst✝ : Monoid M
N : Submonoid M
⊢ FG ↥N ↔ (Submonoid.map N.subtype ⊤).FG
-- Mathlib/RingTheory/ZMod.lean
theorem isReduced_zmod {n : ℕ} : IsReduced (ZMod n) ↔ Squarefree n ∨ n = 0

Proof state:
n : ℕ
⊢ IsReduced (ZMod n) ↔ Squarefree n ∨ n = 0

Tactic:
rw [← RingHom.ker_isRadical_iff_reduced_of_surjective
    (ZMod.ringHom_surjective <| Int.castRingHom <| ZMod n),
    ZMod.ker_intCastRingHom, ← isRadical_iff_span_singleton, isRadical_iff_squarefree_or_zero,
    Int.squarefree_natCast, Nat.cast_eq_zero]

Result:
no goals
-- Mathlib/Data/Int/Cast/Lemmas.lean
lemma AddMonoidHom.apply_int (f : ℤ →+ β) (n : ℤ) : f n = n • f 1

Proof state:
β : Type u_4
inst✝ : AddGroup β
f : ℤ →+ β
n : ℤ
⊢ f n = n • f 1

Tactic:
rw [← zmultiplesHom_symm_apply, ← zmultiplesHom_apply, Equiv.apply_symm_apply]

Result:
no goals
-- Mathlib/Combinatorics/SimpleGraph/Clique.lean
lemma IsMaximumIndepSet.isMaximalIndepSet
    [Fintype α] (s : Finset α) (M : G.IsMaximumIndepSet s) : Maximal G.IsIndepSet s

Proof state:
α : Type u_3
G : SimpleGraph α
inst✝ : Fintype α
s : Finset α
M : Gᶜ.IsMaximumClique s
⊢ Maximal Gᶜ.IsClique ↑s

Tactic:
exact IsMaximumClique.isMaximalClique s M

Result:
no goals

Proof state:
α : Type u_3
G : SimpleGraph α
inst✝ : Fintype α
s : Finset α
M : G.IsMaximumIndepSet s
⊢ Maximal G.IsIndepSet ↑s

Tactic:
rw [← isMaximalClique_compl]

Result:
α : Type u_3
G : SimpleGraph α
inst✝ : Fintype α
s : Finset α
M : G.IsMaximumIndepSet s
⊢ Maximal Gᶜ.IsClique ↑s

Proof state:
α : Type u_3
G : SimpleGraph α
inst✝ : Fintype α
s : Finset α
M : G.IsMaximumIndepSet s
⊢ Maximal Gᶜ.IsClique ↑s

Tactic:
rw [← isMaximumClique_compl] at M

Result:
α : Type u_3
G : SimpleGraph α
inst✝ : Fintype α
s : Finset α
M : Gᶜ.IsMaximumClique s
⊢ Maximal Gᶜ.IsClique ↑s
-- Mathlib/Data/Complex/Norm.lean
theorem norm_le_abs_re_add_abs_im (z : ℂ) : ‖z‖ ≤ |z.re| + |z.im|

Proof state:
z : ℂ
⊢ ‖z‖ ≤ |z.re| + |z.im|

Tactic:
simpa [re_add_im] using norm_add_le (z.re : ℂ) (z.im * I)

Result:
no goals
-- Mathlib/Algebra/MvPolynomial/Eval.lean
theorem aevalTower_ofId :
    aevalTower (Algebra.ofId S A) = (aeval : (σ → A) → MvPolynomial σ S →ₐ[S] A)

Proof state:
case h.hf
σ : Type u_1
S : Type u_2
A : Type u_3
inst✝² : CommSemiring S
inst✝¹ : CommSemiring A
inst✝ : Algebra S A
x✝ : σ → A
i✝ : σ
⊢ (aevalTower (Algebra.ofId S A) x✝) (X i✝) = (aeval x✝) (X i✝)

Tactic:
simp only [aeval_X, aevalTower_X]

Result:
no goals

Proof state:
σ : Type u_1
S : Type u_2
A : Type u_3
inst✝² : CommSemiring S
inst✝¹ : CommSemiring A
inst✝ : Algebra S A
⊢ aevalTower (Algebra.ofId S A) = aeval

Tactic:
ext

Result:
case h.hf
σ : Type u_1
S : Type u_2
A : Type u_3
inst✝² : CommSemiring S
inst✝¹ : CommSemiring A
inst✝ : Algebra S A
x✝ : σ → A
i✝ : σ
⊢ (aevalTower (Algebra.ofId S A) x✝) (X i✝) = (aeval x✝) (X i✝)
-- Mathlib/.lake/packages/lean4/src/lean/Std/Sat/CNF/Basic.lean
theorem mem_cons {v : α} : Mem v (l :: c : Clause α) ↔ (v = l.1 ∨ Mem v c)

Proof state:
case mk.true
α : Type u_1
c : List (Literal α)
v b : α
⊢ Mem v ((b, true) :: c) ↔ v = (b, true).fst ∨ Mem v c

Tactic:
simp [Mem]

Result:
case mk.true
α : Type u_1
c : List (Literal α)
v b : α
⊢ (v, false) ∈ c ∨ v = b ∨ (v, true) ∈ c ↔ v = b ∨ (v, false) ∈ c ∨ (v, true) ∈ c

Proof state:
case mk.true
α : Type u_1
c : List (Literal α)
v b : α
⊢ (v, false) ∈ c ∨ v = b ∨ (v, true) ∈ c ↔ v = b ∨ (v, false) ∈ c ∨ (v, true) ∈ c

Tactic:
rw [or_left_comm]

Result:
no goals

Proof state:
case mk.false
α : Type u_1
c : List (Literal α)
v b : α
⊢ Mem v ((b, false) :: c) ↔ v = (b, false).fst ∨ Mem v c

Tactic:
simp [Mem, or_assoc]

Result:
no goals

Proof state:
α : Type u_1
l : Literal α
c : List (Literal α)
v : α
⊢ Mem v (l :: c) ↔ v = l.fst ∨ Mem v c

Tactic:
rcases l with ⟨b, (_|_)⟩

Result:
case mk.false
α : Type u_1
c : List (Literal α)
v b : α
⊢ Mem v ((b, false) :: c) ↔ v = (b, false).fst ∨ Mem v c

case mk.true
α : Type u_1
c : List (Literal α)
v b : α
⊢ Mem v ((b, true) :: c) ↔ v = (b, true).fst ∨ Mem v c
-- Mathlib/Order/RelSeries.lean
lemma toList_chain' (x : RelSeries r) : x.toList.Chain' r

Proof state:
α : Type u_1
r : Rel α α
x : RelSeries r
i : ℕ
h : i < x.toList.length - 1
⊢ i < x.length

Tactic:
simpa [toList] using h

Result:
no goals

Proof state:
α : Type u_1
r : Rel α α
x : RelSeries r
⊢ ∀ (i : ℕ) (h : i < x.toList.length - 1), r (x.toList.get ⟨i, ⋯⟩) (x.toList.get ⟨i + 1, ⋯⟩)

Tactic:
intros i h

Result:
α : Type u_1
r : Rel α α
x : RelSeries r
i : ℕ
h : i < x.toList.length - 1
⊢ r (x.toList.get ⟨i, ⋯⟩) (x.toList.get ⟨i + 1, ⋯⟩)

Proof state:
α : Type u_1
r : Rel α α
x : RelSeries r
i : ℕ
h : i < x.toList.length - 1
⊢ r (x.toList.get ⟨i, ⋯⟩) (x.toList.get ⟨i + 1, ⋯⟩)

Tactic:
convert x.step ⟨i, by simpa [toList] using h⟩ <;> apply List.get_ofFn

Result:
no goals

Proof state:
α : Type u_1
r : Rel α α
x : RelSeries r
⊢ List.Chain' r x.toList

Tactic:
rw [List.chain'_iff_get]

Result:
α : Type u_1
r : Rel α α
x : RelSeries r
⊢ ∀ (i : ℕ) (h : i < x.toList.length - 1), r (x.toList.get ⟨i, ⋯⟩) (x.toList.get ⟨i + 1, ⋯⟩)
-- Mathlib/.lake/packages/lean4/src/lean/Std/Data/DHashMap/Internal/List/Associative.lean
theorem keys_eq_map (l : List ((a : α) × β a)) : keys l = l.map (·.1)

Proof state:
α : Type u
β : α → Type v
l : List ((a : α) × β a)
⊢ keys l = List.map (fun x => x.fst) l

Tactic:
induction l using assoc_induction <;> simp_all

Result:
no goals