harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/RingTheory/DedekindDomain/Ideal.lean
theorem inv_anti_mono (hI : I ≠ 0) (hJ : J ≠ 0) (hIJ : I ≤ J) : J⁻¹ ≤ I⁻¹

Proof state:
K : Type u_3
inst✝⁴ : Field K
R₁ : Type u_4
inst✝³ : CommRing R₁
inst✝² : IsDomain R₁
inst✝¹ : Algebra R₁ K
inst✝ : IsFractionRing R₁ K
I J : FractionalIdeal R₁⁰ K
hI : I ≠ 0
hJ : J ≠ 0
hIJ : I ≤ J
⊢ J⁻¹ ≤ I⁻¹

Tactic:
intro x

Result:
K : Type u_3
inst✝⁴ : Field K
R₁ : Type u_4
inst✝³ : CommRing R₁
inst✝² : IsDomain R₁
inst✝¹ : Algebra R₁ K
inst✝ : IsFractionRing R₁ K
I J : FractionalIdeal R₁⁰ K
hI : I ≠ 0
hJ : J ≠ 0
hIJ : I ≤ J
x : K
⊢ x ∈ (fun a => ↑a) J⁻¹ → x ∈ (fun a => ↑a) I⁻¹

Proof state:
K : Type u_3
inst✝⁴ : Field K
R₁ : Type u_4
inst✝³ : CommRing R₁
inst✝² : IsDomain R₁
inst✝¹ : Algebra R₁ K
inst✝ : IsFractionRing R₁ K
I J : FractionalIdeal R₁⁰ K
hI : I ≠ 0
hJ : J ≠ 0
hIJ : I ≤ J
x : K
⊢ (∀ y ∈ J, x * y ∈ 1) → ∀ y ∈ I, x * y ∈ 1

Tactic:
exact fun h y hy => h y (hIJ hy)

Result:
no goals

Proof state:
K : Type u_3
inst✝⁴ : Field K
R₁ : Type u_4
inst✝³ : CommRing R₁
inst✝² : IsDomain R₁
inst✝¹ : Algebra R₁ K
inst✝ : IsFractionRing R₁ K
I J : FractionalIdeal R₁⁰ K
hI : I ≠ 0
hJ : J ≠ 0
hIJ : I ≤ J
x : K
⊢ x ∈ (fun a => ↑a) J⁻¹ → x ∈ (fun a => ↑a) I⁻¹

Tactic:
simp only [val_eq_coe, mem_coe, mem_inv_iff hJ, mem_inv_iff hI]

Result:
K : Type u_3
inst✝⁴ : Field K
R₁ : Type u_4
inst✝³ : CommRing R₁
inst✝² : IsDomain R₁
inst✝¹ : Algebra R₁ K
inst✝ : IsFractionRing R₁ K
I J : FractionalIdeal R₁⁰ K
hI : I ≠ 0
hJ : J ≠ 0
hIJ : I ≤ J
x : K
⊢ (∀ y ∈ J, x * y ∈ 1) → ∀ y ∈ I, x * y ∈ 1
-- Mathlib/Algebra/Field/Subfield/Basic.lean
theorem mem_closure_iff {s : Set K} {x} :
    x ∈ closure s ↔ ∃ y ∈ Subring.closure s, ∃ z ∈ Subring.closure s, y / z = x

Proof state:
K : Type u
inst✝ : Field K
s : Set K
x : K
⊢ x ∈ Subfield.commClosure s ↔ ∃ y ∈ Subring.closure s, ∃ z ∈ Subring.closure s, y / z = x

Tactic:
rfl

Result:
no goals

Proof state:
K : Type u
inst✝ : Field K
s : Set K
x : K
⊢ x ∈ closure s ↔ ∃ y ∈ Subring.closure s, ∃ z ∈ Subring.closure s, y / z = x

Tactic:
rw [← commClosure_eq_closure]

Result:
K : Type u
inst✝ : Field K
s : Set K
x : K
⊢ x ∈ Subfield.commClosure s ↔ ∃ y ∈ Subring.closure s, ∃ z ∈ Subring.closure s, y / z = x
-- Mathlib/Data/Finset/Lattice/Fold.lean
theorem sup_le_iff {a : α} : s.sup f ≤ a ↔ ∀ b ∈ s, f b ≤ a

Proof state:
α : Type u_2
β : Type u_3
inst✝¹ : SemilatticeSup α
inst✝ : OrderBot α
s : Finset β
f : β → α
a : α
⊢ s.sup f ≤ a ↔ ∀ b ∈ s, f b ≤ a

Tactic:
apply Iff.trans Multiset.sup_le

Result:
α : Type u_2
β : Type u_3
inst✝¹ : SemilatticeSup α
inst✝ : OrderBot α
s : Finset β
f : β → α
a : α
⊢ (∀ b ∈ Multiset.map f s.val, b ≤ a) ↔ ∀ b ∈ s, f b ≤ a

