harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/Topology/MetricSpace/HausdorffDistance.lean
theorem _root_.IsCompact.exists_infEdist_eq_edist (hs : IsCompact s) (hne : s.Nonempty) (x : α) :
    ∃ y ∈ s, infEdist x s = edist x y

Proof state:
case intro.intro
α : Type u
inst✝ : PseudoEMetricSpace α
s : Set α
hs : IsCompact s
hne : s.Nonempty
x : α
A : Continuous fun y => edist x y
y : α
ys : y ∈ s
hy : IsMinOn (fun y => edist x y) s y
⊢ ∃ y ∈ s, infEdist x s = edist x y

Tactic:
exact ⟨y, ys, le_antisymm (infEdist_le_edist_of_mem ys) (by rwa [le_infEdist])⟩

Result:
no goals

Proof state:
α : Type u
inst✝ : PseudoEMetricSpace α
s : Set α
hs : IsCompact s
hne : s.Nonempty
x : α
⊢ ∃ y ∈ s, infEdist x s = edist x y

Tactic:
have A : Continuous fun y => edist x y := continuous_const.edist continuous_id

Result:
α : Type u
inst✝ : PseudoEMetricSpace α
s : Set α
hs : IsCompact s
hne : s.Nonempty
x : α
A : Continuous fun y => edist x y
⊢ ∃ y ∈ s, infEdist x s = edist x y

Proof state:
α : Type u
inst✝ : PseudoEMetricSpace α
s : Set α
hs : IsCompact s
hne : s.Nonempty
x : α
A : Continuous fun y => edist x y
⊢ ∃ y ∈ s, infEdist x s = edist x y

Tactic:
obtain ⟨y, ys, hy⟩ := hs.exists_isMinOn hne A.continuousOn

Result:
case intro.intro
α : Type u
inst✝ : PseudoEMetricSpace α
s : Set α
hs : IsCompact s
hne : s.Nonempty
x : α
A : Continuous fun y => edist x y
y : α
ys : y ∈ s
hy : IsMinOn (fun y => edist x y) s y
⊢ ∃ y ∈ s, infEdist x s = edist x y

Proof state:
α : Type u
inst✝ : PseudoEMetricSpace α
s : Set α
hs : IsCompact s
hne : s.Nonempty
x : α
A : Continuous fun y => edist x y
y : α
ys : y ∈ s
hy : IsMinOn (fun y => edist x y) s y
⊢ edist x y ≤ infEdist x s

Tactic:
rwa [le_infEdist]

Result:
no goals
-- Mathlib/Analysis/SpecialFunctions/ContinuousFunctionalCalculus/Rpow/Basic.lean
@[simp]
lemma sqrt_algebraMap {r : ℝ≥0} : sqrt (algebraMap ℝ≥0 A r) = algebraMap ℝ≥0 A (NNReal.sqrt r)

Proof state:
A : Type u_1
inst✝⁷ : PartialOrder A
inst✝⁶ : Ring A
inst✝⁵ : StarRing A
inst✝⁴ : TopologicalSpace A
inst✝³ : Algebra ℝ A
inst✝² : ContinuousFunctionalCalculus ℝ≥0 fun a => 0 ≤ a
inst✝¹ : IsTopologicalRing A
inst✝ : T2Space A
r : ℝ≥0
⊢ sqrt ((algebraMap ℝ≥0 A) r) = (algebraMap ℝ≥0 A) (NNReal.sqrt r)

Tactic:
rw [sqrt_eq_cfc, cfc_algebraMap]

Result:
no goals
-- Mathlib/Combinatorics/SimpleGraph/Maps.lean
@[simp] lemma induceHom_comp :
    (induceHom ψ ψtr).comp (induceHom φ φst) = induceHom (ψ.comp φ) (ψtr.comp φst)

Proof state:
V : Type u_1
W : Type u_2
X : Type u_3
G : SimpleGraph V
G' : SimpleGraph W
G'' : SimpleGraph X
s : Set V
t : Set W
r : Set X
φ : G →g G'
φst : Set.MapsTo (⇑φ) s t
ψ : G' →g G''
ψtr : Set.MapsTo (⇑ψ) t r
⊢ (induceHom ψ ψtr).comp (induceHom φ φst) = induceHom (ψ.comp φ) ⋯

Tactic:
ext x

Result:
case h.a
V : Type u_1
W : Type u_2
X : Type u_3
G : SimpleGraph V
G' : SimpleGraph W
G'' : SimpleGraph X
s : Set V
t : Set W
r : Set X
φ : G →g G'
φst : Set.MapsTo (⇑φ) s t
ψ : G' →g G''
ψtr : Set.MapsTo (⇑ψ) t r
x : ↑s
⊢ ↑(((induceHom ψ ψtr).comp (induceHom φ φst)) x) = ↑((induceHom (ψ.comp φ) ⋯) x)

