harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/Topology/Algebra/UniformConvergence.lean
theorem UniformFun.hasBasis_nhds_one_of_basis {p : ι → Prop} {b : ι → Set G}
    (h : (𝓝 1 : Filter G).HasBasis p b) :
    (𝓝 1 : Filter (α →ᵤ G)).HasBasis p fun i => { f : α →ᵤ G | ∀ x, toFun f x ∈ b i }

Proof state:
α : Type u_1
G : Type u_2
ι : Type u_3
inst✝² : Group G
inst✝¹ : UniformSpace G
inst✝ : UniformGroup G
p : ι → Prop
b : ι → Set G
h : (𝓝 1).HasBasis p b
⊢ (𝓝 1).HasBasis p fun i => {f | ∀ (x : α), toFun f x ∈ b i}

Tactic:
convert UniformFun.hasBasis_nhds_of_basis α _ (1 : α →ᵤ G) h.uniformity_of_nhds_one

Result:
case h.e'_5.h.h.e'_2.h.a
α : Type u_1
G : Type u_2
ι : Type u_3
inst✝² : Group G
inst✝¹ : UniformSpace G
inst✝ : UniformGroup G
p : ι → Prop
b : ι → Set G
h : (𝓝 1).HasBasis p b
x✝¹ : ι
x✝ : α →ᵤ G
⊢ (∀ (x : α), toFun x✝ x ∈ b x✝¹) ↔ (1, x✝) ∈ UniformFun.gen α G {x | x.2 / x.1 ∈ b x✝¹}

Proof state:
case h.e'_5.h.h.e'_2.h.a
α : Type u_1
G : Type u_2
ι : Type u_3
inst✝² : Group G
inst✝¹ : UniformSpace G
inst✝ : UniformGroup G
p : ι → Prop
b : ι → Set G
h : (𝓝 1).HasBasis p b
x✝¹ : ι
x✝ : α →ᵤ G
⊢ (∀ (x : α), toFun x✝ x ∈ b x✝¹) ↔ (1, x✝) ∈ UniformFun.gen α G {x | x.2 / x.1 ∈ b x✝¹}

Tactic:
simp

Result:
no goals
-- Mathlib/LinearAlgebra/Ray.lean
theorem refl (x : M) : SameRay R x x

Proof state:
R : Type u_1
inst✝³ : StrictOrderedCommSemiring R
M : Type u_2
inst✝² : AddCommMonoid M
inst✝¹ : Module R M
x : M
inst✝ : Nontrivial R
⊢ SameRay R x x

Tactic:
exact Or.inr (Or.inr <| ⟨1, 1, zero_lt_one, zero_lt_one, rfl⟩)

Result:
no goals

Proof state:
R : Type u_1
inst✝² : StrictOrderedCommSemiring R
M : Type u_2
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
x : M
⊢ SameRay R x x

Tactic:
nontriviality R

Result:
R : Type u_1
inst✝³ : StrictOrderedCommSemiring R
M : Type u_2
inst✝² : AddCommMonoid M
inst✝¹ : Module R M
x : M
inst✝ : Nontrivial R
⊢ SameRay R x x
-- Mathlib/Analysis/SpecificLimits/Basic.lean
theorem dist_le_of_le_geometric_of_tendsto {a : α} (ha : Tendsto f atTop (𝓝 a)) (n : ℕ) :
    dist (f n) a ≤ C * r ^ n / (1 - r)

Proof state:
case h.e'_4
α : Type u_1
inst✝ : PseudoMetricSpace α
r C : ℝ
f : ℕ → α
hr : r < 1
hu : ∀ (n : ℕ), dist (f n) (f (n + 1)) ≤ C * r ^ n
a : α
ha : Tendsto f atTop (𝓝 a)
n : ℕ
this : HasSum (fun n => C * r ^ n) (C / (1 - r))
⊢ C * r ^ n / (1 - r) = ∑' (m : ℕ), C * r ^ (n + m)

Tactic:
simp only [pow_add, mul_left_comm C, mul_div_right_comm]

Result:
case h.e'_4
α : Type u_1
inst✝ : PseudoMetricSpace α
r C : ℝ
f : ℕ → α
hr : r < 1
hu : ∀ (n : ℕ), dist (f n) (f (n + 1)) ≤ C * r ^ n
a : α
ha : Tendsto f atTop (𝓝 a)
n : ℕ
this : HasSum (fun n => C * r ^ n) (C / (1 - r))
⊢ C / (1 - r) * r ^ n = ∑' (m : ℕ), r ^ n * (C * r ^ m)