Proof state:
α : Type u_2
β : Type u_3
inst✝¹ : SemilatticeSup α
inst✝ : OrderBot α
s : Finset β
f : β → α
a : α
⊢ (∀ (b : α), ∀ x ∈ s.val, f x = b → b ≤ a) ↔ ∀ b ∈ s, f b ≤ a

Tactic:
exact ⟨fun k b hb => k _ _ hb rfl, fun k a' b hb h => h ▸ k _ hb⟩

Result:
no goals

Proof state:
α : Type u_2
β : Type u_3
inst✝¹ : SemilatticeSup α
inst✝ : OrderBot α
s : Finset β
f : β → α
a : α
⊢ (∀ b ∈ Multiset.map f s.val, b ≤ a) ↔ ∀ b ∈ s, f b ≤ a

Tactic:
simp only [Multiset.mem_map, and_imp, exists_imp]

Result:
α : Type u_2
β : Type u_3
inst✝¹ : SemilatticeSup α
inst✝ : OrderBot α
s : Finset β
f : β → α
a : α
⊢ (∀ (b : α), ∀ x ∈ s.val, f x = b → b ≤ a) ↔ ∀ b ∈ s, f b ≤ a
-- Mathlib/Analysis/Normed/Lp/ProdLp.lean
theorem prod_lipschitzWith_equiv_aux [PseudoEMetricSpace α] [PseudoEMetricSpace β] :
    LipschitzWith 1 (WithLp.equiv p (α × β))

Proof state:
case inr
p : ℝ≥0∞
α : Type u_2
β : Type u_3
hp : Fact (1 ≤ p)
inst✝¹ : PseudoEMetricSpace α
inst✝ : PseudoEMetricSpace β
x y : WithLp p (α × β)
h : 1 ≤ p.toReal
cancel : p.toReal * (1 / p.toReal) = 1
⊢ edist ((WithLp.equiv p (α × β)) x) ((WithLp.equiv p (α × β)) y) ≤
    ↑1 * (edist x.1 y.1 ^ p.toReal + edist x.2 y.2 ^ p.toReal) ^ (1 / p.toReal)

Tactic:
simp only [edist, forall_prop_of_true, one_mul, ENNReal.coe_one, sup_le_iff]

Result:
case inr
p : ℝ≥0∞
α : Type u_2
β : Type u_3
hp : Fact (1 ≤ p)
inst✝¹ : PseudoEMetricSpace α
inst✝ : PseudoEMetricSpace β
x y : WithLp p (α × β)
h : 1 ≤ p.toReal
cancel : p.toReal * (1 / p.toReal) = 1
⊢ edist ((WithLp.equiv p (α × β)) x).1 ((WithLp.equiv p (α × β)) y).1 ≤
      (edist x.1 y.1 ^ p.toReal + edist x.2 y.2 ^ p.toReal) ^ (1 / p.toReal) ∧
    edist ((WithLp.equiv p (α × β)) x).2 ((WithLp.equiv p (α × β)) y).2 ≤
      (edist x.1 y.1 ^ p.toReal + edist x.2 y.2 ^ p.toReal) ^ (1 / p.toReal)

Proof state:
case h₁
p : ℝ≥0∞
α : Type u_2
β : Type u_3
hp : Fact (1 ≤ p)
inst✝¹ : PseudoEMetricSpace α
inst✝ : PseudoEMetricSpace β
x y : WithLp p (α × β)
h : 1 ≤ p.toReal
cancel : p.toReal * (1 / p.toReal) = 1
⊢ edist x.1 y.1 ^ p.toReal ≤ edist x.1 y.1 ^ p.toReal + edist x.2 y.2 ^ p.toReal

Tactic:
simp only [self_le_add_right]

Result:
no goals
-- Mathlib/Data/Set/Countable.lean
lemma range_enumerateCountable_subset {s : Set α} (h : s.Countable) (default : α) :
    range (enumerateCountable h default) ⊆ insert default s

Proof state:
α : Type u
s : Set α
h : s.Countable
default : α
n : ℕ
⊢ (match decode n with
    | some y => ↑y
    | none => default) ∈
    insert default s

Tactic:
match @decode s (Countable.toEncodable h) n with
| none => exact mem_insert _ _
| some val => simp

Result:
no goals

Proof state:
α : Type u
s : Set α
h : s.Countable
default : α
⊢ range (enumerateCountable h default) ⊆ insert default s

Tactic:
refine range_subset_iff.mpr (fun n ↦ ?_)

Result:
α : Type u
s : Set α
h : s.Countable
default : α
n : ℕ
⊢ enumerateCountable h default n ∈ insert default s

Proof state:
α : Type u
s : Set α
h : s.Countable
default : α
n : ℕ
val : ↑s
⊢ (match some val with
    | some y => ↑y
    | none => default) ∈
    insert default s

Tactic:
simp

Result:
no goals

Proof state:
α : Type u
s : Set α
h : s.Countable
default : α
n : ℕ
⊢ enumerateCountable h default n ∈ insert default s

Tactic:
rw [enumerateCountable]

Result:
α : Type u
s : Set α
h : s.Countable
default : α
n : ℕ
⊢ (match decode n with
    | some y => ↑y
    | none => default) ∈
    insert default s

