harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/FieldTheory/KrullTopology.lean
theorem IntermediateField.fixingSubgroup.bot {K L : Type*} [Field K] [Field L] [Algebra K L] :
    IntermediateField.fixingSubgroup (⊥ : IntermediateField K L) = ⊤

Proof state:
case h.mk
K : Type u_1
L : Type u_2
inst✝² : Field K
inst✝¹ : Field L
inst✝ : Algebra K L
f : L ≃ₐ[K] L
x✝ : f ∈ ⊤
x : L
hx : x ∈ ⊥
⊢ f • ↑⟨x, hx⟩ = ↑⟨x, hx⟩

Tactic:
rw [IntermediateField.mem_bot] at hx

Result:
case h.mk
K : Type u_1
L : Type u_2
inst✝² : Field K
inst✝¹ : Field L
inst✝ : Algebra K L
f : L ≃ₐ[K] L
x✝ : f ∈ ⊤
x : L
hx✝ : x ∈ ⊥
hx : x ∈ Set.range ⇑(algebraMap K L)
⊢ f • ↑⟨x, hx✝⟩ = ↑⟨x, hx✝⟩

Proof state:
case h
K : Type u_1
L : Type u_2
inst✝² : Field K
inst✝¹ : Field L
inst✝ : Algebra K L
f : L ≃ₐ[K] L
x✝ : f ∈ ⊤
⊢ f ∈ ⊥.fixingSubgroup

Tactic:
rintro ⟨x, hx : x ∈ (⊥ : IntermediateField K L)⟩

Result:
case h.mk
K : Type u_1
L : Type u_2
inst✝² : Field K
inst✝¹ : Field L
inst✝ : Algebra K L
f : L ≃ₐ[K] L
x✝ : f ∈ ⊤
x : L
hx : x ∈ ⊥
⊢ f • ↑⟨x, hx⟩ = ↑⟨x, hx⟩

Proof state:
K : Type u_1
L : Type u_2
inst✝² : Field K
inst✝¹ : Field L
inst✝ : Algebra K L
⊢ ⊥.fixingSubgroup = ⊤

Tactic:
ext f

Result:
case h
K : Type u_1
L : Type u_2
inst✝² : Field K
inst✝¹ : Field L
inst✝ : Algebra K L
f : L ≃ₐ[K] L
⊢ f ∈ ⊥.fixingSubgroup ↔ f ∈ ⊤

Proof state:
case h.mk
K : Type u_1
L : Type u_2
inst✝² : Field K
inst✝¹ : Field L
inst✝ : Algebra K L
f : L ≃ₐ[K] L
x✝ : f ∈ ⊤
x : L
hx✝ : x ∈ ⊥
hx : x ∈ Set.range ⇑(algebraMap K L)
⊢ f • ↑⟨x, hx✝⟩ = ↑⟨x, hx✝⟩

Tactic:
rcases hx with ⟨y, rfl⟩

Result:
case h.mk.intro
K : Type u_1
L : Type u_2
inst✝² : Field K
inst✝¹ : Field L
inst✝ : Algebra K L
f : L ≃ₐ[K] L
x✝ : f ∈ ⊤
y : K
hx : (algebraMap K L) y ∈ ⊥
⊢ f • ↑⟨(algebraMap K L) y, hx⟩ = ↑⟨(algebraMap K L) y, hx⟩

Proof state:
case h
K : Type u_1
L : Type u_2
inst✝² : Field K
inst✝¹ : Field L
inst✝ : Algebra K L
f : L ≃ₐ[K] L
⊢ f ∈ ⊥.fixingSubgroup ↔ f ∈ ⊤

Tactic:
refine ⟨fun _ => Subgroup.mem_top _, fun _ => ?_⟩

Result:
case h
K : Type u_1
L : Type u_2
inst✝² : Field K
inst✝¹ : Field L
inst✝ : Algebra K L
f : L ≃ₐ[K] L
x✝ : f ∈ ⊤
⊢ f ∈ ⊥.fixingSubgroup

Proof state:
case h.mk.intro
K : Type u_1
L : Type u_2
inst✝² : Field K
inst✝¹ : Field L
inst✝ : Algebra K L
f : L ≃ₐ[K] L
x✝ : f ∈ ⊤
y : K
hx : (algebraMap K L) y ∈ ⊥
⊢ f • ↑⟨(algebraMap K L) y, hx⟩ = ↑⟨(algebraMap K L) y, hx⟩

Tactic:
exact f.commutes y

Result:
no goals
-- Mathlib/Analysis/LocallyConvex/WithSeminorms.lean
theorem SeminormFamily.withSeminorms_of_nhds [IsTopologicalAddGroup E] (p : SeminormFamily 𝕜 E ι)
    (h : 𝓝 (0 : E) = p.moduleFilterBasis.toFilterBasis.filter) : WithSeminorms p