Proof state:
case h.e'_4
α : Type u_1
inst✝ : PseudoMetricSpace α
r C : ℝ
f : ℕ → α
hr : r < 1
hu : ∀ (n : ℕ), dist (f n) (f (n + 1)) ≤ C * r ^ n
a : α
ha : Tendsto f atTop (𝓝 a)
n : ℕ
this : HasSum (fun n => C * r ^ n) (C / (1 - r))
⊢ r ^ n * (C / (1 - r)) = ∑' (m : ℕ), r ^ n * (C * r ^ m)

Tactic:
exact (this.mul_left _).tsum_eq.symm

Result:
no goals

Proof state:
α : Type u_1
inst✝ : PseudoMetricSpace α
r C : ℝ
f : ℕ → α
hr : r < 1
hu : ∀ (n : ℕ), dist (f n) (f (n + 1)) ≤ C * r ^ n
a : α
ha : Tendsto f atTop (𝓝 a)
n : ℕ
this : HasSum (fun n => C * r ^ n) (C / (1 - r))
⊢ dist (f n) a ≤ C * r ^ n / (1 - r)

Tactic:
convert dist_le_tsum_of_dist_le_of_tendsto _ hu ⟨_, this⟩ ha n

Result:
case h.e'_4
α : Type u_1
inst✝ : PseudoMetricSpace α
r C : ℝ
f : ℕ → α
hr : r < 1
hu : ∀ (n : ℕ), dist (f n) (f (n + 1)) ≤ C * r ^ n
a : α
ha : Tendsto f atTop (𝓝 a)
n : ℕ
this : HasSum (fun n => C * r ^ n) (C / (1 - r))
⊢ C * r ^ n / (1 - r) = ∑' (m : ℕ), C * r ^ (n + m)

Proof state:
α : Type u_1
inst✝ : PseudoMetricSpace α
r C : ℝ
f : ℕ → α
hr : r < 1
hu : ∀ (n : ℕ), dist (f n) (f (n + 1)) ≤ C * r ^ n
a : α
ha : Tendsto f atTop (𝓝 a)
n : ℕ
⊢ dist (f n) a ≤ C * r ^ n / (1 - r)

Tactic:
have := aux_hasSum_of_le_geometric hr hu

Result:
α : Type u_1
inst✝ : PseudoMetricSpace α
r C : ℝ
f : ℕ → α
hr : r < 1
hu : ∀ (n : ℕ), dist (f n) (f (n + 1)) ≤ C * r ^ n
a : α
ha : Tendsto f atTop (𝓝 a)
n : ℕ
this : HasSum (fun n => C * r ^ n) (C / (1 - r))
⊢ dist (f n) a ≤ C * r ^ n / (1 - r)

Proof state:
case h.e'_4
α : Type u_1
inst✝ : PseudoMetricSpace α
r C : ℝ
f : ℕ → α
hr : r < 1
hu : ∀ (n : ℕ), dist (f n) (f (n + 1)) ≤ C * r ^ n
a : α
ha : Tendsto f atTop (𝓝 a)
n : ℕ
this : HasSum (fun n => C * r ^ n) (C / (1 - r))
⊢ C / (1 - r) * r ^ n = ∑' (m : ℕ), r ^ n * (C * r ^ m)

Tactic:
rw [mul_comm]

Result:
case h.e'_4
α : Type u_1
inst✝ : PseudoMetricSpace α
r C : ℝ
f : ℕ → α
hr : r < 1
hu : ∀ (n : ℕ), dist (f n) (f (n + 1)) ≤ C * r ^ n
a : α
ha : Tendsto f atTop (𝓝 a)
n : ℕ
this : HasSum (fun n => C * r ^ n) (C / (1 - r))
⊢ r ^ n * (C / (1 - r)) = ∑' (m : ℕ), r ^ n * (C * r ^ m)
-- Mathlib/Combinatorics/SimpleGraph/Connectivity/Subgraph.lean
protected lemma Connected.sup {H K : G.Subgraph}
    (hH : H.Connected) (hK : K.Connected) (hn : (H ⊓ K).verts.Nonempty) :
    (H ⊔ K).Connected

Proof state:
V : Type u
G : SimpleGraph V
H K : G.Subgraph
hH : H.Connected
hK : K.Connected
hn : (H ⊓ K).verts.Nonempty
⊢ ∃ v, ∀ (w : ↑(H ⊔ K).verts), (H ⊔ K).coe.Reachable v w

Tactic:
obtain ⟨u, hu, hu'⟩ := hn

Result:
case intro.intro
V : Type u
G : SimpleGraph V
H K : G.Subgraph
hH : H.Connected
hK : K.Connected
u : V
hu : u ∈ H.verts
hu' : u ∈ K.verts
⊢ ∃ v, ∀ (w : ↑(H ⊔ K).verts), (H ⊔ K).coe.Reachable v w