Proof state:
α : Type u
s : Set α
h : s.Countable
default : α
n : ℕ
⊢ (match none with
    | some y => ↑y
    | none => default) ∈
    insert default s

Tactic:
exact mem_insert _ _

Result:
no goals
-- Mathlib/Algebra/Order/Floor.lean
theorem floor_neg : ⌊-a⌋ = -⌈a⌉ :=
  eq_of_forall_le_iff fun z => by rw [le_neg, ceil_le, le_floor, Int.cast_neg, le_neg]

Proof state:
α : Type u_2
inst✝¹ : LinearOrderedRing α
inst✝ : FloorRing α
a : α
z : ℤ
⊢ z ≤ ⌊-a⌋ ↔ z ≤ -⌈a⌉

Tactic:
rw [le_neg, ceil_le, le_floor, Int.cast_neg, le_neg]

Result:
no goals
-- Mathlib/Geometry/Euclidean/Angle/Oriented/RightAngle.lean
theorem oangle_right_eq_arccos_of_oangle_eq_pi_div_two {p₁ p₂ p₃ : P} (h : ∡ p₁ p₂ p₃ = ↑(π / 2)) :
    ∡ p₂ p₃ p₁ = Real.arccos (dist p₃ p₂ / dist p₁ p₃)

Proof state:
V : Type u_1
P : Type u_2
inst✝⁴ : NormedAddCommGroup V
inst✝³ : InnerProductSpace ℝ V
inst✝² : MetricSpace P
inst✝¹ : NormedAddTorsor V P
hd2 : Fact (finrank ℝ V = 2)
inst✝ : Oriented ℝ V (Fin 2)
p₁ p₂ p₃ : P
h : ∡ p₁ p₂ p₃ = ↑(π / 2)
hs : (∡ p₂ p₃ p₁).sign = 1
⊢ ∡ p₂ p₃ p₁ = ↑(Real.arccos (dist p₃ p₂ / dist p₁ p₃))

Tactic:
rw [oangle_eq_angle_of_sign_eq_one hs,
  angle_eq_arccos_of_angle_eq_pi_div_two (angle_eq_pi_div_two_of_oangle_eq_pi_div_two h)]

Result:
no goals

Proof state:
V : Type u_1
P : Type u_2
inst✝⁴ : NormedAddCommGroup V
inst✝³ : InnerProductSpace ℝ V
inst✝² : MetricSpace P
inst✝¹ : NormedAddTorsor V P
hd2 : Fact (finrank ℝ V = 2)
inst✝ : Oriented ℝ V (Fin 2)
p₁ p₂ p₃ : P
h : ∡ p₁ p₂ p₃ = ↑(π / 2)
⊢ (∡ p₂ p₃ p₁).sign = 1

Tactic:
rw [oangle_rotate_sign, h, Real.Angle.sign_coe_pi_div_two]

Result:
no goals

Proof state:
V : Type u_1
P : Type u_2
inst✝⁴ : NormedAddCommGroup V
inst✝³ : InnerProductSpace ℝ V
inst✝² : MetricSpace P
inst✝¹ : NormedAddTorsor V P
hd2 : Fact (finrank ℝ V = 2)
inst✝ : Oriented ℝ V (Fin 2)
p₁ p₂ p₃ : P
h : ∡ p₁ p₂ p₃ = ↑(π / 2)
⊢ ∡ p₂ p₃ p₁ = ↑(Real.arccos (dist p₃ p₂ / dist p₁ p₃))

Tactic:
have hs : (∡ p₂ p₃ p₁).sign = 1 := by rw [oangle_rotate_sign, h, Real.Angle.sign_coe_pi_div_two]

Result:
V : Type u_1
P : Type u_2
inst✝⁴ : NormedAddCommGroup V
inst✝³ : InnerProductSpace ℝ V
inst✝² : MetricSpace P
inst✝¹ : NormedAddTorsor V P
hd2 : Fact (finrank ℝ V = 2)
inst✝ : Oriented ℝ V (Fin 2)
p₁ p₂ p₃ : P
h : ∡ p₁ p₂ p₃ = ↑(π / 2)
hs : (∡ p₂ p₃ p₁).sign = 1
⊢ ∡ p₂ p₃ p₁ = ↑(Real.arccos (dist p₃ p₂ / dist p₁ p₃))
-- Mathlib/Topology/Compactness/Compact.lean
/-- If a compact set belongs to a filter and this filter has a unique cluster point `y` in this set,
then the filter is less than or equal to `𝓝 y`. -/
lemma IsCompact.le_nhds_of_unique_clusterPt (hs : IsCompact s) {l : Filter X} {y : X}
    (hmem : s ∈ l) (h : ∀ x ∈ s, ClusterPt x l → x = y) : l ≤ 𝓝 y

Proof state:
X : Type u
inst✝ : TopologicalSpace X
s : Set X
hs : IsCompact s
l : Filter X
y : X
hmem : s ∈ l
h : ∀ x ∈ s, ClusterPt x l → x = y
⊢ l ≤ 𝓝 y