Proof state:
case h.a
V : Type u_1
W : Type u_2
X : Type u_3
G : SimpleGraph V
G' : SimpleGraph W
G'' : SimpleGraph X
s : Set V
t : Set W
r : Set X
φ : G →g G'
φst : Set.MapsTo (⇑φ) s t
ψ : G' →g G''
ψtr : Set.MapsTo (⇑ψ) t r
x : ↑s
⊢ ↑(((induceHom ψ ψtr).comp (induceHom φ φst)) x) = ↑((induceHom (ψ.comp φ) ⋯) x)

Tactic:
rfl

Result:
no goals
-- Mathlib/Geometry/RingedSpace/OpenImmersion.lean
theorem inv_invApp (U : Opens X) :
    inv (H.invApp _ U) =
      f.c.app (op (opensFunctor f |>.obj U)) ≫ X.presheaf.map
        (eqToHom (by simp [Opens.map, Set.preimage_image_eq _ H.base_open.injective])) :=
  PresheafedSpace.IsOpenImmersion.inv_invApp f.1 U

Proof state:
C : Type u
inst✝ : Category.{v, u} C
X Y : LocallyRingedSpace
f : X ⟶ Y
H : IsOpenImmersion f
U : Opens ↑X.toTopCat
⊢ (Opens.map f.base).op.obj (op ((opensFunctor f).obj U)) = op U

Tactic:
simp [Opens.map, Set.preimage_image_eq _ H.base_open.injective]

Result:
no goals
-- Mathlib/CategoryTheory/Subterminal.lean
theorem IsSubterminal.isIso_diag (hA : IsSubterminal A) [HasBinaryProduct A A] : IsIso (diag A) :=
  ⟨⟨Limits.prod.fst,
      ⟨by simp, by
        rw [IsSubterminal.def] at hA
        aesop_cat⟩⟩⟩

Proof state:
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
A : C
hA : IsSubterminal A
inst✝ : HasBinaryProduct A A
⊢ diag A ≫ prod.fst = 𝟙 A

Tactic:
simp

Result:
no goals

Proof state:
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
A : C
hA : IsSubterminal A
inst✝ : HasBinaryProduct A A
⊢ prod.fst ≫ diag A = 𝟙 (A ⨯ A)

Tactic:
rw [IsSubterminal.def] at hA

Result:
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
A : C
hA : ∀ ⦃Z : C⦄ (f g : Z ⟶ A), f = g
inst✝ : HasBinaryProduct A A
⊢ prod.fst ≫ diag A = 𝟙 (A ⨯ A)

Proof state:
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
A : C
hA : ∀ ⦃Z : C⦄ (f g : Z ⟶ A), f = g
inst✝ : HasBinaryProduct A A
⊢ prod.fst ≫ diag A = 𝟙 (A ⨯ A)

Tactic:
aesop_cat

Result:
no goals
-- Mathlib/RingTheory/Localization/FractionRing.lean
theorem ringHom_fieldRange_eq_of_comp_eq_of_range_eq (h : RingHom.comp f (algebraMap A K) = g)
    {s : Set L} (hs : g.range = Subring.closure s) : f.fieldRange = Subfield.closure s

Proof state:
case h
A : Type u_4
inst✝⁴ : CommRing A
K : Type u_5
inst✝³ : Field K
inst✝² : Algebra A K
inst✝¹ : IsFractionRing A K
L : Type u_8
inst✝ : Field L
g : A →+* L
f : K →+* L
h : f.comp (algebraMap A K) = g
s : Set L
hs : g.range = Subring.closure s
x✝ : L
⊢ x✝ ∈ Subfield.closure ↑(Subring.closure s) ↔ x✝ ∈ Subfield.closure s

Tactic:
simp_rw [Subfield.mem_closure_iff, Subring.closure_eq]

Result:
no goals

Proof state:
A : Type u_4
inst✝⁴ : CommRing A
K : Type u_5
inst✝³ : Field K
inst✝² : Algebra A K
inst✝¹ : IsFractionRing A K
L : Type u_8
inst✝ : Field L
g : A →+* L
f : K →+* L
h : f.comp (algebraMap A K) = g
s : Set L
hs : g.range = Subring.closure s
⊢ Subfield.closure ↑(Subring.closure s) = Subfield.closure s

Tactic:
ext

Result:
case h
A : Type u_4
inst✝⁴ : CommRing A
K : Type u_5
inst✝³ : Field K
inst✝² : Algebra A K
inst✝¹ : IsFractionRing A K
L : Type u_8
inst✝ : Field L
g : A →+* L
f : K →+* L
h : f.comp (algebraMap A K) = g
s : Set L
hs : g.range = Subring.closure s
x✝ : L
⊢ x✝ ∈ Subfield.closure ↑(Subring.closure s) ↔ x✝ ∈ Subfield.closure s

Proof state:
A : Type u_4
inst✝⁴ : CommRing A
K : Type u_5
inst✝³ : Field K
inst✝² : Algebra A K
inst✝¹ : IsFractionRing A K
L : Type u_8
inst✝ : Field L
g : A →+* L
f : K →+* L
h : f.comp (algebraMap A K) = g
s : Set L
hs : g.range = Subring.closure s
⊢ f.fieldRange = Subfield.closure s