Proof state:
case intro.intro
V : Type u
G : SimpleGraph V
H K : G.Subgraph
hH : H.Connected
hK : K.Connected
u : V
hu : u ∈ H.verts
hu' : u ∈ K.verts
⊢ ∀ (w : ↑(H ⊔ K).verts), (H ⊔ K).coe.Reachable ⟨u, ⋯⟩ w

Tactic:
rintro ⟨v, (hv|hv)⟩

Result:
case intro.intro.mk.inl
V : Type u
G : SimpleGraph V
H K : G.Subgraph
hH : H.Connected
hK : K.Connected
u : V
hu : u ∈ H.verts
hu' : u ∈ K.verts
v : V
hv : v ∈ H.verts
⊢ (H ⊔ K).coe.Reachable ⟨u, ⋯⟩ ⟨v, ⋯⟩

case intro.intro.mk.inr
V : Type u
G : SimpleGraph V
H K : G.Subgraph
hH : H.Connected
hK : K.Connected
u : V
hu : u ∈ H.verts
hu' : u ∈ K.verts
v : V
hv : v ∈ K.verts
⊢ (H ⊔ K).coe.Reachable ⟨u, ⋯⟩ ⟨v, ⋯⟩

Proof state:
case intro.intro.mk.inl
V : Type u
G : SimpleGraph V
H K : G.Subgraph
hH : H.Connected
hK : K.Connected
u : V
hu : u ∈ H.verts
hu' : u ∈ K.verts
v : V
hv : v ∈ H.verts
⊢ (H ⊔ K).coe.Reachable ⟨u, ⋯⟩ ⟨v, ⋯⟩

Tactic:
exact Reachable.map (Subgraph.inclusion (le_sup_left : H ≤ H ⊔ K)) (hH ⟨u, hu⟩ ⟨v, hv⟩)

Result:
no goals

Proof state:
case intro.intro.mk.inr
V : Type u
G : SimpleGraph V
H K : G.Subgraph
hH : H.Connected
hK : K.Connected
u : V
hu : u ∈ H.verts
hu' : u ∈ K.verts
v : V
hv : v ∈ K.verts
⊢ (H ⊔ K).coe.Reachable ⟨u, ⋯⟩ ⟨v, ⋯⟩