Tactic:
refine le_iff_ultrafilter.2 fun f hf ↦ ?_

Result:
X : Type u
inst✝ : TopologicalSpace X
s : Set X
hs : IsCompact s
l : Filter X
y : X
hmem : s ∈ l
h : ∀ x ∈ s, ClusterPt x l → x = y
f : Ultrafilter X
hf : ↑f ≤ l
⊢ ↑f ≤ 𝓝 y

Proof state:
X : Type u
inst✝ : TopologicalSpace X
s : Set X
hs : IsCompact s
l : Filter X
y : X
hmem : s ∈ l
h : ∀ x ∈ s, ClusterPt x l → x = y
f : Ultrafilter X
hf : ↑f ≤ l
⊢ ↑f ≤ 𝓝 y

Tactic:
rcases hs.ultrafilter_le_nhds' f (hf hmem) with ⟨x, hxs, hx⟩

Result:
case intro.intro
X : Type u
inst✝ : TopologicalSpace X
s : Set X
hs : IsCompact s
l : Filter X
y : X
hmem : s ∈ l
h : ∀ x ∈ s, ClusterPt x l → x = y
f : Ultrafilter X
hf : ↑f ≤ l
x : X
hxs : x ∈ s
hx : ↑f ≤ 𝓝 x
⊢ ↑f ≤ 𝓝 y

Proof state:
case intro.intro
X : Type u
inst✝ : TopologicalSpace X
s : Set X
hs : IsCompact s
l : Filter X
y : X
hmem : s ∈ l
h : ∀ x ∈ s, ClusterPt x l → x = y
f : Ultrafilter X
hf : ↑f ≤ l
x : X
hxs : x ∈ s
hx : ↑f ≤ 𝓝 x
⊢ ↑f ≤ 𝓝 y

Tactic:
convert ← hx

Result:
case h.e'_4.h.e'_3
X : Type u
inst✝ : TopologicalSpace X
s : Set X
hs : IsCompact s
l : Filter X
y : X
hmem : s ∈ l
h : ∀ x ∈ s, ClusterPt x l → x = y
f : Ultrafilter X
hf : ↑f ≤ l
x : X
hxs : x ∈ s
hx : ↑f ≤ 𝓝 x
⊢ x = y

Proof state:
case h.e'_4.h.e'_3
X : Type u
inst✝ : TopologicalSpace X
s : Set X
hs : IsCompact s
l : Filter X
y : X
hmem : s ∈ l
h : ∀ x ∈ s, ClusterPt x l → x = y
f : Ultrafilter X
hf : ↑f ≤ l
x : X
hxs : x ∈ s
hx : ↑f ≤ 𝓝 x
⊢ x = y

Tactic:
exact h x hxs (.mono (.of_le_nhds hx) hf)

Result:
no goals
-- Mathlib/MeasureTheory/Function/ConvergenceInMeasure.lean
theorem seqTendstoAeSeq_strictMono (hfg : TendstoInMeasure μ f atTop g) :
    StrictMono (seqTendstoAeSeq hfg)

Proof state:
α : Type u_1
E : Type u_4
m : MeasurableSpace α
μ : Measure α
inst✝ : MetricSpace E
f : ℕ → α → E
g : α → E
hfg : TendstoInMeasure μ f atTop g
n : ℕ
⊢ seqTendstoAeSeq hfg n < seqTendstoAeSeq hfg (n + 1)

Tactic:
rw [seqTendstoAeSeq_succ]

Result:
α : Type u_1
E : Type u_4
m : MeasurableSpace α
μ : Measure α
inst✝ : MetricSpace E
f : ℕ → α → E
g : α → E
hfg : TendstoInMeasure μ f atTop g
n : ℕ
⊢ seqTendstoAeSeq hfg n < seqTendstoAeSeqAux hfg (n + 1) ⊔ (seqTendstoAeSeq hfg n + 1)

Proof state:
α : Type u_1
E : Type u_4
m : MeasurableSpace α
μ : Measure α
inst✝ : MetricSpace E
f : ℕ → α → E
g : α → E
hfg : TendstoInMeasure μ f atTop g
⊢ StrictMono (seqTendstoAeSeq hfg)

Tactic:
refine strictMono_nat_of_lt_succ fun n => ?_

Result:
α : Type u_1
E : Type u_4
m : MeasurableSpace α
μ : Measure α
inst✝ : MetricSpace E
f : ℕ → α → E
g : α → E
hfg : TendstoInMeasure μ f atTop g
n : ℕ
⊢ seqTendstoAeSeq hfg n < seqTendstoAeSeq hfg (n + 1)

Proof state:
α : Type u_1
E : Type u_4
m : MeasurableSpace α
μ : Measure α
inst✝ : MetricSpace E
f : ℕ → α → E
g : α → E
hfg : TendstoInMeasure μ f atTop g
n : ℕ
⊢ seqTendstoAeSeq hfg n < seqTendstoAeSeqAux hfg (n + 1) ⊔ (seqTendstoAeSeq hfg n + 1)

Tactic:
exact lt_of_lt_of_le (lt_add_one <| seqTendstoAeSeq hfg n) (le_max_right _ _)