Proof state:
𝕜 : Type u_1
E : Type u_5
ι : Type u_8
inst✝⁴ : NormedField 𝕜
inst✝³ : AddCommGroup E
inst✝² : Module 𝕜 E
inst✝¹ : Nonempty ι
t : TopologicalSpace E
inst✝ : IsTopologicalAddGroup E
p : SeminormFamily 𝕜 E ι
h : 𝓝 0 = AddGroupFilterBasis.toFilterBasis.filter
⊢ WithSeminorms p

Tactic:
refine
  ⟨IsTopologicalAddGroup.ext inferInstance p.addGroupFilterBasis.isTopologicalAddGroup ?_⟩

Result:
𝕜 : Type u_1
E : Type u_5
ι : Type u_8
inst✝⁴ : NormedField 𝕜
inst✝³ : AddCommGroup E
inst✝² : Module 𝕜 E
inst✝¹ : Nonempty ι
t : TopologicalSpace E
inst✝ : IsTopologicalAddGroup E
p : SeminormFamily 𝕜 E ι
h : 𝓝 0 = AddGroupFilterBasis.toFilterBasis.filter
⊢ 𝓝 0 = 𝓝 0

Proof state:
𝕜 : Type u_1
E : Type u_5
ι : Type u_8
inst✝⁴ : NormedField 𝕜
inst✝³ : AddCommGroup E
inst✝² : Module 𝕜 E
inst✝¹ : Nonempty ι
t : TopologicalSpace E
inst✝ : IsTopologicalAddGroup E
p : SeminormFamily 𝕜 E ι
h : 𝓝 0 = AddGroupFilterBasis.toFilterBasis.filter
⊢ 𝓝 0 = AddGroupFilterBasis.toFilterBasis.filter

Tactic:
exact h

Result:
no goals

Proof state:
𝕜 : Type u_1
E : Type u_5
ι : Type u_8
inst✝⁴ : NormedField 𝕜
inst✝³ : AddCommGroup E
inst✝² : Module 𝕜 E
inst✝¹ : Nonempty ι
t : TopologicalSpace E
inst✝ : IsTopologicalAddGroup E
p : SeminormFamily 𝕜 E ι
h : 𝓝 0 = AddGroupFilterBasis.toFilterBasis.filter
⊢ 𝓝 0 = 𝓝 0

Tactic:
rw [AddGroupFilterBasis.nhds_zero_eq]

Result:
𝕜 : Type u_1
E : Type u_5
ι : Type u_8
inst✝⁴ : NormedField 𝕜
inst✝³ : AddCommGroup E
inst✝² : Module 𝕜 E
inst✝¹ : Nonempty ι
t : TopologicalSpace E
inst✝ : IsTopologicalAddGroup E
p : SeminormFamily 𝕜 E ι
h : 𝓝 0 = AddGroupFilterBasis.toFilterBasis.filter
⊢ 𝓝 0 = AddGroupFilterBasis.toFilterBasis.filter
-- Mathlib/Analysis/NormedSpace/Multilinear/Basic.lean
theorem isLeast_opNorm (f : ContinuousMultilinearMap 𝕜 E G) :
    IsLeast {c : ℝ | 0 ≤ c ∧ ∀ m, ‖f m‖ ≤ c * ∏ i, ‖m i‖} ‖f‖

Proof state:
𝕜 : Type u
ι : Type v
E : ι → Type wE
G : Type wG
inst✝⁵ : NontriviallyNormedField 𝕜
inst✝⁴ : (i : ι) → SeminormedAddCommGroup (E i)
inst✝³ : (i : ι) → NormedSpace 𝕜 (E i)
inst✝² : SeminormedAddCommGroup G
inst✝¹ : NormedSpace 𝕜 G
inst✝ : Fintype ι
f : ContinuousMultilinearMap 𝕜 E G
⊢ IsLeast {c | 0 ≤ c ∧ ∀ (m : (i : ι) → E i), ‖f m‖ ≤ c * ∏ i : ι, ‖m i‖} ‖f‖

Tactic:
refine IsClosed.isLeast_csInf ?_ bounds_nonempty bounds_bddBelow

Result:
𝕜 : Type u
ι : Type v
E : ι → Type wE
G : Type wG
inst✝⁵ : NontriviallyNormedField 𝕜
inst✝⁴ : (i : ι) → SeminormedAddCommGroup (E i)
inst✝³ : (i : ι) → NormedSpace 𝕜 (E i)
inst✝² : SeminormedAddCommGroup G
inst✝¹ : NormedSpace 𝕜 G
inst✝ : Fintype ι
f : ContinuousMultilinearMap 𝕜 E G
⊢ IsClosed {c | 0 ≤ c ∧ ∀ (m : (i : ι) → E i), ‖f m‖ ≤ c * ∏ i : ι, ‖m i‖}

Proof state:
𝕜 : Type u
ι : Type v
E : ι → Type wE
G : Type wG
inst✝⁵ : NontriviallyNormedField 𝕜
inst✝⁴ : (i : ι) → SeminormedAddCommGroup (E i)
inst✝³ : (i : ι) → NormedSpace 𝕜 (E i)
inst✝² : SeminormedAddCommGroup G
inst✝¹ : NormedSpace 𝕜 G
inst✝ : Fintype ι
f : ContinuousMultilinearMap 𝕜 E G
⊢ IsClosed {c | 0 ≤ c ∧ ∀ (m : (i : ι) → E i), ‖f m‖ ≤ c * ∏ i : ι, ‖m i‖}