Tactic:
exact Reachable.map (Subgraph.inclusion (le_sup_right : K ≤ H ⊔ K)) (hK ⟨u, hu'⟩ ⟨v, hv⟩)

Result:
no goals

Proof state:
V : Type u
G : SimpleGraph V
H K : G.Subgraph
hH : H.Connected
hK : K.Connected
hn : (H ⊓ K).verts.Nonempty
⊢ (H ⊔ K).Connected

Tactic:
rw [Subgraph.connected_iff', connected_iff_exists_forall_reachable]

Result:
V : Type u
G : SimpleGraph V
H K : G.Subgraph
hH : H.Connected
hK : K.Connected
hn : (H ⊓ K).verts.Nonempty
⊢ ∃ v, ∀ (w : ↑(H ⊔ K).verts), (H ⊔ K).coe.Reachable v w

Proof state:
case intro.intro
V : Type u
G : SimpleGraph V
H K : G.Subgraph
hH : H.Connected
hK : K.Connected
u : V
hu : u ∈ H.verts
hu' : u ∈ K.verts
⊢ ∃ v, ∀ (w : ↑(H ⊔ K).verts), (H ⊔ K).coe.Reachable v w

Tactic:
exists ⟨u, Or.inl hu⟩

Result:
case intro.intro
V : Type u
G : SimpleGraph V
H K : G.Subgraph
hH : H.Connected
hK : K.Connected
u : V
hu : u ∈ H.verts
hu' : u ∈ K.verts
⊢ ∀ (w : ↑(H ⊔ K).verts), (H ⊔ K).coe.Reachable ⟨u, ⋯⟩ w
-- Mathlib/Data/Finset/Prod.lean
theorem product_image_snd [DecidableEq β] (ht : s.Nonempty) : (s ×ˢ t).image Prod.snd = t

Proof state:
α : Type u_1
β : Type u_2
s : Finset α
t : Finset β
inst✝ : DecidableEq β
ht : s.Nonempty
⊢ image Prod.snd (s ×ˢ t) = t

Tactic:
ext i

Result:
case h
α : Type u_1
β : Type u_2
s : Finset α
t : Finset β
inst✝ : DecidableEq β
ht : s.Nonempty
i : β
⊢ i ∈ image Prod.snd (s ×ˢ t) ↔ i ∈ t

Proof state:
case h
α : Type u_1
β : Type u_2
s : Finset α
t : Finset β
inst✝ : DecidableEq β
ht : s.Nonempty
i : β
⊢ i ∈ image Prod.snd (s ×ˢ t) ↔ i ∈ t

Tactic:
simp [mem_image, ht.exists_mem]

Result:
no goals
-- Mathlib/Algebra/Homology/ComplexShape.lean
theorem next_eq' (c : ComplexShape ι) {i j : ι} (h : c.Rel i j) : c.next i = j

Proof state:
ι : Type u_1
c : ComplexShape ι
i j : ι
h : c.Rel i j
⊢ c.next i = j

Tactic:
apply c.next_eq _ h

Result:
ι : Type u_1
c : ComplexShape ι
i j : ι
h : c.Rel i j
⊢ c.Rel i (c.next i)

Proof state:
ι : Type u_1
c : ComplexShape ι
i j : ι
h : c.Rel i j
⊢ c.Rel i (if h : ∃ j, c.Rel i j then h.choose else i)

Tactic:
rw [dif_pos]

Result:
ι : Type u_1
c : ComplexShape ι
i j : ι
h : c.Rel i j
⊢ c.Rel i (Exists.choose ?hc)

case hc
ι : Type u_1
c : ComplexShape ι
i j : ι
h : c.Rel i j
⊢ ∃ j, c.Rel i j

Proof state:
ι : Type u_1
c : ComplexShape ι
i j : ι
h : c.Rel i j
⊢ c.Rel i (c.next i)

Tactic:
rw [next]

Result:
ι : Type u_1
c : ComplexShape ι
i j : ι
h : c.Rel i j
⊢ c.Rel i (if h : ∃ j, c.Rel i j then h.choose else i)

Proof state:
ι : Type u_1
c : ComplexShape ι
i j : ι
h : c.Rel i j
⊢ c.Rel i (Exists.choose ?hc)

case hc
ι : Type u_1
c : ComplexShape ι
i j : ι
h : c.Rel i j
⊢ ∃ j, c.Rel i j

Tactic:
exact Exists.choose_spec ⟨j, h⟩

Result:
no goals
-- Mathlib/Analysis/RCLike/Basic.lean
theorem add_conj (z : K) : z + conj z = 2 * re z :=
  calc
    z + conj z = re z + im z * I + (re z - im z * I)

Proof state:
K : Type u_1
inst✝ : RCLike K
z : K
⊢ ↑(re z) + ↑(im z) * I + (↑(re z) - ↑(im z) * I) = 2 * ↑(re z)

Tactic:
rw [add_add_sub_cancel, two_mul]

Result:
no goals

Proof state:
K : Type u_1
inst✝ : RCLike K
z : K
⊢ z + (starRingEnd K) z = ↑(re z) + ↑(im z) * I + (↑(re z) - ↑(im z) * I)

Tactic:
rw [re_add_im, conj_eq_re_sub_im]

Result:
no goals
-- Mathlib/Algebra/Module/Submodule/Lattice.lean
theorem mem_sup_right {S T : Submodule R M} : ∀ {x : M}, x ∈ T → x ∈ S ⊔ T

Proof state:
R : Type u_1
M : Type u_3
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
S T : Submodule R M
this : T ≤ S ⊔ T
⊢ ∀ {x : M}, x ∈ T → x ∈ S ⊔ T

Tactic:
rw [LE.le] at this

Result:
R : Type u_1
M : Type u_3
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
S T : Submodule R M
this : Preorder.toLE.1 T (S ⊔ T)
⊢ ∀ {x : M}, x ∈ T → x ∈ S ⊔ T

Proof state:
R : Type u_1
M : Type u_3
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
S T : Submodule R M
⊢ ∀ {x : M}, x ∈ T → x ∈ S ⊔ T

Tactic:
have : T ≤ S ⊔ T := le_sup_right

Result:
R : Type u_1
M : Type u_3
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
S T : Submodule R M
this : T ≤ S ⊔ T
⊢ ∀ {x : M}, x ∈ T → x ∈ S ⊔ T

Proof state:
R : Type u_1
M : Type u_3
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
S T : Submodule R M
this : Preorder.toLE.1 T (S ⊔ T)
⊢ ∀ {x : M}, x ∈ T → x ∈ S ⊔ T

Tactic:
exact this

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Array/Lemmas.lean
theorem getElem?_eq_getElem?_toList (a : Array α) (i : Nat) : a[i]? = a.toList[i]?

Proof state:
α : Type u_1
a : Array α
i : Nat
⊢ (if h : i < a.size then some a[i] else none) = a.toList[i]?

Tactic:
split <;> simp_all

Result:
no goals

Proof state:
α : Type u_1
a : Array α
i : Nat
⊢ a[i]? = a.toList[i]?

Tactic:
rw [getElem?_def]

Result:
α : Type u_1
a : Array α
i : Nat
⊢ (if h : i < a.size then some a[i] else none) = a.toList[i]?
-- Mathlib/MeasureTheory/Integral/IntegrableOn.lean
theorem ContinuousOn.aemeasurable [TopologicalSpace α] [OpensMeasurableSpace α] [MeasurableSpace β]
    [TopologicalSpace β] [BorelSpace β] {f : α → β} {s : Set α} {μ : Measure α}
    (hf : ContinuousOn f s) (hs : MeasurableSet s) : AEMeasurable f (μ.restrict s)

Proof state:
α : Type u_1
β : Type u_2
inst✝⁵ : MeasurableSpace α
inst✝⁴ : TopologicalSpace α
inst✝³ : OpensMeasurableSpace α
inst✝² : MeasurableSpace β
inst✝¹ : TopologicalSpace β
inst✝ : BorelSpace β
f : α → β
s : Set α
μ : Measure α
hf : ContinuousOn f s
hs : MeasurableSet s
a✝ : Nontrivial α
inhabited_h : Inhabited α
⊢ AEMeasurable f (μ.restrict s)

Tactic:
have : (Set.piecewise s f fun _ => f default) =ᵐ[μ.restrict s] f := piecewise_ae_eq_restrict hs

Result:
α : Type u_1
β : Type u_2
inst✝⁵ : MeasurableSpace α
inst✝⁴ : TopologicalSpace α
inst✝³ : OpensMeasurableSpace α
inst✝² : MeasurableSpace β
inst✝¹ : TopologicalSpace β
inst✝ : BorelSpace β
f : α → β
s : Set α
μ : Measure α
hf : ContinuousOn f s
hs : MeasurableSet s
a✝ : Nontrivial α
inhabited_h : Inhabited α
this : (s.piecewise f fun x => f default) =ᶠ[ae (μ.restrict s)] f
⊢ AEMeasurable f (μ.restrict s)

Proof state:
case hf
α : Type u_1
β : Type u_2
inst✝⁵ : MeasurableSpace α
inst✝⁴ : TopologicalSpace α
inst✝³ : OpensMeasurableSpace α
inst✝² : MeasurableSpace β
inst✝¹ : TopologicalSpace β
inst✝ : BorelSpace β
f : α → β
s : Set α
μ : Measure α
hf : ContinuousOn f s
hs : MeasurableSet s
a✝ : Nontrivial α
inhabited_h : Inhabited α
this : (s.piecewise f fun x => f default) =ᶠ[ae (μ.restrict s)] f
t : Set β
ht : IsOpen t
⊢ MeasurableSet ((s.piecewise f fun x => f default) ⁻¹' t)

Tactic:
obtain ⟨u, u_open, hu⟩ : ∃ u : Set α, IsOpen u ∧ f ⁻¹' t ∩ s = u ∩ s :=
  _root_.continuousOn_iff'.1 hf t ht

Result:
case hf.intro.intro
α : Type u_1
β : Type u_2
inst✝⁵ : MeasurableSpace α
inst✝⁴ : TopologicalSpace α
inst✝³ : OpensMeasurableSpace α
inst✝² : MeasurableSpace β
inst✝¹ : TopologicalSpace β
inst✝ : BorelSpace β
f : α → β
s : Set α
μ : Measure α
hf : ContinuousOn f s
hs : MeasurableSet s
a✝ : Nontrivial α
inhabited_h : Inhabited α
this : (s.piecewise f fun x => f default) =ᶠ[ae (μ.restrict s)] f
t : Set β
ht : IsOpen t
u : Set α
u_open : IsOpen u
hu : f ⁻¹' t ∩ s = u ∩ s
⊢ MeasurableSet ((s.piecewise f fun x => f default) ⁻¹' t)
-- Mathlib/FieldTheory/PolynomialGaloisGroup.lean
theorem restrictProd_injective : Function.Injective (restrictProd p q)

Proof state:
case neg.h
F : Type u_1
inst✝ : Field F
p q : F[X]
hpq : ¬p * q = 0
f g : (p * q).Gal
hfg :
  (restrict p (p * q).SplittingField) f = (restrict p (p * q).SplittingField) g ∧
    (restrict q (p * q).SplittingField) f = (restrict q (p * q).SplittingField) g
x : (p * q).SplittingField
hx : x ∈ ↑(p.aroots (p * q).SplittingField + q.aroots (p * q).SplittingField).toFinset
⊢ f x = g x

Tactic:
rcases Multiset.mem_add.mp (Multiset.mem_toFinset.mp hx) with h | h

Result:
case neg.h.inl
F : Type u_1
inst✝ : Field F
p q : F[X]
hpq : ¬p * q = 0
f g : (p * q).Gal
hfg :
  (restrict p (p * q).SplittingField) f = (restrict p (p * q).SplittingField) g ∧
    (restrict q (p * q).SplittingField) f = (restrict q (p * q).SplittingField) g
x : (p * q).SplittingField
hx : x ∈ ↑(p.aroots (p * q).SplittingField + q.aroots (p * q).SplittingField).toFinset
h : x ∈ p.aroots (p * q).SplittingField
⊢ f x = g x

case neg.h.inr
F : Type u_1
inst✝ : Field F
p q : F[X]
hpq : ¬p * q = 0
f g : (p * q).Gal
hfg :
  (restrict p (p * q).SplittingField) f = (restrict p (p * q).SplittingField) g ∧
    (restrict q (p * q).SplittingField) f = (restrict q (p * q).SplittingField) g
x : (p * q).SplittingField
hx : x ∈ ↑(p.aroots (p * q).SplittingField + q.aroots (p * q).SplittingField).toFinset
h : x ∈ q.aroots (p * q).SplittingField
⊢ f x = g x

Proof state:
case neg
F : Type u_1
inst✝ : Field F
p q : F[X]
hpq : ¬p * q = 0
⊢ Function.Injective ⇑(restrictProd p q)

Tactic:
intro f g hfg

Result:
case neg
F : Type u_1
inst✝ : Field F
p q : F[X]
hpq : ¬p * q = 0
f g : (p * q).Gal
hfg : (restrictProd p q) f = (restrictProd p q) g
⊢ f = g

Proof state:
case pos
F : Type u_1
inst✝ : Field F
p q : F[X]
hpq : p * q = 0
this : Unique (p * q).Gal
⊢ Function.Injective ⇑(restrictProd p q)

Tactic:
exact fun f g _ => Eq.trans (Unique.eq_default f) (Unique.eq_default g).symm

Result:
no goals
-- Mathlib/Topology/ContinuousMap/ContinuousMapZero.lean
@[fun_prop]
lemma continuous_comp_left {X Y Z : Type*} [TopologicalSpace X]
    [TopologicalSpace Y] [TopologicalSpace Z] [Zero X] [Zero Y] [Zero Z] (f : C(X, Y)₀) :
    Continuous fun g : C(Y, Z)₀ ↦ g.comp f

Proof state:
X : Type u_4
Y : Type u_5
Z : Type u_6
inst✝⁵ : TopologicalSpace X
inst✝⁴ : TopologicalSpace Y
inst✝³ : TopologicalSpace Z
inst✝² : Zero X
inst✝¹ : Zero Y
inst✝ : Zero Z
f : C(X, Y)₀
⊢ Continuous fun g => g.comp f

Tactic:
rw [continuous_induced_rng]

Result:
X : Type u_4
Y : Type u_5
Z : Type u_6
inst✝⁵ : TopologicalSpace X
inst✝⁴ : TopologicalSpace Y
inst✝³ : TopologicalSpace Z
inst✝² : Zero X
inst✝¹ : Zero Y
inst✝ : Zero Z
f : C(X, Y)₀
⊢ Continuous (_root_.toContinuousMap ∘ fun g => g.comp f)

Proof state:
X : Type u_4
Y : Type u_5
Z : Type u_6
inst✝⁵ : TopologicalSpace X
inst✝⁴ : TopologicalSpace Y
inst✝³ : TopologicalSpace Z
inst✝² : Zero X
inst✝¹ : Zero Y
inst✝ : Zero Z
f : C(X, Y)₀
⊢ Continuous fun g => (↑g).comp ↑f

Tactic:
fun_prop

Result:
no goals

Proof state:
X : Type u_4
Y : Type u_5
Z : Type u_6
inst✝⁵ : TopologicalSpace X
inst✝⁴ : TopologicalSpace Y
inst✝³ : TopologicalSpace Z
inst✝² : Zero X
inst✝¹ : Zero Y
inst✝ : Zero Z
f : C(X, Y)₀
⊢ Continuous (_root_.toContinuousMap ∘ fun g => g.comp f)

Tactic:
show Continuous fun g : C(Y, Z)₀ ↦ (g : C(Y, Z)).comp (f : C(X, Y))

Result:
X : Type u_4
Y : Type u_5
Z : Type u_6
inst✝⁵ : TopologicalSpace X
inst✝⁴ : TopologicalSpace Y
inst✝³ : TopologicalSpace Z
inst✝² : Zero X
inst✝¹ : Zero Y
inst✝ : Zero Z
f : C(X, Y)₀
⊢ Continuous fun g => (↑g).comp ↑f
-- Mathlib/Order/RelIso/Set.lean
theorem RelIso.preimage_eq_image_symm (e : r ≃r s) (t : Set β) : e ⁻¹' t = e.symm '' t

Proof state:
α : Type u_1
β : Type u_2
r : α → α → Prop
s : β → β → Prop
e : r ≃r s
t : Set β
⊢ ⇑e ⁻¹' t = ⇑e.symm '' t

Tactic:
rw [e.symm.image_eq_preimage_symm]

Result:
α : Type u_1
β : Type u_2
r : α → α → Prop
s : β → β → Prop
e : r ≃r s
t : Set β
⊢ ⇑e ⁻¹' t = ⇑e.symm.symm ⁻¹' t

Proof state:
α : Type u_1
β : Type u_2
r : α → α → Prop
s : β → β → Prop
e : r ≃r s
t : Set β
⊢ ⇑e ⁻¹' t = ⇑e.symm.symm ⁻¹' t

Tactic:
rfl

Result:
no goals
-- Mathlib/Data/Matroid/Constructions.lean
theorem uniqueBaseOn_dual_eq (I E : Set α) :
    (uniqueBaseOn I E)✶ = uniqueBaseOn (E \ I) E

Proof state:
α : Type u_1
I E B : Set α
hB : B ⊆ E
h : B = E \ I
⊢ E \ B = I ∩ E

Tactic:
rw [h, inter_comm I]

Result:
α : Type u_1
I E B : Set α
hB : B ⊆ E
h : B = E \ I
⊢ E \ (E \ I) = E ∩ I

Proof state:
α : Type u_1
I E B : Set α
hB : B ⊆ E
h : E \ B = I ∩ E
⊢ B = E \ I

Tactic:
rw [← diff_diff_cancel_left hB, h, diff_inter_self_eq_diff]

Result:
no goals

Proof state:
α : Type u_1
I E B : Set α
hB : B ⊆ E
h : B = E \ I
⊢ E \ (E \ I) = E ∩ I

Tactic:
simp

Result:
no goals

Proof state:
α : Type u_1
I E : Set α
⊢ (uniqueBaseOn I E)✶ = uniqueBaseOn (E \ I) E

Tactic:
rw [← uniqueBaseOn_inter_ground_eq]

Result:
α : Type u_1
I E : Set α
⊢ (uniqueBaseOn (I ∩ E) E)✶ = uniqueBaseOn (E \ I) E

Proof state:
α : Type u_1
I E B : Set α
hB : B ⊆ E
⊢ (uniqueBaseOn (I ∩ E) E)✶.IsBase B ↔ (uniqueBaseOn (E \ I) E).IsBase B

Tactic:
rw [dual_isBase_iff, uniqueBaseOn_isBase_iff inter_subset_right,
  uniqueBaseOn_isBase_iff diff_subset, uniqueBaseOn_ground]

Result:
α : Type u_1
I E B : Set α
hB : B ⊆ E
⊢ E \ B = I ∩ E ↔ B = E \ I

Proof state:
α : Type u_1
I E B : Set α
hB : B ⊆ E
⊢ E \ B = I ∩ E ↔ B = E \ I

Tactic:
exact ⟨fun h ↦ by rw [← diff_diff_cancel_left hB, h, diff_inter_self_eq_diff],
  fun h ↦ by rw [h, inter_comm I]; simp⟩

Result:
no goals

Proof state:
α : Type u_1
I E : Set α
⊢ (uniqueBaseOn (I ∩ E) E)✶ = uniqueBaseOn (E \ I) E

Tactic:
refine ext_isBase rfl (fun B (hB : B ⊆ E) ↦ ?_)

Result:
α : Type u_1
I E B : Set α
hB : B ⊆ E
⊢ (uniqueBaseOn (I ∩ E) E)✶.IsBase B ↔ (uniqueBaseOn (E \ I) E).IsBase B
-- Mathlib/Algebra/Module/LocalizedModule/Basic.lean
theorem fromLocalizedModule'_smul (r : R) (x : LocalizedModule S M) :
    r • fromLocalizedModule' S f x = fromLocalizedModule' S f (r • x) :=
  LocalizedModule.induction_on
    (by
      intro a b
      rw [fromLocalizedModule'_mk, LocalizedModule.smul'_mk, fromLocalizedModule'_mk,
        f.map_smul, map_smul])
    x

Proof state:
R : Type u_1
inst✝⁵ : CommSemiring R
S : Submonoid R
M : Type u_2
M' : Type u_3
inst✝⁴ : AddCommMonoid M
inst✝³ : AddCommMonoid M'
inst✝² : Module R M
inst✝¹ : Module R M'
f : M →ₗ[R] M'
inst✝ : IsLocalizedModule S f
r : R
x : LocalizedModule S M
⊢ ∀ (m : M) (s : ↥S),
    r • fromLocalizedModule' S f (LocalizedModule.mk m s) = fromLocalizedModule' S f (r • LocalizedModule.mk m s)

Tactic:
intro a b

Result:
R : Type u_1
inst✝⁵ : CommSemiring R
S : Submonoid R
M : Type u_2
M' : Type u_3
inst✝⁴ : AddCommMonoid M
inst✝³ : AddCommMonoid M'
inst✝² : Module R M
inst✝¹ : Module R M'
f : M →ₗ[R] M'
inst✝ : IsLocalizedModule S f
r : R
x : LocalizedModule S M
a : M
b : ↥S
⊢ r • fromLocalizedModule' S f (LocalizedModule.mk a b) = fromLocalizedModule' S f (r • LocalizedModule.mk a b)

Proof state:
R : Type u_1
inst✝⁵ : CommSemiring R
S : Submonoid R
M : Type u_2
M' : Type u_3
inst✝⁴ : AddCommMonoid M
inst✝³ : AddCommMonoid M'
inst✝² : Module R M
inst✝¹ : Module R M'
f : M →ₗ[R] M'
inst✝ : IsLocalizedModule S f
r : R
x : LocalizedModule S M
a : M
b : ↥S
⊢ r • fromLocalizedModule' S f (LocalizedModule.mk a b) = fromLocalizedModule' S f (r • LocalizedModule.mk a b)

Tactic:
rw [fromLocalizedModule'_mk, LocalizedModule.smul'_mk, fromLocalizedModule'_mk,
  f.map_smul, map_smul]

Result:
no goals
-- Mathlib/GroupTheory/PushoutI.lean
theorem of_comp_eq_base (i : ι) : (of i).comp (φ i) = (base φ)

Proof state:
case h
ι : Type u_1
G : ι → Type u_2
H : Type u_3
inst✝¹ : (i : ι) → Monoid (G i)
inst✝ : Monoid H
φ : (i : ι) → H →* G i
i : ι
x : H
⊢ ∃ i_1 x', (inl.comp CoprodI.of) ((φ i) x) = inl (CoprodI.of ((φ i_1) x')) ∧ inr x = inr x'

Tactic:
simp only [MonoidHom.comp_apply, Set.mem_iUnion, Set.mem_range]

Result:
case h
ι : Type u_1
G : ι → Type u_2
H : Type u_3
inst✝¹ : (i : ι) → Monoid (G i)
inst✝ : Monoid H
φ : (i : ι) → H →* G i
i : ι
x : H
⊢ ∃ i_1 x', inl (CoprodI.of ((φ i) x)) = inl (CoprodI.of ((φ i_1) x')) ∧ inr x = inr x'