Result:
no goals
-- Mathlib/RingTheory/Spectrum/Prime/Polynomial.lean
lemma comap_C_surjective : Function.Surjective (comap (R := R) C)

Proof state:
R : Type u_1
inst✝ : CommRing R
x : PrimeSpectrum R
⊢ ∃ a, (comap C) a = x

Tactic:
refine ⟨comap (evalRingHom 0) x, ?_⟩

Result:
R : Type u_1
inst✝ : CommRing R
x : PrimeSpectrum R
⊢ (comap C) ((comap (evalRingHom 0)) x) = x

Proof state:
case a
R : Type u_1
inst✝ : CommRing R
x : PrimeSpectrum R
x✝ : R
⊢ ((evalRingHom 0).comp C) x✝ = (RingHom.id R) x✝

Tactic:
simp

Result:
no goals

Proof state:
R : Type u_1
inst✝ : CommRing R
x : PrimeSpectrum R
⊢ (evalRingHom 0).comp C = RingHom.id R

Tactic:
ext

Result:
case a
R : Type u_1
inst✝ : CommRing R
x : PrimeSpectrum R
x✝ : R
⊢ ((evalRingHom 0).comp C) x✝ = (RingHom.id R) x✝

Proof state:
R : Type u_1
inst✝ : CommRing R
⊢ Function.Surjective ⇑(comap C)

Tactic:
intro x

Result:
R : Type u_1
inst✝ : CommRing R
x : PrimeSpectrum R
⊢ ∃ a, (comap C) a = x

Proof state:
R : Type u_1
inst✝ : CommRing R
x : PrimeSpectrum R
⊢ (comap C) ((comap (evalRingHom 0)) x) = x

Tactic:
rw [← comap_comp_apply, (show (evalRingHom 0).comp C = .id R by ext; simp),
  comap_id, ContinuousMap.id_apply]

Result:
no goals
-- Mathlib/Topology/Basic.lean
theorem dense_iff_inter_open :
    Dense s ↔ ∀ U, IsOpen U → U.Nonempty → (U ∩ s).Nonempty

Proof state:
case mpr
X : Type u
s : Set X
inst✝ : TopologicalSpace X
h : ∀ (U : Set X), IsOpen U → U.Nonempty → (U ∩ s).Nonempty
x : X
U : Set X
U_op : IsOpen U
x_in : x ∈ U
⊢ (U ∩ s).Nonempty

Tactic:
exact h U U_op ⟨_, x_in⟩

Result:
no goals

Proof state:
case mpr
X : Type u
s : Set X
inst✝ : TopologicalSpace X
h : ∀ (U : Set X), IsOpen U → U.Nonempty → (U ∩ s).Nonempty
x : X
⊢ ∀ (o : Set X), IsOpen o → x ∈ o → (o ∩ s).Nonempty

Tactic:
intro U U_op x_in

Result:
case mpr
X : Type u
s : Set X
inst✝ : TopologicalSpace X
h : ∀ (U : Set X), IsOpen U → U.Nonempty → (U ∩ s).Nonempty
x : X
U : Set X
U_op : IsOpen U
x_in : x ∈ U
⊢ (U ∩ s).Nonempty

Proof state:
X : Type u
s : Set X
inst✝ : TopologicalSpace X
⊢ Dense s ↔ ∀ (U : Set X), IsOpen U → U.Nonempty → (U ∩ s).Nonempty

Tactic:
constructor <;> intro h

Result:
case mp
X : Type u
s : Set X
inst✝ : TopologicalSpace X
h : Dense s
⊢ ∀ (U : Set X), IsOpen U → U.Nonempty → (U ∩ s).Nonempty

case mpr
X : Type u
s : Set X
inst✝ : TopologicalSpace X
h : ∀ (U : Set X), IsOpen U → U.Nonempty → (U ∩ s).Nonempty
⊢ Dense s

Proof state:
case mp
X : Type u
s : Set X
inst✝ : TopologicalSpace X
h : Dense s
⊢ ∀ (U : Set X), IsOpen U → U.Nonempty → (U ∩ s).Nonempty

Tactic:
rintro U U_op ⟨x, x_in⟩

Result:
case mp.intro
X : Type u
s : Set X
inst✝ : TopologicalSpace X
h : Dense s
U : Set X
U_op : IsOpen U
x : X
x_in : x ∈ U
⊢ (U ∩ s).Nonempty

Proof state:
case mpr
X : Type u
s : Set X
inst✝ : TopologicalSpace X
h : ∀ (U : Set X), IsOpen U → U.Nonempty → (U ∩ s).Nonempty
x : X
⊢ x ∈ closure s

Tactic:
rw [mem_closure_iff]

Result:
case mpr
X : Type u
s : Set X
inst✝ : TopologicalSpace X
h : ∀ (U : Set X), IsOpen U → U.Nonempty → (U ∩ s).Nonempty
x : X
⊢ ∀ (o : Set X), IsOpen o → x ∈ o → (o ∩ s).Nonempty