Tactic:
simp only [Set.setOf_and, Set.setOf_forall]

Result:
𝕜 : Type u
ι : Type v
E : ι → Type wE
G : Type wG
inst✝⁵ : NontriviallyNormedField 𝕜
inst✝⁴ : (i : ι) → SeminormedAddCommGroup (E i)
inst✝³ : (i : ι) → NormedSpace 𝕜 (E i)
inst✝² : SeminormedAddCommGroup G
inst✝¹ : NormedSpace 𝕜 G
inst✝ : Fintype ι
f : ContinuousMultilinearMap 𝕜 E G
⊢ IsClosed ({a | 0 ≤ a} ∩ ⋂ i, {x | ‖f i‖ ≤ x * ∏ i_1 : ι, ‖i i_1‖})

Proof state:
𝕜 : Type u
ι : Type v
E : ι → Type wE
G : Type wG
inst✝⁵ : NontriviallyNormedField 𝕜
inst✝⁴ : (i : ι) → SeminormedAddCommGroup (E i)
inst✝³ : (i : ι) → NormedSpace 𝕜 (E i)
inst✝² : SeminormedAddCommGroup G
inst✝¹ : NormedSpace 𝕜 G
inst✝ : Fintype ι
f : ContinuousMultilinearMap 𝕜 E G
⊢ IsClosed ({a | 0 ≤ a} ∩ ⋂ i, {x | ‖f i‖ ≤ x * ∏ i_1 : ι, ‖i i_1‖})

Tactic:
exact isClosed_Ici.inter (isClosed_iInter fun m ↦
  isClosed_le continuous_const (continuous_id.mul continuous_const))

Result:
no goals
-- Mathlib/Data/Nat/GCD/Basic.lean
theorem gcd_sub_self_left {m n : ℕ} (h : m ≤ n) : gcd (n - m) m = gcd n m

Proof state:
m n : ℕ
h : m ≤ n
⊢ (n - m).gcd m = n.gcd m

Tactic:
calc
  gcd (n - m) m = gcd (n - m + m) m := by rw [← gcd_add_self_left (n - m) m]
              _ = gcd n m := by rw [Nat.sub_add_cancel h]

Result:
no goals

Proof state:
m n : ℕ
h : m ≤ n
⊢ (n - m + m).gcd m = n.gcd m

Tactic:
rw [Nat.sub_add_cancel h]

Result:
no goals

Proof state:
m n : ℕ
h : m ≤ n
⊢ (n - m).gcd m = (n - m + m).gcd m

Tactic:
rw [← gcd_add_self_left (n - m) m]

Result:
no goals
-- Mathlib/Data/ENNReal/Inv.lean
theorem div_pos_iff : 0 < a / b ↔ a ≠ 0 ∧ b ≠ ∞

Proof state:
a b : ℝ≥0∞
⊢ 0 < a / b ↔ a ≠ 0 ∧ b ≠ ⊤

Tactic:
simp [pos_iff_ne_zero, not_or]

Result:
no goals
-- Mathlib/RingTheory/Smooth/Locus.lean
lemma smoothLocus_eq_compl_support_inter [EssFiniteType R A] :
    smoothLocus R A = (Module.support A (H1Cotangent R A))ᶜ ∩ Module.freeLocus A (Ω[A⁄R])

Proof state:
case h.a.h.e'_1.a
R A : Type u
inst✝³ : CommRing R
inst✝² : CommRing A
inst✝¹ : Algebra R A
inst✝ : EssFiniteType R A
p : PrimeSpectrum A
⊢ Subsingleton (H1Cotangent R (Localization.AtPrime p.asIdeal)) ↔
    Subsingleton (LocalizedModule p.asIdeal.primeCompl (H1Cotangent R A))

Tactic:
have := IsLocalizedModule.iso p.asIdeal.primeCompl
  (H1Cotangent.map R R A (Localization.AtPrime p.asIdeal))

Result:
case h.a.h.e'_1.a
R A : Type u
inst✝³ : CommRing R
inst✝² : CommRing A
inst✝¹ : Algebra R A
inst✝ : EssFiniteType R A
p : PrimeSpectrum A
this : LocalizedModule p.asIdeal.primeCompl (H1Cotangent R A) ≃ₗ[A] H1Cotangent R (Localization.AtPrime p.asIdeal)
⊢ Subsingleton (H1Cotangent R (Localization.AtPrime p.asIdeal)) ↔
    Subsingleton (LocalizedModule p.asIdeal.primeCompl (H1Cotangent R A))

Proof state:
case h
R A : Type u
inst✝³ : CommRing R
inst✝² : CommRing A
inst✝¹ : Algebra R A
inst✝ : EssFiniteType R A
p : PrimeSpectrum A
⊢ Subsingleton (H1Cotangent R (Localization.AtPrime p.asIdeal)) ∧
      Module.Projective (Localization.AtPrime p.asIdeal) (Ω[Localization.AtPrime p.asIdeal⁄R]) ↔
    Subsingleton (LocalizedModule p.asIdeal.primeCompl (H1Cotangent R A)) ∧
      Module.Free (Localization.AtPrime p.asIdeal) (LocalizedModule p.asIdeal.primeCompl (Ω[A⁄R]))