Tactic:
rw [ringHom_fieldRange_eq_of_comp_eq h, hs]

Result:
A : Type u_4
inst✝⁴ : CommRing A
K : Type u_5
inst✝³ : Field K
inst✝² : Algebra A K
inst✝¹ : IsFractionRing A K
L : Type u_8
inst✝ : Field L
g : A →+* L
f : K →+* L
h : f.comp (algebraMap A K) = g
s : Set L
hs : g.range = Subring.closure s
⊢ Subfield.closure ↑(Subring.closure s) = Subfield.closure s
-- Mathlib/MeasureTheory/Measure/Typeclasses.lean
theorem exists_subset_measure_lt_top [SigmaFinite μ] {r : ℝ≥0∞} (hs : MeasurableSet s)
    (h's : r < μ s) : ∃ t, MeasurableSet t ∧ t ⊆ s ∧ r < μ t ∧ μ t < ∞

Proof state:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
s : Set α
inst✝ : SigmaFinite μ
r : ℝ≥0∞
hs : MeasurableSet s
h's : r < μ s
⊢ ∃ t, MeasurableSet t ∧ t ⊆ s ∧ r < μ t ∧ μ t < ⊤

Tactic:
rw [← iSup_restrict_spanningSets,
  @lt_iSup_iff _ _ _ r fun i : ℕ => μ.restrict (spanningSets μ i) s] at h's

Result:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
s : Set α
inst✝ : SigmaFinite μ
r : ℝ≥0∞
hs : MeasurableSet s
h's : ∃ i, r < (μ.restrict (spanningSets μ i)) s
⊢ ∃ t, MeasurableSet t ∧ t ⊆ s ∧ r < μ t ∧ μ t < ⊤

Proof state:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
s : Set α
inst✝ : SigmaFinite μ
r : ℝ≥0∞
hs : MeasurableSet s
h's : ∃ i, r < (μ.restrict (spanningSets μ i)) s
⊢ ∃ t, MeasurableSet t ∧ t ⊆ s ∧ r < μ t ∧ μ t < ⊤

Tactic:
rcases h's with ⟨n, hn⟩

Result:
case intro
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
s : Set α
inst✝ : SigmaFinite μ
r : ℝ≥0∞
hs : MeasurableSet s
n : ℕ
hn : r < (μ.restrict (spanningSets μ n)) s
⊢ ∃ t, MeasurableSet t ∧ t ⊆ s ∧ r < μ t ∧ μ t < ⊤

Proof state:
case intro
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
s : Set α
inst✝ : SigmaFinite μ
r : ℝ≥0∞
hs : MeasurableSet s
n : ℕ
hn : r < μ (s ∩ spanningSets μ n)
⊢ ∃ t, MeasurableSet t ∧ t ⊆ s ∧ r < μ t ∧ μ t < ⊤

Tactic:
refine
  ⟨s ∩ spanningSets μ n, hs.inter (measurableSet_spanningSets _ _), inter_subset_left, hn, ?_⟩

Result:
case intro
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
s : Set α
inst✝ : SigmaFinite μ
r : ℝ≥0∞
hs : MeasurableSet s
n : ℕ
hn : r < μ (s ∩ spanningSets μ n)
⊢ μ (s ∩ spanningSets μ n) < ⊤

Proof state:
case intro
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
s : Set α
inst✝ : SigmaFinite μ
r : ℝ≥0∞
hs : MeasurableSet s
n : ℕ
hn : r < (μ.restrict (spanningSets μ n)) s
⊢ ∃ t, MeasurableSet t ∧ t ⊆ s ∧ r < μ t ∧ μ t < ⊤

Tactic:
simp only [restrict_apply hs] at hn

Result:
case intro
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
s : Set α
inst✝ : SigmaFinite μ
r : ℝ≥0∞
hs : MeasurableSet s
n : ℕ
hn : r < μ (s ∩ spanningSets μ n)
⊢ ∃ t, MeasurableSet t ∧ t ⊆ s ∧ r < μ t ∧ μ t < ⊤

Proof state:
case intro
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
s : Set α
inst✝ : SigmaFinite μ
r : ℝ≥0∞
hs : MeasurableSet s
n : ℕ
hn : r < μ (s ∩ spanningSets μ n)
⊢ μ (s ∩ spanningSets μ n) < ⊤

Tactic:
exact (measure_mono inter_subset_right).trans_lt (measure_spanningSets_lt_top _ _)

Result:
no goals
-- Mathlib/Probability/Kernel/Disintegration/Integral.lean
lemma setIntegral_condKernel_univ_right {s : Set β} (hs : MeasurableSet s)
    (hf : IntegrableOn f (s ×ˢ Set.univ) ρ) :
    ∫ b in s, ∫ ω, f (b, ω) ∂(ρ.condKernel b) ∂ρ.fst = ∫ x in s ×ˢ Set.univ, f x ∂ρ

Proof state:
β : Type u_1
Ω : Type u_2
mβ : MeasurableSpace β
inst✝⁵ : MeasurableSpace Ω
inst✝⁴ : StandardBorelSpace Ω
inst✝³ : Nonempty Ω
ρ : Measure (β × Ω)
inst✝² : IsFiniteMeasure ρ
E : Type u_3
f : β × Ω → E
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
s : Set β
hs : MeasurableSet s
hf : IntegrableOn f (s ×ˢ Set.univ) ρ
⊢ ∫ (b : β) in s, ∫ (ω : Ω), f (b, ω) ∂ρ.condKernel b ∂ρ.fst = ∫ (x : β × Ω) in s ×ˢ Set.univ, f x ∂ρ

Tactic:
rw [← setIntegral_condKernel hs MeasurableSet.univ hf]

Result:
β : Type u_1
Ω : Type u_2
mβ : MeasurableSpace β
inst✝⁵ : MeasurableSpace Ω
inst✝⁴ : StandardBorelSpace Ω
inst✝³ : Nonempty Ω
ρ : Measure (β × Ω)
inst✝² : IsFiniteMeasure ρ
E : Type u_3
f : β × Ω → E
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
s : Set β
hs : MeasurableSet s
hf : IntegrableOn f (s ×ˢ Set.univ) ρ
⊢ ∫ (b : β) in s, ∫ (ω : Ω), f (b, ω) ∂ρ.condKernel b ∂ρ.fst =
    ∫ (b : β) in s, ∫ (ω : Ω) in Set.univ, f (b, ω) ∂ρ.condKernel b ∂ρ.fst

Proof state:
β : Type u_1
Ω : Type u_2
mβ : MeasurableSpace β
inst✝⁵ : MeasurableSpace Ω
inst✝⁴ : StandardBorelSpace Ω
inst✝³ : Nonempty Ω
ρ : Measure (β × Ω)
inst✝² : IsFiniteMeasure ρ
E : Type u_3
f : β × Ω → E
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
s : Set β
hs : MeasurableSet s
hf : IntegrableOn f (s ×ˢ Set.univ) ρ
⊢ ∫ (b : β) in s, ∫ (ω : Ω), f (b, ω) ∂ρ.condKernel b ∂ρ.fst =
    ∫ (b : β) in s, ∫ (ω : Ω) in Set.univ, f (b, ω) ∂ρ.condKernel b ∂ρ.fst

Tactic:
simp_rw [Measure.restrict_univ]

Result:
no goals
-- Mathlib/Algebra/Polynomial/FieldDivision.lean
theorem map_div [Field k] (f : R →+* k) : (p / q).map f = p.map f / q.map f

Proof state:
R : Type u
k : Type y
inst✝¹ : Field R
p q : R[X]
inst✝ : Field k
f : R →+* k
hq0 : q = 0
⊢ map f (p / q) = map f p / map f q

Tactic:
simp [hq0]

Result:
no goals

Proof state:
R : Type u
k : Type y
inst✝¹ : Field R
p q : R[X]
inst✝ : Field k
f : R →+* k
hq0 : ¬q = 0
⊢ map f (p / q) = map f p / map f q

Tactic:
rw [div_def, div_def, Polynomial.map_mul, map_divByMonic f (monic_mul_leadingCoeff_inv hq0),
  Polynomial.map_mul, map_C, leadingCoeff_map, map_inv₀]

Result:
no goals

Proof state:
R : Type u
k : Type y
inst✝¹ : Field R
p q : R[X]
inst✝ : Field k
f : R →+* k
⊢ map f (p / q) = map f p / map f q

Tactic:
if hq0 : q = 0 then simp [hq0]
else
  rw [div_def, div_def, Polynomial.map_mul, map_divByMonic f (monic_mul_leadingCoeff_inv hq0),
    Polynomial.map_mul, map_C, leadingCoeff_map, map_inv₀]

Result:
no goals
-- Mathlib/SetTheory/Nimber/Basic.lean
theorem add_zero (a : Nimber) : a + 0 = a

Proof state:
case a.h₁
a a' : Nimber
ha : a' < a
⊢ a' ≠ a

Tactic:
exact ha.ne

Result:
no goals

Proof state:
case a.h₁
a : Nimber
⊢ ∀ a' < a, a' + 0 ≠ a

Tactic:
intro a' ha

Result:
case a.h₁
a a' : Nimber
ha : a' < a
⊢ a' + 0 ≠ a

Proof state:
case a
a : Nimber
h : a + 0 < a
⊢ False

Tactic:
have := Nimber.add_zero (a + 0)

Result:
case a
a : Nimber
h : a + 0 < a
this : a + 0 + 0 = a + 0
⊢ False

Proof state:
case a
a : Nimber
⊢ a + 0 ≤ a

Tactic:
apply add_le_of_forall_ne

Result:
case a.h₁
a : Nimber
⊢ ∀ a' < a, a' + 0 ≠ a

case a.h₂
a : Nimber
⊢ ∀ b' < 0, a + b' ≠ a

Proof state:
case a
a : Nimber
h : a + 0 < a
this : a + 0 + 0 = a + 0
⊢ False

Tactic:
rw [add_left_inj] at this

Result:
case a
a : Nimber
h : a + 0 < a
this : a + 0 = a
⊢ False

Proof state:
case a.h₁
a a' : Nimber
ha : a' < a
⊢ a' + 0 ≠ a

Tactic:
rw [Nimber.add_zero]

Result:
case a.h₁
a a' : Nimber
ha : a' < a
⊢ a' ≠ a

Proof state:
case a
a : Nimber
h : a + 0 < a
this : a + 0 = a
⊢ False

Tactic:
exact this.not_lt h

Result:
no goals

Proof state:
a : Nimber
⊢ a + 0 = a

Tactic:
apply le_antisymm

Result:
case a
a : Nimber
⊢ a + 0 ≤ a

case a
a : Nimber
⊢ a ≤ a + 0

Proof state:
case a.h₂
a : Nimber
⊢ ∀ b' < 0, a + b' ≠ a

Tactic:
intro _ h

Result:
case a.h₂
a b'✝ : Nimber
h : b'✝ < 0
⊢ a + b'✝ ≠ a

Proof state:
case a
a : Nimber
⊢ a ≤ a + 0

Tactic:
by_contra! h

Result:
case a
a : Nimber
h : a + 0 < a
⊢ False

Proof state:
case a.h₂
a b'✝ : Nimber
h : b'✝ < 0
⊢ a + b'✝ ≠ a

Tactic:
exact (Nimber.not_lt_zero _ h).elim

Result:
no goals
-- Mathlib/Data/Num/Lemmas.lean
theorem size_eq_natSize : ∀ n, (size n : ℕ) = natSize n
  | 1 => rfl
  | bit0 n => by rw [size, succ_to_nat, natSize, size_eq_natSize n]
  | bit1 n => by rw [size, succ_to_nat, natSize, size_eq_natSize n]

Proof state:
n : PosNum
⊢ ↑n.bit0.size = n.bit0.natSize

Tactic:
rw [size, succ_to_nat, natSize, size_eq_natSize n]

Result:
no goals

Proof state:
n : PosNum
⊢ ↑n.bit1.size = n.bit1.natSize

Tactic:
rw [size, succ_to_nat, natSize, size_eq_natSize n]

Result:
no goals
-- Mathlib/Data/Set/Lattice.lean
theorem surjOn_iInter [Nonempty ι] {s : ι → Set α} {t : Set β} {f : α → β}
    (H : ∀ i, SurjOn f (s i) t) (Hinj : InjOn f (⋃ i, s i)) : SurjOn f (⋂ i, s i) t

Proof state:
α : Type u_1
β : Type u_2
ι : Sort u_5
inst✝ : Nonempty ι
s : ι → Set α
t : Set β
f : α → β
H : ∀ (i : ι), SurjOn f (s i) t
Hinj : InjOn f (⋃ i, s i)
y : β
hy : y ∈ t
⊢ y ∈ f '' ⋂ i, s i

Tactic:
rw [Hinj.image_iInter_eq, mem_iInter]

Result:
α : Type u_1
β : Type u_2
ι : Sort u_5
inst✝ : Nonempty ι
s : ι → Set α
t : Set β
f : α → β
H : ∀ (i : ι), SurjOn f (s i) t
Hinj : InjOn f (⋃ i, s i)
y : β
hy : y ∈ t
⊢ ∀ (i : ι), y ∈ f '' s i

Proof state:
α : Type u_1
β : Type u_2
ι : Sort u_5
inst✝ : Nonempty ι
s : ι → Set α
t : Set β
f : α → β
H : ∀ (i : ι), SurjOn f (s i) t
Hinj : InjOn f (⋃ i, s i)
y : β
hy : y ∈ t
⊢ ∀ (i : ι), y ∈ f '' s i

Tactic:
exact fun i => H i hy

Result:
no goals

Proof state:
α : Type u_1
β : Type u_2
ι : Sort u_5
inst✝ : Nonempty ι
s : ι → Set α
t : Set β
f : α → β
H : ∀ (i : ι), SurjOn f (s i) t
Hinj : InjOn f (⋃ i, s i)
⊢ SurjOn f (⋂ i, s i) t

Tactic:
intro y hy

Result:
α : Type u_1
β : Type u_2
ι : Sort u_5
inst✝ : Nonempty ι
s : ι → Set α
t : Set β
f : α → β
H : ∀ (i : ι), SurjOn f (s i) t
Hinj : InjOn f (⋃ i, s i)
y : β
hy : y ∈ t
⊢ y ∈ f '' ⋂ i, s i
-- Mathlib/RingTheory/Ideal/Norm/AbsNorm.lean
theorem absNorm_eq_one_iff {I : Ideal S} : absNorm I = 1 ↔ I = ⊤

Proof state:
S : Type u_1
inst✝³ : CommRing S
inst✝² : Nontrivial S
inst✝¹ : IsDedekindDomain S
inst✝ : Module.Free ℤ S
I : Ideal S
⊢ absNorm I = 1 ↔ I = ⊤

Tactic:
rw [absNorm_apply, cardQuot_eq_one_iff]

Result:
no goals
-- Mathlib/ModelTheory/Definability.lean
theorem Definable.mono (hAs : A.Definable L s) (hAB : A ⊆ B) : B.Definable L s

Proof state:
M : Type w
A : Set M
L : Language
inst✝ : L.Structure M
α : Type u₁
B : Set M
s : Set (α → M)
hAs : A.Definable L s
hAB : A ⊆ B
⊢ B.Definable L s

Tactic:
rw [definable_iff_empty_definable_with_params] at *

Result:
M : Type w
A : Set M
L : Language
inst✝ : L.Structure M
α : Type u₁
B : Set M
s : Set (α → M)
hAs : ∅.Definable (L[[↑A]]) s
hAB : A ⊆ B
⊢ ∅.Definable (L[[↑B]]) s

Proof state:
M : Type w
A : Set M
L : Language
inst✝ : L.Structure M
α : Type u₁
B : Set M
s : Set (α → M)
hAs : ∅.Definable (L[[↑A]]) s
hAB : A ⊆ B
⊢ ∅.Definable (L[[↑B]]) s

Tactic:
exact hAs.map_expansion (L.lhomWithConstantsMap (Set.inclusion hAB))

Result:
no goals
-- Mathlib/Data/Nat/Factorization/Defs.lean
theorem factorization_eq_zero_of_non_prime (n : ℕ) {p : ℕ} (hp : ¬p.Prime) :
    n.factorization p = 0

Proof state:
n p : ℕ
hp : ¬Prime p
⊢ n.factorization p = 0

Tactic:
simp [factorization_eq_zero_iff, hp]

Result:
no goals
-- Mathlib/Topology/UniformSpace/Defs.lean
theorem nhds_basis_uniformity {p : ι → Prop} {s : ι → Set (α × α)} (h : (𝓤 α).HasBasis p s)
    {x : α} : (𝓝 x).HasBasis p fun i => { y | (y, x) ∈ s i }

Proof state:
α : Type ua
ι : Sort u_1
inst✝ : UniformSpace α
p : ι → Prop
s : ι → Set (α × α)
h : (𝓤 α).HasBasis p s
x : α
⊢ (𝓝 x).HasBasis p fun i => {y | (y, x) ∈ s i}

Tactic:
replace h := h.comap Prod.swap

Result:
α : Type ua
ι : Sort u_1
inst✝ : UniformSpace α
p : ι → Prop
s : ι → Set (α × α)
x : α
h : (comap Prod.swap (𝓤 α)).HasBasis p fun i => Prod.swap ⁻¹' s i
⊢ (𝓝 x).HasBasis p fun i => {y | (y, x) ∈ s i}

Proof state:
α : Type ua
ι : Sort u_1
inst✝ : UniformSpace α
p : ι → Prop
s : ι → Set (α × α)
x : α
h : (comap Prod.swap (𝓤 α)).HasBasis p fun i => Prod.swap ⁻¹' s i
⊢ (𝓝 x).HasBasis p fun i => {y | (y, x) ∈ s i}

Tactic:
rw [comap_swap_uniformity] at h

Result:
α : Type ua
ι : Sort u_1
inst✝ : UniformSpace α
p : ι → Prop
s : ι → Set (α × α)
x : α
h : (𝓤 α).HasBasis p fun i => Prod.swap ⁻¹' s i
⊢ (𝓝 x).HasBasis p fun i => {y | (y, x) ∈ s i}

Proof state:
α : Type ua
ι : Sort u_1
inst✝ : UniformSpace α
p : ι → Prop
s : ι → Set (α × α)
x : α
h : (𝓤 α).HasBasis p fun i => Prod.swap ⁻¹' s i
⊢ (𝓝 x).HasBasis p fun i => {y | (y, x) ∈ s i}

Tactic:
exact nhds_basis_uniformity' h

Result:
no goals
-- Mathlib/Algebra/Order/Ring/Defs.lean
lemma one_add_le_one_add_mul_one_sub (h : a + c + b * c ≤ b) : 1 + a ≤ (1 + b) * (1 - c)

Proof state:
α : Type u
inst✝ : OrderedRing α
a b c : α
h : a + c + b * c ≤ b
⊢ 1 + a ≤ (1 + b) * (1 - c)

Tactic:
rw [mul_one_sub, one_add_mul, le_sub_iff_add_le, add_assoc, ← add_assoc a]

Result:
α : Type u
inst✝ : OrderedRing α
a b c : α
h : a + c + b * c ≤ b
⊢ 1 + (a + c + b * c) ≤ 1 + b

Proof state:
α : Type u
inst✝ : OrderedRing α
a b c : α
h : a + c + b * c ≤ b
⊢ 1 + (a + c + b * c) ≤ 1 + b

Tactic:
gcongr

Result:
no goals
-- Mathlib/Topology/UniformSpace/Cauchy.lean
theorem le_nhds_of_cauchy_adhp_aux {f : Filter α} {x : α}
    (adhs : ∀ s ∈ 𝓤 α, ∃ t ∈ f, t ×ˢ t ⊆ s ∧ ∃ y, (x, y) ∈ s ∧ y ∈ t) : f ≤ 𝓝 x

Proof state:
case intro.intro.intro.intro.intro.intro.intro
α : Type u
uniformSpace : UniformSpace α
f : Filter α
x : α
adhs : ∀ s ∈ 𝓤 α, ∃ t ∈ f, t ×ˢ t ⊆ s ∧ ∃ y, (x, y) ∈ s ∧ y ∈ t
s : Set α
hs : s ∈ 𝓝 x
U : Set (α × α)
U_mem : U ∈ 𝓤 α
hU : U ○ U ⊆ {p | p.1 = x → p.2 ∈ s}
t : Set α
t_mem : t ∈ f
ht : t ×ˢ t ⊆ U
y : α
hxy : (x, y) ∈ U
hy : y ∈ t
⊢ s ∈ f

Tactic:
apply mem_of_superset t_mem

Result:
case intro.intro.intro.intro.intro.intro.intro
α : Type u
uniformSpace : UniformSpace α
f : Filter α
x : α
adhs : ∀ s ∈ 𝓤 α, ∃ t ∈ f, t ×ˢ t ⊆ s ∧ ∃ y, (x, y) ∈ s ∧ y ∈ t
s : Set α
hs : s ∈ 𝓝 x
U : Set (α × α)
U_mem : U ∈ 𝓤 α
hU : U ○ U ⊆ {p | p.1 = x → p.2 ∈ s}
t : Set α
t_mem : t ∈ f
ht : t ×ˢ t ⊆ U
y : α
hxy : (x, y) ∈ U
hy : y ∈ t
⊢ t ⊆ s

Proof state:
α : Type u
uniformSpace : UniformSpace α
f : Filter α
x : α
adhs : ∀ s ∈ 𝓤 α, ∃ t ∈ f, t ×ˢ t ⊆ s ∧ ∃ y, (x, y) ∈ s ∧ y ∈ t
⊢ f ≤ 𝓝 x

Tactic:
intro s hs

Result:
α : Type u
uniformSpace : UniformSpace α
f : Filter α
x : α
adhs : ∀ s ∈ 𝓤 α, ∃ t ∈ f, t ×ˢ t ⊆ s ∧ ∃ y, (x, y) ∈ s ∧ y ∈ t
s : Set α
hs : s ∈ 𝓝 x
⊢ s ∈ f

Proof state:
α : Type u
uniformSpace : UniformSpace α
f : Filter α
x : α
adhs : ∀ s ∈ 𝓤 α, ∃ t ∈ f, t ×ˢ t ⊆ s ∧ ∃ y, (x, y) ∈ s ∧ y ∈ t
s : Set α
hs : s ∈ 𝓝 x
⊢ s ∈ f

Tactic:
rcases comp_mem_uniformity_sets (mem_nhds_uniformity_iff_right.1 hs) with ⟨U, U_mem, hU⟩

Result:
case intro.intro
α : Type u
uniformSpace : UniformSpace α
f : Filter α
x : α
adhs : ∀ s ∈ 𝓤 α, ∃ t ∈ f, t ×ˢ t ⊆ s ∧ ∃ y, (x, y) ∈ s ∧ y ∈ t
s : Set α
hs : s ∈ 𝓝 x
U : Set (α × α)
U_mem : U ∈ 𝓤 α
hU : U ○ U ⊆ {p | p.1 = x → p.2 ∈ s}
⊢ s ∈ f

Proof state:
case intro.intro
α : Type u
uniformSpace : UniformSpace α
f : Filter α
x : α
adhs : ∀ s ∈ 𝓤 α, ∃ t ∈ f, t ×ˢ t ⊆ s ∧ ∃ y, (x, y) ∈ s ∧ y ∈ t
s : Set α
hs : s ∈ 𝓝 x
U : Set (α × α)
U_mem : U ∈ 𝓤 α
hU : U ○ U ⊆ {p | p.1 = x → p.2 ∈ s}
⊢ s ∈ f

Tactic:
rcases adhs U U_mem with ⟨t, t_mem, ht, y, hxy, hy⟩

Result:
case intro.intro.intro.intro.intro.intro.intro
α : Type u
uniformSpace : UniformSpace α
f : Filter α
x : α
adhs : ∀ s ∈ 𝓤 α, ∃ t ∈ f, t ×ˢ t ⊆ s ∧ ∃ y, (x, y) ∈ s ∧ y ∈ t
s : Set α
hs : s ∈ 𝓝 x
U : Set (α × α)
U_mem : U ∈ 𝓤 α
hU : U ○ U ⊆ {p | p.1 = x → p.2 ∈ s}
t : Set α
t_mem : t ∈ f
ht : t ×ˢ t ⊆ U
y : α
hxy : (x, y) ∈ U
hy : y ∈ t
⊢ s ∈ f

Proof state:
case intro.intro.intro.intro.intro.intro.intro
α : Type u
uniformSpace : UniformSpace α
f : Filter α
x : α
adhs : ∀ s ∈ 𝓤 α, ∃ t ∈ f, t ×ˢ t ⊆ s ∧ ∃ y, (x, y) ∈ s ∧ y ∈ t
s : Set α
hs : s ∈ 𝓝 x
U : Set (α × α)
U_mem : U ∈ 𝓤 α
hU : U ○ U ⊆ {p | p.1 = x → p.2 ∈ s}
t : Set α
t_mem : t ∈ f
ht : t ×ˢ t ⊆ U
y : α
hxy : (x, y) ∈ U
hy : y ∈ t
⊢ t ⊆ s

Tactic:
exact fun z hz => hU (prod_mk_mem_compRel hxy (ht <| mk_mem_prod hy hz)) rfl

Result:
no goals
-- Mathlib/GroupTheory/OrderOfElement.lean
theorem IsOfFinOrder.apply {η : Type*} {Gs : η → Type*} [∀ i, Monoid (Gs i)] {x : ∀ i, Gs i}
    (h : IsOfFinOrder x) : ∀ i, IsOfFinOrder (x i)

Proof state:
case intro.intro
η : Type u_6
Gs : η → Type u_7
inst✝ : (i : η) → Monoid (Gs i)
x : (i : η) → Gs i
h : IsOfFinOrder x
n : ℕ
npos : 0 < n
hn : x ^ n = 1
⊢ ∀ (i : η), IsOfFinOrder (x i)

Tactic:
exact fun _ => isOfFinOrder_iff_pow_eq_one.mpr ⟨n, npos, (congr_fun hn.symm _).symm⟩

Result:
no goals

Proof state:
η : Type u_6
Gs : η → Type u_7
inst✝ : (i : η) → Monoid (Gs i)
x : (i : η) → Gs i
h : IsOfFinOrder x
⊢ ∀ (i : η), IsOfFinOrder (x i)

Tactic:
obtain ⟨n, npos, hn⟩ := h.exists_pow_eq_one

Result:
case intro.intro
η : Type u_6
Gs : η → Type u_7
inst✝ : (i : η) → Monoid (Gs i)
x : (i : η) → Gs i
h : IsOfFinOrder x
n : ℕ
npos : 0 < n
hn : x ^ n = 1
⊢ ∀ (i : η), IsOfFinOrder (x i)
-- Mathlib/Algebra/BigOperators/Group/List/Basic.lean
theorem _root_.Commute.list_prod_right (l : List M) (y : M) (h : ∀ x ∈ l, Commute y x) :
    Commute y l.prod

Proof state:
case cons
M : Type u_4
inst✝ : Monoid M
y z : M
l : List M
IH : (∀ (x : M), x ∈ l → Commute y x) → Commute y l.prod
h : Commute y z ∧ ∀ (x : M), x ∈ l → Commute y x
⊢ Commute y (z :: l).prod

Tactic:
rw [List.prod_cons]

Result:
case cons
M : Type u_4
inst✝ : Monoid M
y z : M
l : List M
IH : (∀ (x : M), x ∈ l → Commute y x) → Commute y l.prod
h : Commute y z ∧ ∀ (x : M), x ∈ l → Commute y x
⊢ Commute y (z * l.prod)

Proof state:
case cons
M : Type u_4
inst✝ : Monoid M
y z : M
l : List M
IH : (∀ (x : M), x ∈ l → Commute y x) → Commute y l.prod
h : ∀ (x : M), x ∈ z :: l → Commute y x
⊢ Commute y (z :: l).prod

Tactic:
rw [List.forall_mem_cons] at h

Result:
case cons
M : Type u_4
inst✝ : Monoid M
y z : M
l : List M
IH : (∀ (x : M), x ∈ l → Commute y x) → Commute y l.prod
h : Commute y z ∧ ∀ (x : M), x ∈ l → Commute y x
⊢ Commute y (z :: l).prod

Proof state:
case nil
M : Type u_4
inst✝ : Monoid M
y : M
h : ∀ (x : M), x ∈ [] → Commute y x
⊢ Commute y [].prod

Tactic:
simp

Result:
no goals

Proof state:
M : Type u_4
inst✝ : Monoid M
l : List M
y : M
h : ∀ (x : M), x ∈ l → Commute y x
⊢ Commute y l.prod

Tactic:
induction l with
| nil => simp
| cons z l IH =>
  rw [List.forall_mem_cons] at h
  rw [List.prod_cons]
  exact Commute.mul_right h.1 (IH h.2)

Result:
no goals

Proof state:
case cons
M : Type u_4
inst✝ : Monoid M
y z : M
l : List M
IH : (∀ (x : M), x ∈ l → Commute y x) → Commute y l.prod
h : Commute y z ∧ ∀ (x : M), x ∈ l → Commute y x
⊢ Commute y (z * l.prod)

Tactic:
exact Commute.mul_right h.1 (IH h.2)

Result:
no goals