Proof state:
case mp.intro
X : Type u
s : Set X
inst✝ : TopologicalSpace X
h : Dense s
U : Set X
U_op : IsOpen U
x : X
x_in : x ∈ U
⊢ (U ∩ s).Nonempty

Tactic:
exact mem_closure_iff.1 (h _) U U_op x_in

Result:
no goals

Proof state:
case mpr
X : Type u
s : Set X
inst✝ : TopologicalSpace X
h : ∀ (U : Set X), IsOpen U → U.Nonempty → (U ∩ s).Nonempty
⊢ Dense s

Tactic:
intro x

Result:
case mpr
X : Type u
s : Set X
inst✝ : TopologicalSpace X
h : ∀ (U : Set X), IsOpen U → U.Nonempty → (U ∩ s).Nonempty
x : X
⊢ x ∈ closure s
-- Mathlib/Topology/UniformSpace/UniformEmbedding.lean
lemma isUniformInducing_iff_uniformSpace {f : α → β} :
    IsUniformInducing f ↔ ‹UniformSpace β›.comap f = ‹UniformSpace α›

Proof state:
α : Type u
β : Type v
inst✝¹ : UniformSpace α
inst✝ : UniformSpace β
f : α → β
⊢ (∀ (s : Set (α × α)), s ∈ comap (fun x => (f x.1, f x.2)) (𝓤 β) ↔ s ∈ 𝓤 α) ↔ ∀ (s : Set (α × α)), s ∈ 𝓤 α ↔ s ∈ 𝓤 α

Tactic:
rfl

Result:
no goals

Proof state:
α : Type u
β : Type v
inst✝¹ : UniformSpace α
inst✝ : UniformSpace β
f : α → β
⊢ IsUniformInducing f ↔ UniformSpace.comap f inst✝ = inst✝¹

Tactic:
rw [isUniformInducing_iff, UniformSpace.ext_iff, Filter.ext_iff]

Result:
α : Type u
β : Type v
inst✝¹ : UniformSpace α
inst✝ : UniformSpace β
f : α → β
⊢ (∀ (s : Set (α × α)), s ∈ comap (fun x => (f x.1, f x.2)) (𝓤 β) ↔ s ∈ 𝓤 α) ↔ ∀ (s : Set (α × α)), s ∈ 𝓤 α ↔ s ∈ 𝓤 α
-- Mathlib/Order/Minimal.lean
theorem maximal_mem_image (f : α ↪o β) (hx : Maximal (· ∈ s) x) : Maximal (· ∈ f '' s) (f x) :=
  _root_.maximal_mem_image_monotone (by simp [f.le_iff_le]) hx

Proof state:
α : Type u_1
x : α
inst✝¹ : Preorder α
β : Type u_2
inst✝ : Preorder β
s : Set α
f : α ↪o β
hx : Maximal (fun x => x ∈ s) x
⊢ ∀ ⦃x y : α⦄, x ∈ s → y ∈ s → (f x ≤ f y ↔ x ≤ y)

Tactic:
simp [f.le_iff_le]

Result:
no goals
-- Mathlib/Data/Fin/VecNotation.lean
theorem cons_vec_bit1_eq_alt1 (x : α) (u : Fin n → α) (i : Fin (n + 1)) :
    vecCons x u ((i + i) + 1) = vecAlt1 rfl (vecAppend rfl (vecCons x u) (vecCons x u)) i

Proof state:
α : Type u
n : ℕ
x : α
u : Fin n → α
i : Fin (n + 1)
⊢ vecCons x u (i + i + 1) = (vecCons x u ∘ fun n_1 => n_1 + n_1 + 1) i

Tactic:
rfl

Result:
no goals

Proof state:
α : Type u
n : ℕ
x : α
u : Fin n → α
i : Fin (n + 1)
⊢ vecCons x u (i + i + 1) = vecAlt1 ⋯ (vecAppend ⋯ (vecCons x u) (vecCons x u)) i

Tactic:
rw [vecAlt1_vecAppend]

Result:
α : Type u
n : ℕ
x : α
u : Fin n → α
i : Fin (n + 1)
⊢ vecCons x u (i + i + 1) = (vecCons x u ∘ fun n_1 => n_1 + n_1 + 1) i
-- Mathlib/Analysis/SpecialFunctions/Trigonometric/Basic.lean
theorem exists_cos_eq_zero : 0 ∈ cos '' Icc (1 : ℝ) 2 :=
  intermediate_value_Icc' (by norm_num) continuousOn_cos
    ⟨le_of_lt cos_two_neg, le_of_lt cos_one_pos⟩

Proof state:
⊢ 1 ≤ 2

Tactic:
norm_num

Result:
no goals
-- Mathlib/LinearAlgebra/RootSystem/Hom.lean
@[simp]
lemma comp_id {ι₂ M₂ N₂ : Type*}
    [AddCommGroup M₂] [Module R M₂] [AddCommGroup N₂] [Module R N₂]
    (P : RootPairing ι R M N) (Q : RootPairing ι₂ R M₂ N₂) (f : RootPairing.Equiv P Q) :
    comp (id Q) f = f