Tactic:
congr! 1

Result:
case h.a.h.e'_1.a
R A : Type u
inst✝³ : CommRing R
inst✝² : CommRing A
inst✝¹ : Algebra R A
inst✝ : EssFiniteType R A
p : PrimeSpectrum A
⊢ Subsingleton (H1Cotangent R (Localization.AtPrime p.asIdeal)) ↔
    Subsingleton (LocalizedModule p.asIdeal.primeCompl (H1Cotangent R A))

case h.a.h.e'_2.a
R A : Type u
inst✝³ : CommRing R
inst✝² : CommRing A
inst✝¹ : Algebra R A
inst✝ : EssFiniteType R A
p : PrimeSpectrum A
⊢ Module.Projective (Localization.AtPrime p.asIdeal) (Ω[Localization.AtPrime p.asIdeal⁄R]) ↔
    Module.Free (Localization.AtPrime p.asIdeal) (LocalizedModule p.asIdeal.primeCompl (Ω[A⁄R]))

Proof state:
R A : Type u
inst✝³ : CommRing R
inst✝² : CommRing A
inst✝¹ : Algebra R A
inst✝ : EssFiniteType R A
p : PrimeSpectrum A
⊢ Module.Free (Localization.AtPrime p.asIdeal) (Ω[Localization.AtPrime p.asIdeal⁄R]) ↔
    Module.Free (Localization.AtPrime p.asIdeal) (LocalizedModule p.asIdeal.primeCompl (Ω[A⁄R]))

Tactic:
have := IsLocalizedModule.iso p.asIdeal.primeCompl
  (KaehlerDifferential.map R R A (Localization.AtPrime p.asIdeal))

Result:
R A : Type u
inst✝³ : CommRing R
inst✝² : CommRing A
inst✝¹ : Algebra R A
inst✝ : EssFiniteType R A
p : PrimeSpectrum A
this : LocalizedModule p.asIdeal.primeCompl (Ω[A⁄R]) ≃ₗ[A] Ω[Localization.AtPrime p.asIdeal⁄R]
⊢ Module.Free (Localization.AtPrime p.asIdeal) (Ω[Localization.AtPrime p.asIdeal⁄R]) ↔
    Module.Free (Localization.AtPrime p.asIdeal) (LocalizedModule p.asIdeal.primeCompl (Ω[A⁄R]))
-- Mathlib/CategoryTheory/Sites/NonabelianCohomology/H1.lean
lemma equivalence_isCohomologous :
    _root_.Equivalence (IsCohomologous (G := G) (U := U)) where
  refl γ := ⟨_, OneCohomologyRelation.refl γ.toOneCochain⟩
  symm

Proof state:
case intro
C : Type u
inst✝ : Category.{v, u} C
G : Cᵒᵖ ⥤ Grp
I : Type w'
U : I → C
γ₁ γ₂ : OneCocycle G U
α : ZeroCochain G U
h : OneCohomologyRelation γ₁.toOneCochain γ₂.toOneCochain α
⊢ γ₂.IsCohomologous γ₁

Tactic:
exact ⟨_, h.symm⟩

Result:
no goals

Proof state:
case intro.intro
C : Type u
inst✝ : Category.{v, u} C
G : Cᵒᵖ ⥤ Grp
I : Type w'
U : I → C
γ₁ γ₂✝ γ₂ : OneCocycle G U
α : ZeroCochain G U
h : OneCohomologyRelation γ₁.toOneCochain γ₂✝.toOneCochain α
β : ZeroCochain G U
h' : OneCohomologyRelation γ₂✝.toOneCochain γ₂.toOneCochain β
⊢ γ₁.IsCohomologous γ₂

Tactic:
exact ⟨_, h.trans h'⟩

Result:
no goals

Proof state:
C : Type u
inst✝ : Category.{v, u} C
G : Cᵒᵖ ⥤ Grp
I : Type w'
U : I → C
⊢ ∀ {x y : OneCocycle G U}, x.IsCohomologous y → y.IsCohomologous x

Tactic:
rintro γ₁ γ₂ ⟨α, h⟩

Result:
case intro
C : Type u
inst✝ : Category.{v, u} C
G : Cᵒᵖ ⥤ Grp
I : Type w'
U : I → C
γ₁ γ₂ : OneCocycle G U
α : ZeroCochain G U
h : OneCohomologyRelation γ₁.toOneCochain γ₂.toOneCochain α
⊢ γ₂.IsCohomologous γ₁

Proof state:
C : Type u
inst✝ : Category.{v, u} C
G : Cᵒᵖ ⥤ Grp
I : Type w'
U : I → C
⊢ ∀ {x y z : OneCocycle G U}, x.IsCohomologous y → y.IsCohomologous z → x.IsCohomologous z