Proof state:
case h
ι : Type u_1
G : ι → Type u_2
H : Type u_3
inst✝¹ : (i : ι) → Monoid (G i)
inst✝ : Monoid H
φ : (i : ι) → H →* G i
i : ι
x : H
⊢ ((of i).comp (φ i)) x = (base φ) x

Tactic:
apply (Con.eq _).2

Result:
case h
ι : Type u_1
G : ι → Type u_2
H : Type u_3
inst✝¹ : (i : ι) → Monoid (G i)
inst✝ : Monoid H
φ : (i : ι) → H →* G i
i : ι
x : H
⊢ (con φ) ((inl.comp CoprodI.of) ((φ i) x)) (inr x)

Proof state:
case h
ι : Type u_1
G : ι → Type u_2
H : Type u_3
inst✝¹ : (i : ι) → Monoid (G i)
inst✝ : Monoid H
φ : (i : ι) → H →* G i
i : ι
x : H
⊢ ∃ i_1 x', inl (CoprodI.of ((φ i) x)) = inl (CoprodI.of ((φ i_1) x')) ∧ inr x = inr x'

Tactic:
exact ⟨_, _, rfl, rfl⟩

Result:
no goals

Proof state:
case h
ι : Type u_1
G : ι → Type u_2
H : Type u_3
inst✝¹ : (i : ι) → Monoid (G i)
inst✝ : Monoid H
φ : (i : ι) → H →* G i
i : ι
x : H
⊢ (con φ) ((inl.comp CoprodI.of) ((φ i) x)) (inr x)

Tactic:
refine ConGen.Rel.of _ _ ?_

Result:
case h
ι : Type u_1
G : ι → Type u_2
H : Type u_3
inst✝¹ : (i : ι) → Monoid (G i)
inst✝ : Monoid H
φ : (i : ι) → H →* G i
i : ι
x : H
⊢ ∃ i_1 x', (inl.comp CoprodI.of) ((φ i) x) = inl (CoprodI.of ((φ i_1) x')) ∧ inr x = inr x'

Proof state:
ι : Type u_1
G : ι → Type u_2
H : Type u_3
inst✝¹ : (i : ι) → Monoid (G i)
inst✝ : Monoid H
φ : (i : ι) → H →* G i
i : ι
⊢ (of i).comp (φ i) = base φ

Tactic:
ext x

Result:
case h
ι : Type u_1
G : ι → Type u_2
H : Type u_3
inst✝¹ : (i : ι) → Monoid (G i)
inst✝ : Monoid H
φ : (i : ι) → H →* G i
i : ι
x : H
⊢ ((of i).comp (φ i)) x = (base φ) x