Proof state:
ι : Type u_1
R : Type u_2
M : Type u_3
N : Type u_4
inst✝⁸ : CommRing R
inst✝⁷ : AddCommGroup M
inst✝⁶ : Module R M
inst✝⁵ : AddCommGroup N
inst✝⁴ : Module R N
ι₂ : Type u_8
M₂ : Type u_9
N₂ : Type u_10
inst✝³ : AddCommGroup M₂
inst✝² : Module R M₂
inst✝¹ : AddCommGroup N₂
inst✝ : Module R N₂
P : RootPairing ι R M N
Q : RootPairing ι₂ R M₂ N₂
f : P.Equiv Q
⊢ (id Q).comp f = f

Tactic:
ext x <;> simp

Result:
no goals
-- Mathlib/RingTheory/Ideal/Prod.lean
theorem map_prodComm_prod :
    map ((RingEquiv.prodComm : R × S ≃+* S × R) : R × S →+* S × R) (prod I J) = prod J I

Proof state:
R : Type u
S : Type v
inst✝¹ : Semiring R
inst✝ : Semiring S
I : Ideal R
J : Ideal S
⊢ (map (RingHom.fst S R) (map (↑RingEquiv.prodComm) (I.prod J))).prod
      (map (RingHom.snd S R) (map (↑RingEquiv.prodComm) (I.prod J))) =
    J.prod I

Tactic:
simp [map_map]

Result:
no goals

Proof state:
R : Type u
S : Type v
inst✝¹ : Semiring R
inst✝ : Semiring S
I : Ideal R
J : Ideal S
⊢ map (↑RingEquiv.prodComm) (I.prod J) = J.prod I

Tactic:
refine Trans.trans (ideal_prod_eq _) ?_

Result:
R : Type u
S : Type v
inst✝¹ : Semiring R
inst✝ : Semiring S
I : Ideal R
J : Ideal S
⊢ (map (RingHom.fst S R) (map (↑RingEquiv.prodComm) (I.prod J))).prod
      (map (RingHom.snd S R) (map (↑RingEquiv.prodComm) (I.prod J))) =
    J.prod I
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Array/MapIdx.lean
theorem mapFinIdx_eq_mapIdx {l : Array α} {f : (i : Nat) → α → (h : i < l.size) → β} {g : Nat → α → β}
    (h : ∀ (i : Nat) (h : i < l.size), f i l[i] h = g i l[i]) :
    l.mapFinIdx f = l.mapIdx g

Proof state:
α : Type u_1
β : Type u_2
l : Array α
f : (i : Nat) → α → i < l.size → β
g : Nat → α → β
h : ∀ (i : Nat) (h : i < l.size), f i l[i] h = g i l[i]
⊢ l.mapFinIdx f = mapIdx g l

Tactic:
simp_all [mapFinIdx_eq_iff]

Result:
no goals
-- Mathlib/Algebra/Ring/SumsOfSquares.lean
theorem sumSq_toAddSubmonoid : (sumSq T).toAddSubmonoid = .sumSq T

Proof state:
T : Type u_2
inst✝ : NonUnitalCommSemiring T
⊢ (sumSq T).toAddSubmonoid = AddSubmonoid.sumSq T

Tactic:
simp [sumSq, ← AddSubmonoid.closure_isSquare,
  Subsemigroup.nonUnitalSubsemiringClosure_toAddSubmonoid]

Result:
no goals
-- Mathlib/FieldTheory/Extension.lean
theorem eq_iff : L₁ = L₂ ↔
    ∃ h : L₁.carrier = L₂.carrier, L₂.emb.comp (inclusion h.le) = L₁.emb

Proof state:
F : Type u_1
E : Type u_2
K : Type u_3
inst✝⁴ : Field F
inst✝³ : Field E
inst✝² : Field K
inst✝¹ : Algebra F E
inst✝ : Algebra F K
L₁ L₂ : Lifts F E K
⊢ L₁ = L₂ ↔ ∃ (h : L₁.carrier = L₂.carrier), L₂.emb.comp (inclusion ⋯) = L₁.emb

Tactic:
rw [eq_iff_le_carrier_eq, le_iff]

Result:
F : Type u_1
E : Type u_2
K : Type u_3
inst✝⁴ : Field F
inst✝³ : Field E
inst✝² : Field K
inst✝¹ : Algebra F E
inst✝ : Algebra F K
L₁ L₂ : Lifts F E K
⊢ (∃ (h : L₁.carrier ≤ L₂.carrier), L₂.emb.comp (inclusion h) = L₁.emb) ∧ L₁.carrier = L₂.carrier ↔
    ∃ (h : L₁.carrier = L₂.carrier), L₂.emb.comp (inclusion ⋯) = L₁.emb

Proof state:
F : Type u_1
E : Type u_2
K : Type u_3
inst✝⁴ : Field F
inst✝³ : Field E
inst✝² : Field K
inst✝¹ : Algebra F E
inst✝ : Algebra F K
L₁ L₂ : Lifts F E K
⊢ (∃ (h : L₁.carrier ≤ L₂.carrier), L₂.emb.comp (inclusion h) = L₁.emb) ∧ L₁.carrier = L₂.carrier ↔
    ∃ (h : L₁.carrier = L₂.carrier), L₂.emb.comp (inclusion ⋯) = L₁.emb