Tactic:
rintro γ₁ γ₂ γ₂ ⟨α, h⟩ ⟨β, h'⟩

Result:
case intro.intro
C : Type u
inst✝ : Category.{v, u} C
G : Cᵒᵖ ⥤ Grp
I : Type w'
U : I → C
γ₁ γ₂✝ γ₂ : OneCocycle G U
α : ZeroCochain G U
h : OneCohomologyRelation γ₁.toOneCochain γ₂✝.toOneCochain α
β : ZeroCochain G U
h' : OneCohomologyRelation γ₂✝.toOneCochain γ₂.toOneCochain β
⊢ γ₁.IsCohomologous γ₂
-- Mathlib/MeasureTheory/Measure/Tilted.lean
@[simp]
lemma tilted_neg_same [IsProbabilityMeasure μ] (hf : Integrable (fun x ↦ exp (f x)) μ) :
    (μ.tilted f).tilted (-f) = μ

Proof state:
α : Type u_1
mα : MeasurableSpace α
μ : Measure α
f : α → ℝ
inst✝ : IsProbabilityMeasure μ
hf : Integrable (fun x => rexp (f x)) μ
⊢ (μ.tilted f).tilted (-f) = μ

Tactic:
simp [hf]

Result:
no goals
-- Mathlib/Computability/Primrec.lean
theorem list_range : Primrec List.range :=
  (nat_rec' .id (const []) ((list_concat.comp snd fst).comp snd).to₂).of_eq fun n => by
    simp; induction n <;> simp [*, List.range_succ]

Proof state:
n : ℕ
⊢ Nat.rec [] (fun n IH => IH ++ [n]) n = List.range n

Tactic:
induction n <;> simp [*, List.range_succ]

Result:
no goals

Proof state:
n : ℕ
⊢ Nat.rec [] (fun n_1 IH => (n, n_1, IH).2.2 ++ [(n, n_1, IH).2.1]) (id n) = List.range n

Tactic:
simp

Result:
n : ℕ
⊢ Nat.rec [] (fun n IH => IH ++ [n]) n = List.range n
-- Mathlib/Analysis/Normed/Group/Basic.lean
theorem preimage_mul_ball (a b : E) (r : ℝ) : (b * ·) ⁻¹' ball a r = ball (a / b) r

Proof state:
case h
E : Type u_5
inst✝ : SeminormedCommGroup E
a b : E
r : ℝ
c : E
⊢ c ∈ (fun x => b * x) ⁻¹' ball a r ↔ c ∈ ball (a / b) r

Tactic:
simp only [dist_eq_norm_div, Set.mem_preimage, mem_ball, div_div_eq_mul_div, mul_comm]

Result:
no goals

Proof state:
E : Type u_5
inst✝ : SeminormedCommGroup E
a b : E
r : ℝ
⊢ (fun x => b * x) ⁻¹' ball a r = ball (a / b) r

Tactic:
ext c

Result:
case h
E : Type u_5
inst✝ : SeminormedCommGroup E
a b : E
r : ℝ
c : E
⊢ c ∈ (fun x => b * x) ⁻¹' ball a r ↔ c ∈ ball (a / b) r
-- Mathlib/Topology/Category/TopCat/Limits/Pullbacks.lean
lemma isQuotientMap_of_isColimit_cofork (c : Cofork f g) (hc : IsColimit c) :
    IsQuotientMap c.π

Proof state:
case right
X Y : TopCat
f g : X ⟶ Y
c : Cofork f g
hc : IsColimit c
⊢ ∀ (s : Set ↑(((Functor.const WalkingParallelPair).obj c.pt).obj WalkingParallelPair.one)),
    IsOpen s ↔ IsOpen (⇑(ConcreteCategory.hom c.π) ⁻¹' s)

Tactic:
exact isOpen_iff_of_isColimit_cofork c hc

Result:
no goals

Proof state:
X Y : TopCat
f g : X ⟶ Y
c : Cofork f g
hc : IsColimit c
⊢ IsQuotientMap ⇑(ConcreteCategory.hom c.π)

Tactic:
rw [isQuotientMap_iff]

Result:
X Y : TopCat
f g : X ⟶ Y
c : Cofork f g
hc : IsColimit c
⊢ Function.Surjective ⇑(ConcreteCategory.hom c.π) ∧
    ∀ (s : Set ↑(((Functor.const WalkingParallelPair).obj c.pt).obj WalkingParallelPair.one)),
      IsOpen s ↔ IsOpen (⇑(ConcreteCategory.hom c.π) ⁻¹' s)

Proof state:
case left
X Y : TopCat
f g : X ⟶ Y
c : Cofork f g
hc : IsColimit c
⊢ Function.Surjective ⇑(ConcreteCategory.hom c.π)

Tactic:
simpa only [← epi_iff_surjective] using epi_of_isColimit_cofork hc

Result:
no goals

Proof state:
X Y : TopCat
f g : X ⟶ Y
c : Cofork f g
hc : IsColimit c
⊢ Function.Surjective ⇑(ConcreteCategory.hom c.π) ∧
    ∀ (s : Set ↑(((Functor.const WalkingParallelPair).obj c.pt).obj WalkingParallelPair.one)),
      IsOpen s ↔ IsOpen (⇑(ConcreteCategory.hom c.π) ⁻¹' s)

Tactic:
constructor

Result:
case left
X Y : TopCat
f g : X ⟶ Y
c : Cofork f g
hc : IsColimit c
⊢ Function.Surjective ⇑(ConcreteCategory.hom c.π)

case right
X Y : TopCat
f g : X ⟶ Y
c : Cofork f g
hc : IsColimit c
⊢ ∀ (s : Set ↑(((Functor.const WalkingParallelPair).obj c.pt).obj WalkingParallelPair.one)),
    IsOpen s ↔ IsOpen (⇑(ConcreteCategory.hom c.π) ⁻¹' s)
-- Mathlib/GroupTheory/PushoutI.lean
theorem prod_injective {ι : Type*} {G : ι → Type*} [(i : ι) → Group (G i)] {φ : (i : ι) → H →* G i}
    {d : Transversal φ} : Function.Injective (prod : NormalWord d → PushoutI φ)

Proof state:
H : Type u_3
inst✝¹ : Group H
ι : Type u_5
G : ι → Type u_6
inst✝ : (i : ι) → Group (G i)
φ : (i : ι) → H →* G i
d : Transversal φ
this✝ : DecidableEq ι := Classical.decEq ι
this : (i : ι) → DecidableEq (G i) := fun i => Classical.decEq (G i)
⊢ Injective prod

Tactic:
exact equiv.symm.injective

Result:
no goals

Proof state:
H : Type u_3
inst✝¹ : Group H
ι : Type u_5
G : ι → Type u_6
inst✝ : (i : ι) → Group (G i)
φ : (i : ι) → H →* G i
d : Transversal φ
this : DecidableEq ι := Classical.decEq ι
⊢ Injective prod

Tactic:
letI := fun i => Classical.decEq (G i)

Result:
H : Type u_3
inst✝¹ : Group H
ι : Type u_5
G : ι → Type u_6
inst✝ : (i : ι) → Group (G i)
φ : (i : ι) → H →* G i
d : Transversal φ
this✝ : DecidableEq ι := Classical.decEq ι
this : (i : ι) → DecidableEq (G i) := fun i => Classical.decEq (G i)
⊢ Injective prod

Proof state:
H : Type u_3
inst✝¹ : Group H
ι : Type u_5
G : ι → Type u_6
inst✝ : (i : ι) → Group (G i)
φ : (i : ι) → H →* G i
d : Transversal φ
⊢ Injective prod

Tactic:
letI := Classical.decEq ι

Result:
H : Type u_3
inst✝¹ : Group H
ι : Type u_5
G : ι → Type u_6
inst✝ : (i : ι) → Group (G i)
φ : (i : ι) → H →* G i
d : Transversal φ
this : DecidableEq ι := Classical.decEq ι
⊢ Injective prod

Proof state:
H : Type u_3
inst✝¹ : Group H
ι : Type u_5
G : ι → Type u_6
inst✝ : (i : ι) → Group (G i)
φ : (i : ι) → H →* G i
d : Transversal φ
this✝ : DecidableEq ι := Classical.decEq ι
this : (i : ι) → DecidableEq (G i) := fun i => Classical.decEq (G i)
⊢ Injective prod

Tactic:
classical exact equiv.symm.injective

Result:
no goals
-- Mathlib/.lake/packages/batteries/Batteries/Logic.lean
theorem eqRec_heq_iff_heq {α : Sort _} {a : α} {motive : (a' : α) → a = a' → Sort _}
    {x : motive a rfl} {a' : α} {e : a = a'} {β : Sort _} {y : β} :
    HEq (@Eq.rec α a motive x a' e) y ↔ HEq x y

Proof state:
α : Sort u_1
a : α
motive : (a' : α) → a = a' → Sort u_2
x : motive a ⋯
a' : α
e : a = a'
β : Sort u_2
y : β
⊢ HEq (e ▸ x) y ↔ HEq x y

Tactic:
subst e

Result:
α : Sort u_1
a : α
motive : (a' : α) → a = a' → Sort u_2
x : motive a ⋯
β : Sort u_2
y : β
⊢ HEq (⋯ ▸ x) y ↔ HEq x y

Proof state:
α : Sort u_1
a : α
motive : (a' : α) → a = a' → Sort u_2
x : motive a ⋯
β : Sort u_2
y : β
⊢ HEq (⋯ ▸ x) y ↔ HEq x y

Tactic:
rfl

Result:
no goals
-- Mathlib/CategoryTheory/Iso.lean
theorem of_isIso_fac_left {X Y Z : C} {f : X ⟶ Y} {g : Y ⟶ Z} {h : X ⟶ Z} [IsIso f]
    [hh : IsIso h] (w : f ≫ g = h) : IsIso g

Proof state:
C : Type u
inst✝¹ : Category.{v, u} C
X Y Z : C
f : X ⟶ Y
g : Y ⟶ Z
h : X ⟶ Z
inst✝ : IsIso f
hh : IsIso (f ≫ g)
w : f ≫ g = h
⊢ IsIso g

Tactic:
haveI := hh

Result:
C : Type u
inst✝¹ : Category.{v, u} C
X Y Z : C
f : X ⟶ Y
g : Y ⟶ Z
h : X ⟶ Z
inst✝ : IsIso f
hh : IsIso (f ≫ g)
w : f ≫ g = h
this : IsIso (f ≫ g)
⊢ IsIso g

Proof state:
C : Type u
inst✝¹ : Category.{v, u} C
X Y Z : C
f : X ⟶ Y
g : Y ⟶ Z
h : X ⟶ Z
inst✝ : IsIso f
hh : IsIso h
w : f ≫ g = h
⊢ IsIso g

Tactic:
rw [← w] at hh

Result:
C : Type u
inst✝¹ : Category.{v, u} C
X Y Z : C
f : X ⟶ Y
g : Y ⟶ Z
h : X ⟶ Z
inst✝ : IsIso f
hh : IsIso (f ≫ g)
w : f ≫ g = h
⊢ IsIso g

Proof state:
C : Type u
inst✝¹ : Category.{v, u} C
X Y Z : C
f : X ⟶ Y
g : Y ⟶ Z
h : X ⟶ Z
inst✝ : IsIso f
hh : IsIso (f ≫ g)
w : f ≫ g = h
this : IsIso (f ≫ g)
⊢ IsIso g

Tactic:
exact of_isIso_comp_left f g

Result:
no goals
-- Mathlib/CategoryTheory/HomCongr.lean
theorem homCongr_trans {X₁ Y₁ X₂ Y₂ X₃ Y₃ : C} (α₁ : X₁ ≅ X₂) (β₁ : Y₁ ≅ Y₂) (α₂ : X₂ ≅ X₃)
    (β₂ : Y₂ ≅ Y₃) (f : X₁ ⟶ Y₁) :
    (α₁ ≪≫ α₂).homCongr (β₁ ≪≫ β₂) f = (α₁.homCongr β₁).trans (α₂.homCongr β₂) f

Proof state:
C : Type u
inst✝ : Category.{v, u} C
X₁ Y₁ X₂ Y₂ X₃ Y₃ : C
α₁ : X₁ ≅ X₂
β₁ : Y₁ ≅ Y₂
α₂ : X₂ ≅ X₃
β₂ : Y₂ ≅ Y₃
f : X₁ ⟶ Y₁
⊢ ((α₁ ≪≫ α₂).homCongr (β₁ ≪≫ β₂)) f = ((α₁.homCongr β₁).trans (α₂.homCongr β₂)) f

Tactic:
simp

Result:
no goals
-- Mathlib/NumberTheory/Zsqrtd/Basic.lean
theorem add_le_add_left (a b : ℤ√d) (ab : a ≤ b) (c : ℤ√d) : c + a ≤ c + b :=
  show Nonneg _ by rw [add_sub_add_left_eq_sub]; exact ab

Proof state:
d : ℕ
a b : ℤ√↑d
ab : a ≤ b
c : ℤ√↑d
⊢ (b - a).Nonneg

Tactic:
exact ab

Result:
no goals

Proof state:
d : ℕ
a b : ℤ√↑d
ab : a ≤ b
c : ℤ√↑d
⊢ (c + b - (c + a)).Nonneg

Tactic:
rw [add_sub_add_left_eq_sub]

Result:
d : ℕ
a b : ℤ√↑d
ab : a ≤ b
c : ℤ√↑d
⊢ (b - a).Nonneg
-- Mathlib/Data/PFun.lean
theorem preimage_comp (f : β →. γ) (g : α →. β) (s : Set γ) :
    (f.comp g).preimage s = g.preimage (f.preimage s)

Proof state:
α : Type u_1
β : Type u_2
γ : Type u_3
f : β →. γ
g : α →. β
s : Set γ
⊢ (f.comp g).preimage s = g.preimage (f.preimage s)

Tactic:
ext

Result:
case h
α : Type u_1
β : Type u_2
γ : Type u_3
f : β →. γ
g : α →. β
s : Set γ
x✝ : α
⊢ x✝ ∈ (f.comp g).preimage s ↔ x✝ ∈ g.preimage (f.preimage s)

Proof state:
case h
α : Type u_1
β : Type u_2
γ : Type u_3
f : β →. γ
g : α →. β
s : Set γ
x✝ : α
⊢ (∃ b, ∃ a ∈ s, b ∈ g x✝ ∧ a ∈ f b) ↔ ∃ y x, (x ∈ s ∧ x ∈ f y) ∧ y ∈ g x✝

Tactic:
simp_rw [and_assoc, and_comm]

Result:
no goals

Proof state:
case h
α : Type u_1
β : Type u_2
γ : Type u_3
f : β →. γ
g : α →. β
s : Set γ
x✝ : α
⊢ x✝ ∈ (f.comp g).preimage s ↔ x✝ ∈ g.preimage (f.preimage s)

Tactic:
simp_rw [mem_preimage, comp_apply, Part.mem_bind_iff, ← exists_and_right, ← exists_and_left]

Result:
case h
α : Type u_1
β : Type u_2
γ : Type u_3
f : β →. γ
g : α →. β
s : Set γ
x✝ : α
⊢ (∃ y x, y ∈ s ∧ x ∈ g x✝ ∧ y ∈ f x) ↔ ∃ y x, (x ∈ s ∧ x ∈ f y) ∧ y ∈ g x✝

Proof state:
case h
α : Type u_1
β : Type u_2
γ : Type u_3
f : β →. γ
g : α →. β
s : Set γ
x✝ : α
⊢ (∃ y x, y ∈ s ∧ x ∈ g x✝ ∧ y ∈ f x) ↔ ∃ y x, (x ∈ s ∧ x ∈ f y) ∧ y ∈ g x✝

Tactic:
rw [exists_comm]

Result:
case h
α : Type u_1
β : Type u_2
γ : Type u_3
f : β →. γ
g : α →. β
s : Set γ
x✝ : α
⊢ (∃ b, ∃ a ∈ s, b ∈ g x✝ ∧ a ∈ f b) ↔ ∃ y x, (x ∈ s ∧ x ∈ f y) ∧ y ∈ g x✝
-- Mathlib/Data/Set/Lattice.lean
theorem image_iInter₂ {f : α → β} (hf : Bijective f) (s : ∀ i, κ i → Set α) :
    (f '' ⋂ (i) (j), s i j) = ⋂ (i) (j), f '' s i j

Proof state:
α : Type u_1
β : Type u_2
ι : Sort u_5
κ : ι → Sort u_8
f : α → β
hf : Bijective f
s : (i : ι) → κ i → Set α
⊢ f '' ⋂ i, ⋂ j, s i j = ⋂ i, ⋂ j, f '' s i j

Tactic:
simp_rw [image_iInter hf]

Result:
no goals
-- Mathlib/CategoryTheory/Monoidal/Rigid/Basic.lean
theorem tensorLeftHomEquiv_naturality {X Y Y' Z Z' : C} [ExactPairing Y Y'] (f : Y' ⊗ X ⟶ Z)
    (g : Z ⟶ Z') :
    (tensorLeftHomEquiv X Y Y' Z') (f ≫ g) = (tensorLeftHomEquiv X Y Y' Z) f ≫ Y ◁ g

Proof state:
C : Type u₁
inst✝² : Category.{v₁, u₁} C
inst✝¹ : MonoidalCategory C
X Y Y' Z Z' : C
inst✝ : ExactPairing Y Y'
f : Y' ⊗ X ⟶ Z
g : Z ⟶ Z'
⊢ (tensorLeftHomEquiv X Y Y' Z') (f ≫ g) = (tensorLeftHomEquiv X Y Y' Z) f ≫ Y ◁ g

Tactic:
simp [tensorLeftHomEquiv]

Result:
no goals
-- Mathlib/SetTheory/Cardinal/Cofinality.lean
theorem isStrongLimit_aleph0 : IsStrongLimit ℵ₀ where
  ne_zero := aleph0_ne_zero
  two_power_lt x hx

Proof state:
case intro
n : ℕ
hx : ↑n < ℵ₀
⊢ 2 ^ ↑n < ℵ₀

Tactic:
exact_mod_cast nat_lt_aleph0 _

Result:
no goals

Proof state:
x : Cardinal.{u_1}
hx : x < ℵ₀
⊢ 2 ^ x < ℵ₀

Tactic:
obtain ⟨n, rfl⟩ := lt_aleph0.1 hx

Result:
case intro
n : ℕ
hx : ↑n < ℵ₀
⊢ 2 ^ ↑n < ℵ₀
-- Mathlib/RingTheory/PowerSeries/Basic.lean
@[simp]
lemma polynomial_map_coe {U V : Type*} [CommSemiring U] [CommSemiring V] {φ : U →+* V}
    {f : Polynomial U} : Polynomial.map φ f = PowerSeries.map φ f

Proof state:
U : Type u_2
V : Type u_3
inst✝¹ : CommSemiring U
inst✝ : CommSemiring V
φ : U →+* V
f : U[X]
⊢ ↑(map φ f) = (PowerSeries.map φ) ↑f

Tactic:
ext

Result:
case h
U : Type u_2
V : Type u_3
inst✝¹ : CommSemiring U
inst✝ : CommSemiring V
φ : U →+* V
f : U[X]
n✝ : ℕ
⊢ (PowerSeries.coeff V n✝) ↑(map φ f) = (PowerSeries.coeff V n✝) ((PowerSeries.map φ) ↑f)

Proof state:
case h
U : Type u_2
V : Type u_3
inst✝¹ : CommSemiring U
inst✝ : CommSemiring V
φ : U →+* V
f : U[X]
n✝ : ℕ
⊢ (PowerSeries.coeff V n✝) ↑(map φ f) = (PowerSeries.coeff V n✝) ((PowerSeries.map φ) ↑f)

Tactic:
simp

Result:
no goals