Tactic:
exact ⟨fun h ↦ ⟨h.2, h.1.2⟩, fun h ↦ ⟨⟨h.1.le, h.2⟩, h.1⟩⟩

Result:
no goals
-- Mathlib/RingTheory/AlgebraicIndependent/RankAndCardinality.lean
theorem Algebra.Transcendental.rank_eq_cardinalMk
    (F : Type u) (E : Type v) [Field F] [Field E] [Algebra F E] [Algebra.Transcendental F E] :
    Module.rank F E = #E

Proof state:
case intro.intro
F : Type u
E : Type v
inst✝³ : Field F
inst✝² : Field E
inst✝¹ : Algebra F E
inst✝ : Algebra.Transcendental F E
ι : Type v
x : ι → E
hx : IsTranscendenceBasis F x
this : Nonempty ι
⊢ Module.rank F E = #E

Tactic:
simpa [← hx.lift_cardinalMk_eq_max_lift] using hx.lift_rank_eq_max_lift

Result:
no goals

Proof state:
case intro.intro
F : Type u
E : Type v
inst✝³ : Field F
inst✝² : Field E
inst✝¹ : Algebra F E
inst✝ : Algebra.Transcendental F E
ι : Type v
x : ι → E
hx : IsTranscendenceBasis F x
⊢ Module.rank F E = #E

Tactic:
haveI := hx.nonempty_iff_transcendental.2 ‹_›

Result:
case intro.intro
F : Type u
E : Type v
inst✝³ : Field F
inst✝² : Field E
inst✝¹ : Algebra F E
inst✝ : Algebra.Transcendental F E
ι : Type v
x : ι → E
hx : IsTranscendenceBasis F x
this : Nonempty ι
⊢ Module.rank F E = #E

Proof state:
F : Type u
E : Type v
inst✝³ : Field F
inst✝² : Field E
inst✝¹ : Algebra F E
inst✝ : Algebra.Transcendental F E
⊢ Module.rank F E = #E

Tactic:
obtain ⟨ι, x, hx⟩ := exists_isTranscendenceBasis' _ (algebraMap F E).injective

Result:
case intro.intro
F : Type u
E : Type v
inst✝³ : Field F
inst✝² : Field E
inst✝¹ : Algebra F E
inst✝ : Algebra.Transcendental F E
ι : Type v
x : ι → E
hx : IsTranscendenceBasis F x
⊢ Module.rank F E = #E
-- Mathlib/Data/Rat/Lemmas.lean
theorem add_num_den (q r : ℚ) :
    q + r = (q.num * r.den + q.den * r.num : ℤ) /. (↑q.den * ↑r.den : ℤ)

Proof state:
q r : ℚ
⊢ q + r = (q.num * ↑r.den + ↑q.den * r.num) /. (↑q.den * ↑r.den)

Tactic:
have hqd : (q.den : ℤ) ≠ 0 := Int.natCast_ne_zero_iff_pos.2 q.den_pos

Result:
q r : ℚ
hqd : ↑q.den ≠ 0
⊢ q + r = (q.num * ↑r.den + ↑q.den * r.num) /. (↑q.den * ↑r.den)

Proof state:
q r : ℚ
hqd : ↑q.den ≠ 0
hrd : ↑r.den ≠ 0
⊢ (q.num * ↑r.den + r.num * ↑q.den) /. (↑q.den * ↑r.den) = (q.num * ↑r.den + ↑q.den * r.num) /. (↑q.den * ↑r.den)

Tactic:
rw [mul_comm r.num q.den]

Result:
no goals

Proof state:
q r : ℚ
hqd : ↑q.den ≠ 0
hrd : ↑r.den ≠ 0
⊢ q + r = (q.num * ↑r.den + ↑q.den * r.num) /. (↑q.den * ↑r.den)

Tactic:
conv_lhs => rw [← num_divInt_den q, ← num_divInt_den r, divInt_add_divInt _ _ hqd hrd]

Result:
q r : ℚ
hqd : ↑q.den ≠ 0
hrd : ↑r.den ≠ 0
⊢ (q.num * ↑r.den + r.num * ↑q.den) /. (↑q.den * ↑r.den) = (q.num * ↑r.den + ↑q.den * r.num) /. (↑q.den * ↑r.den)

Proof state:
q r : ℚ
hqd : ↑q.den ≠ 0
⊢ q + r = (q.num * ↑r.den + ↑q.den * r.num) /. (↑q.den * ↑r.den)

Tactic:
have hrd : (r.den : ℤ) ≠ 0 := Int.natCast_ne_zero_iff_pos.2 r.den_pos

Result:
q r : ℚ
hqd : ↑q.den ≠ 0
hrd : ↑r.den ≠ 0
⊢ q + r = (q.num * ↑r.den + ↑q.den * r.num) /. (↑q.den * ↑r.den)