harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/Analysis/NormedSpace/HahnBanach/Separation.lean
theorem separate_convex_open_set [TopologicalSpace E] [AddCommGroup E] [IsTopologicalAddGroup E]
    [Module ℝ E] [ContinuousSMul ℝ E] {s : Set E} (hs₀ : (0 : E) ∈ s) (hs₁ : Convex ℝ s)
    (hs₂ : IsOpen s) {x₀ : E} (hx₀ : x₀ ∉ s) : ∃ f : E →L[ℝ] ℝ, f x₀ = 1 ∧ ∀ x ∈ s, f x < 1

Proof state:
case refine_1.mk.intro
E : Type u_2
inst✝⁴ : TopologicalSpace E
inst✝³ : AddCommGroup E
inst✝² : IsTopologicalAddGroup E
inst✝¹ : Module ℝ E
inst✝ : ContinuousSMul ℝ E
s : Set E
hs₀ : 0 ∈ s
hs₁ : Convex ℝ s
hs₂ : IsOpen s
x₀ : E
hx₀ : x₀ ∉ s
f : E →ₗ.[ℝ] ℝ := LinearPMap.mkSpanSingleton x₀ 1 ⋯
y : ℝ
hx : y • x₀ ∈ f.domain
⊢ y • 1 ≤ gauge s ↑⟨y • x₀, hx⟩

Tactic:
simp only [mul_one, Algebra.id.smul_eq_mul, Submodule.coe_mk]

Result:
case refine_1.mk.intro
E : Type u_2
inst✝⁴ : TopologicalSpace E
inst✝³ : AddCommGroup E
inst✝² : IsTopologicalAddGroup E
inst✝¹ : Module ℝ E
inst✝ : ContinuousSMul ℝ E
s : Set E
hs₀ : 0 ∈ s
hs₁ : Convex ℝ s
hs₂ : IsOpen s
x₀ : E
hx₀ : x₀ ∉ s
f : E →ₗ.[ℝ] ℝ := LinearPMap.mkSpanSingleton x₀ 1 ⋯
y : ℝ
hx : y • x₀ ∈ f.domain
⊢ y ≤ gauge s (y • x₀)

Proof state:
case refine_1.mk.intro.inr
E : Type u_2
inst✝⁴ : TopologicalSpace E
inst✝³ : AddCommGroup E
inst✝² : IsTopologicalAddGroup E
inst✝¹ : Module ℝ E
inst✝ : ContinuousSMul ℝ E
s : Set E
hs₀ : 0 ∈ s
hs₁ : Convex ℝ s
hs₂ : IsOpen s
x₀ : E
hx₀ : x₀ ∉ s
f : E →ₗ.[ℝ] ℝ := LinearPMap.mkSpanSingleton x₀ 1 ⋯
y : ℝ
hx : y • x₀ ∈ f.domain
h : 0 < y
⊢ 1 ≤ gauge s x₀

Tactic:
exact
  one_le_gauge_of_not_mem (hs₁.starConvex hs₀)
    (absorbent_nhds_zero <| hs₂.mem_nhds hs₀).absorbs hx₀

Result:
no goals

Proof state:
case refine_2.intro.intro
E : Type u_2
inst✝⁴ : TopologicalSpace E
inst✝³ : AddCommGroup E
inst✝² : IsTopologicalAddGroup E
inst✝¹ : Module ℝ E
inst✝ : ContinuousSMul ℝ E
s : Set E
hs₀ : 0 ∈ s
hs₁ : Convex ℝ s
hs₂ : IsOpen s
x₀ : E
hx₀ : x₀ ∉ s
f : E →ₗ.[ℝ] ℝ := LinearPMap.mkSpanSingleton x₀ 1 ⋯
φ : E →ₗ[ℝ] ℝ
hφ₁ : ∀ (x : ↥f.domain), φ ↑x = ↑f x
hφ₂ : ∀ (x : E), φ x ≤ gauge s x
hφ₃ : φ x₀ = 1
⊢ ∃ f, f x₀ = 1 ∧ ∀ x ∈ s, f x < 1

Tactic:
have hφ₄ : ∀ x ∈ s, φ x < 1 := fun x hx =>
  (hφ₂ x).trans_lt (gauge_lt_one_of_mem_of_isOpen hs₂ hx)

Result:
case refine_2.intro.intro
E : Type u_2
inst✝⁴ : TopologicalSpace E
inst✝³ : AddCommGroup E
inst✝² : IsTopologicalAddGroup E
inst✝¹ : Module ℝ E
inst✝ : ContinuousSMul ℝ E
s : Set E
hs₀ : 0 ∈ s
hs₁ : Convex ℝ s
hs₂ : IsOpen s
x₀ : E
hx₀ : x₀ ∉ s
f : E →ₗ.[ℝ] ℝ := LinearPMap.mkSpanSingleton x₀ 1 ⋯
φ : E →ₗ[ℝ] ℝ
hφ₁ : ∀ (x : ↥f.domain), φ ↑x = ↑f x
hφ₂ : ∀ (x : E), φ x ≤ gauge s x
hφ₃ : φ x₀ = 1
hφ₄ : ∀ x ∈ s, φ x < 1
⊢ ∃ f, f x₀ = 1 ∧ ∀ x ∈ s, f x < 1
-- Mathlib/MeasureTheory/Integral/IntervalIntegral.lean
theorem integral_comp_mul_left (hc : c ≠ 0) :
    (∫ x in a..b, f (c * x)) = c⁻¹ • ∫ x in c * a..c * b, f x

Proof state:
E : Type u_3
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
a b c : ℝ
f : ℝ → E
hc : c ≠ 0
⊢ ∫ (x : ℝ) in a..b, f (c * x) = c⁻¹ • ∫ (x : ℝ) in c * a..c * b, f x

Tactic:
simpa only [mul_comm c] using integral_comp_mul_right f hc

Result:
no goals
-- Mathlib/NumberTheory/LSeries/Convergence.lean
lemma LSeries.abscissaOfAbsConv_le_of_forall_lt_LSeriesSummable' {f : ℕ → ℂ} {x : EReal}
    (h : ∀ y : ℝ, x < y → LSeriesSummable f y) :
    abscissaOfAbsConv f ≤ x

Proof state:
case h_bot
f : ℕ → ℂ
h : ∀ (y : ℝ), ⊥ < ↑y → LSeriesSummable f ↑y
⊢ abscissaOfAbsConv f ≤ ⊥

Tactic:
refine le_of_eq <| sInf_eq_bot.mpr fun y hy ↦ ?_

Result:
case h_bot
f : ℕ → ℂ
h : ∀ (y : ℝ), ⊥ < ↑y → LSeriesSummable f ↑y
y : EReal
hy : y > ⊥
⊢ ∃ a ∈ Real.toEReal '' {x | LSeriesSummable f ↑x}, a < y

Proof state:
f : ℕ → ℂ
x : EReal
h : ∀ (y : ℝ), x < ↑y → LSeriesSummable f ↑y
⊢ abscissaOfAbsConv f ≤ x

Tactic:
cases x with
| h_real => exact abscissaOfAbsConv_le_of_forall_lt_LSeriesSummable <| mod_cast h
| h_top => exact le_top
| h_bot =>
  refine le_of_eq <| sInf_eq_bot.mpr fun y hy ↦ ?_
  cases y with
  | h_bot => simp at hy
  | h_real y => exact ⟨_,  ⟨_, h _ <| EReal.bot_lt_coe _, rfl⟩, mod_cast sub_one_lt y⟩
  | h_top => exact ⟨_, ⟨_, h _ <| EReal.bot_lt_coe 0, rfl⟩, EReal.zero_lt_top⟩

Result:
no goals

Proof state:
case h_bot.h_bot
f : ℕ → ℂ
h : ∀ (y : ℝ), ⊥ < ↑y → LSeriesSummable f ↑y
hy : ⊥ > ⊥
⊢ ∃ a ∈ Real.toEReal '' {x | LSeriesSummable f ↑x}, a < ⊥

Tactic:
simp at hy

Result:
no goals

Proof state:
case h_bot
f : ℕ → ℂ
h : ∀ (y : ℝ), ⊥ < ↑y → LSeriesSummable f ↑y
y : EReal
hy : y > ⊥
⊢ ∃ a ∈ Real.toEReal '' {x | LSeriesSummable f ↑x}, a < y

Tactic:
cases y with
| h_bot => simp at hy
| h_real y => exact ⟨_,  ⟨_, h _ <| EReal.bot_lt_coe _, rfl⟩, mod_cast sub_one_lt y⟩
| h_top => exact ⟨_, ⟨_, h _ <| EReal.bot_lt_coe 0, rfl⟩, EReal.zero_lt_top⟩

Result:
no goals

Proof state:
case h_bot.h_top
f : ℕ → ℂ
h : ∀ (y : ℝ), ⊥ < ↑y → LSeriesSummable f ↑y
hy : ⊤ > ⊥
⊢ ∃ a ∈ Real.toEReal '' {x | LSeriesSummable f ↑x}, a < ⊤

Tactic:
exact ⟨_, ⟨_, h _ <| EReal.bot_lt_coe 0, rfl⟩, EReal.zero_lt_top⟩

Result:
no goals

Proof state:
case h_top
f : ℕ → ℂ
h : ∀ (y : ℝ), ⊤ < ↑y → LSeriesSummable f ↑y
⊢ abscissaOfAbsConv f ≤ ⊤

Tactic:
exact le_top

Result:
no goals

Proof state:
case h_bot.h_real
f : ℕ → ℂ
h : ∀ (y : ℝ), ⊥ < ↑y → LSeriesSummable f ↑y
y : ℝ
hy : ↑y > ⊥
⊢ ∃ a ∈ Real.toEReal '' {x | LSeriesSummable f ↑x}, a < ↑y

Tactic:
exact ⟨_,  ⟨_, h _ <| EReal.bot_lt_coe _, rfl⟩, mod_cast sub_one_lt y⟩

Result:
no goals

Proof state:
case h_real
f : ℕ → ℂ
a✝ : ℝ
h : ∀ (y : ℝ), ↑a✝ < ↑y → LSeriesSummable f ↑y
⊢ abscissaOfAbsConv f ≤ ↑a✝

Tactic:
exact abscissaOfAbsConv_le_of_forall_lt_LSeriesSummable <| mod_cast h

Result:
no goals
-- Mathlib/Analysis/InnerProductSpace/Basic.lean
theorem real_inner_div_norm_mul_norm_eq_one_of_ne_zero_of_pos_mul {x : F} {r : ℝ} (hx : x ≠ 0)
    (hr : 0 < r) : ⟪x, r • x⟫_ℝ / (‖x‖ * ‖r • x‖) = 1

Proof state:
F : Type u_3
inst✝¹ : NormedAddCommGroup F
inst✝ : InnerProductSpace ℝ F
x : F
r : ℝ
hx : x ≠ 0
hr : 0 < r
⊢ ⟪x, r • x⟫_ℝ / (‖x‖ * ‖r • x‖) = 1

Tactic:
rw [real_inner_smul_self_right, norm_smul, Real.norm_eq_abs, ← mul_assoc ‖x‖, mul_comm _ |r|,
  mul_assoc, abs_of_nonneg hr.le, div_self]

Result:
F : Type u_3
inst✝¹ : NormedAddCommGroup F
inst✝ : InnerProductSpace ℝ F
x : F
r : ℝ
hx : x ≠ 0
hr : 0 < r
⊢ r * (‖x‖ * ‖x‖) ≠ 0

Proof state:
F : Type u_3
inst✝¹ : NormedAddCommGroup F
inst✝ : InnerProductSpace ℝ F
x : F
r : ℝ
hx : x ≠ 0
hr : 0 < r
⊢ r * (‖x‖ * ‖x‖) ≠ 0

Tactic:
exact mul_ne_zero hr.ne' (mul_self_ne_zero.2 (norm_ne_zero_iff.2 hx))

Result:
no goals
-- Mathlib/Topology/Constructible.lean
@[elab_as_elim]
lemma IsConstructible.induction_of_isTopologicalBasis {ι : Type*} [Nonempty ι] (b : ι → Set X)
    (basis : IsTopologicalBasis (range b)) (isCompact_basis : ∀ i, IsCompact (b i))
    (sdiff : ∀ i s (hs : Set.Finite s), P (b i \ ⋃ j ∈ s, b j)
      ((basis.isConstructible isCompact_basis _).sdiff <| .biUnion hs fun _ _ ↦
        basis.isConstructible isCompact_basis _))
    (union : ∀ s hs t ht, P s hs → P t ht → P (s ∪ t) (hs.union ht))
    (s : Set X) (hs : IsConstructible s) : P s hs

Proof state:
case sdiff.intro.intro.intro.intro.insert
X : Type u_2
inst✝³ : TopologicalSpace X
inst✝² : CompactSpace X
P : (s : Set X) → IsConstructible s → Prop
inst✝¹ : QuasiSeparatedSpace X
ι : Type u_4
inst✝ : Nonempty ι
b : ι → Set X
basis : IsTopologicalBasis (range b)
isCompact_basis : ∀ (i : ι), IsCompact (b i)
sdiff : ∀ (i : ι) (s : Set ι) (hs : s.Finite), P (b i \ ⋃ j ∈ s, b j) ⋯
union : ∀ (s : Set X) (hs : IsConstructible s) (t : Set X) (ht : IsConstructible t), P s hs → P t ht → P (s ∪ t) ⋯
s✝¹ : Set X
this : ∀ (U : Set X), IsCompact U ∧ IsOpen U ↔ ∃ s, s.Finite ∧ U = ⋃ i ∈ s, b i
s✝ t : Set ι
ht : t.Finite
hV : ⋃ i ∈ t, b i ∈ {U | IsOpen U ∧ IsRetrocompact U}
i : ι
s : Set ι
hi : i ∉ s
hs : s.Finite
ih : ∀ (hU : ⋃ i ∈ s, b i ∈ {U | IsOpen U ∧ IsRetrocompact U}), P (⋃ i ∈ s, b i \ ⋃ i ∈ t, b i) ⋯
hU : ⋃ i_1 ∈ insert i s, b i_1 ∈ {U | IsOpen U ∧ IsRetrocompact U}
⊢ P (⋃ i_1 ∈ insert i s, b i_1 \ ⋃ i ∈ t, b i) ⋯

Tactic:
simp_rw [biUnion_insert]

Result:
case sdiff.intro.intro.intro.intro.insert
X : Type u_2
inst✝³ : TopologicalSpace X
inst✝² : CompactSpace X
P : (s : Set X) → IsConstructible s → Prop
inst✝¹ : QuasiSeparatedSpace X
ι : Type u_4
inst✝ : Nonempty ι
b : ι → Set X
basis : IsTopologicalBasis (range b)
isCompact_basis : ∀ (i : ι), IsCompact (b i)
sdiff : ∀ (i : ι) (s : Set ι) (hs : s.Finite), P (b i \ ⋃ j ∈ s, b j) ⋯
union : ∀ (s : Set X) (hs : IsConstructible s) (t : Set X) (ht : IsConstructible t), P s hs → P t ht → P (s ∪ t) ⋯
s✝¹ : Set X
this : ∀ (U : Set X), IsCompact U ∧ IsOpen U ↔ ∃ s, s.Finite ∧ U = ⋃ i ∈ s, b i
s✝ t : Set ι
ht : t.Finite
hV : ⋃ i ∈ t, b i ∈ {U | IsOpen U ∧ IsRetrocompact U}
i : ι
s : Set ι
hi : i ∉ s
hs : s.Finite
ih : ∀ (hU : ⋃ i ∈ s, b i ∈ {U | IsOpen U ∧ IsRetrocompact U}), P (⋃ i ∈ s, b i \ ⋃ i ∈ t, b i) ⋯
hU : ⋃ i_1 ∈ insert i s, b i_1 ∈ {U | IsOpen U ∧ IsRetrocompact U}
⊢ P ((b i \ ⋃ i ∈ t, b i) ∪ ⋃ x ∈ s, b x \ ⋃ i ∈ t, b i) ⋯
-- Mathlib/Topology/Algebra/UniformField.lean
theorem mul_hatInv_cancel {x : hat K} (x_ne : x ≠ 0) : x * hatInv x = 1

Proof state:
case intro.intro
K : Type u_1
inst✝⁴ : Field K
inst✝³ : UniformSpace K
inst✝² : TopologicalDivisionRing K
inst✝¹ : CompletableTopField K
inst✝ : UniformAddGroup K
x : hat K
x_ne : x ≠ 0
this : T1Space (hat K)
f : hat K → hat K := fun x => x * x.hatInv
c : K → hat K := fun x => ↑x
cont : ContinuousAt f x
clo : x ∈ closure (c '' {0}ᶜ)
fxclo : f x ∈ closure (f '' (c '' {0}ᶜ))
z : K
z_ne : z ≠ 0
⊢ (fun x => f (c x)) z = 1

Tactic:
dsimp [f]

Result:
case intro.intro
K : Type u_1
inst✝⁴ : Field K
inst✝³ : UniformSpace K
inst✝² : TopologicalDivisionRing K
inst✝¹ : CompletableTopField K
inst✝ : UniformAddGroup K
x : hat K
x_ne : x ≠ 0
this : T1Space (hat K)
f : hat K → hat K := fun x => x * x.hatInv
c : K → hat K := fun x => ↑x
cont : ContinuousAt f x
clo : x ∈ closure (c '' {0}ᶜ)
fxclo : f x ∈ closure (f '' (c '' {0}ᶜ))
z : K
z_ne : z ≠ 0
⊢ c z * (c z).hatInv = 1

Proof state:
K : Type u_1
inst✝⁴ : Field K
inst✝³ : UniformSpace K
inst✝² : TopologicalDivisionRing K
inst✝¹ : CompletableTopField K
inst✝ : UniformAddGroup K
x : hat K
x_ne : x ≠ 0
this : T1Space (hat K)
f : hat K → hat K := fun x => x * x.hatInv
c : K → hat K := fun x => ↑x
cont : ContinuousAt f x
⊢ f x = 1

Tactic:
have clo : x ∈ closure (c '' {0}ᶜ) := by
  have := isDenseInducing_coe.dense x
  rw [← image_univ, show (univ : Set K) = {0} ∪ {0}ᶜ from (union_compl_self _).symm,
    image_union] at this
  apply mem_closure_of_mem_closure_union this
  rw [image_singleton]
  exact compl_singleton_mem_nhds x_ne

Result:
K : Type u_1
inst✝⁴ : Field K
inst✝³ : UniformSpace K
inst✝² : TopologicalDivisionRing K
inst✝¹ : CompletableTopField K
inst✝ : UniformAddGroup K
x : hat K
x_ne : x ≠ 0
this : T1Space (hat K)
f : hat K → hat K := fun x => x * x.hatInv
c : K → hat K := fun x => ↑x
cont : ContinuousAt f x
clo : x ∈ closure (c '' {0}ᶜ)
⊢ f x = 1
-- Mathlib/Order/CompleteBooleanAlgebra.lean
lemma himp_le_iff : a ⇨ b ≤ c ↔ ∀ d, d ⊓ a ≤ b → d ≤ c

Proof state:
α : Type u
inst✝ : Frame α
a b c : α
⊢ a ⇨ b ≤ c ↔ ∀ (d : α), d ⊓ a ≤ b → d ≤ c

Tactic:
simp [himp_eq_sSup]

Result:
no goals
-- Mathlib/NumberTheory/FLT/Three.lean
private lemma three_dvd_b_of_dvd_a_of_gcd_eq_one_of_case2 {a b c : ℤ} (ha : a ≠ 0)
    (Hgcd : Finset.gcd {a, b, c} id = 1) (h3a : 3 ∣ a) (HF : a ^ 3 + b ^ 3 + c ^ 3 = 0)
    (H : ∀ a b c : ℤ, c ≠ 0 → ¬ 3 ∣ a → ¬ 3 ∣ b  → 3 ∣ c → IsCoprime a b → a ^ 3 + b ^ 3 ≠ c ^ 3) :
    3 ∣ b

Proof state:
a b c : ℤ
ha : a ≠ 0
Hgcd : {a, b, c}.gcd id = 1
h3a : 3 ∣ a
HF : a ^ 3 + b ^ 3 + c ^ 3 = 0
H : ∀ (a b c : ℤ), c ≠ 0 → ¬3 ∣ a → ¬3 ∣ b → 3 ∣ c → IsCoprime a b → a ^ 3 + b ^ 3 ≠ c ^ 3
hbc : IsCoprime (-b) (-c)
h3b : ¬3 ∣ b
h3c : ¬3 ∣ c
⊢ ¬3 ∣ -b

Tactic:
simp [h3b]

Result:
no goals

Proof state:
a b c : ℤ
ha : a ≠ 0
Hgcd : {a, b, c}.gcd id = 1
h3a : 3 ∣ a
HF : b ^ 3 + c ^ 3 + a ^ 3 = 0
H : ∀ (a b c : ℤ), c ≠ 0 → ¬3 ∣ a → ¬3 ∣ b → 3 ∣ c → IsCoprime a b → a ^ 3 + b ^ 3 ≠ c ^ 3
⊢ {b, c, a}.gcd id = 1

Tactic:
convert Hgcd using 2

Result:
case h.e'_2.h.e'_5
a b c : ℤ
ha : a ≠ 0
Hgcd : {a, b, c}.gcd id = 1
h3a : 3 ∣ a
HF : b ^ 3 + c ^ 3 + a ^ 3 = 0
H : ∀ (a b c : ℤ), c ≠ 0 → ¬3 ∣ a → ¬3 ∣ b → 3 ∣ c → IsCoprime a b → a ^ 3 + b ^ 3 ≠ c ^ 3
⊢ {b, c, a} = {a, b, c}

Proof state:
a b c : ℤ
ha : a ≠ 0
Hgcd : {a, b, c}.gcd id = 1
h3a : 3 ∣ a
HF : a ^ 3 + b ^ 3 + c ^ 3 = 0
H : ∀ (a b c : ℤ), c ≠ 0 → ¬3 ∣ a → ¬3 ∣ b → 3 ∣ c → IsCoprime a b → a ^ 3 + b ^ 3 ≠ c ^ 3
⊢ IsCoprime (-b) (-c)

Tactic:
refine IsCoprime.neg_neg ?_

Result:
a b c : ℤ
ha : a ≠ 0
Hgcd : {a, b, c}.gcd id = 1
h3a : 3 ∣ a
HF : a ^ 3 + b ^ 3 + c ^ 3 = 0
H : ∀ (a b c : ℤ), c ≠ 0 → ¬3 ∣ a → ¬3 ∣ b → 3 ∣ c → IsCoprime a b → a ^ 3 + b ^ 3 ≠ c ^ 3
⊢ IsCoprime b c
-- Mathlib/AlgebraicGeometry/AffineSpace.lean
@[simp, reassoc]
lemma reindex_comp {n₁ n₂ n₃ : Type v} (i : n₁ → n₂) (j : n₂ → n₃) (S : Scheme.{max u v}) :
    reindex (j ∘ i) S = reindex j S ≫ reindex i S

Proof state:
n₁ n₂ n₃ : Type v
i : n₁ → n₂
j : n₂ → n₃
S : Scheme
H₁ : reindex (j ∘ i) S ≫ 𝔸(n₁; S) ↘ S = (reindex j S ≫ reindex i S) ≫ 𝔸(n₁; S) ↘ S
k : n₁
⊢ coord S ((j ∘ i) k) = coord S (j (i k))

Tactic:
rfl

Result:
no goals

Proof state:
n₁ n₂ n₃ : Type v
i : n₁ → n₂
j : n₂ → n₃
S : Scheme
⊢ reindex (j ∘ i) S = reindex j S ≫ reindex i S

Tactic:
have H₁ : reindex (j ∘ i) S ≫ 𝔸(n₁; S) ↘ S = (reindex j S ≫ reindex i S) ≫ 𝔸(n₁; S) ↘ S := by simp

Result:
n₁ n₂ n₃ : Type v
i : n₁ → n₂
j : n₂ → n₃
S : Scheme
H₁ : reindex (j ∘ i) S ≫ 𝔸(n₁; S) ↘ S = (reindex j S ≫ reindex i S) ≫ 𝔸(n₁; S) ↘ S
⊢ reindex (j ∘ i) S = reindex j S ≫ reindex i S

Proof state:
n₁ n₂ n₃ : Type v
i : n₁ → n₂
j : n₂ → n₃
S : Scheme
H₁ : reindex (j ∘ i) S ≫ 𝔸(n₁; S) ↘ S = (reindex j S ≫ reindex i S) ≫ 𝔸(n₁; S) ↘ S
⊢ reindex (j ∘ i) S = reindex j S ≫ reindex i S

Tactic:
have H₂ (k) : (reindex (j ∘ i) S).appTop (coord S k) =
    (reindex j S).appTop ((reindex i S).appTop (coord S k)) := by
  rw [reindex_appTop_coord, reindex_appTop_coord, reindex_appTop_coord]
  rfl

Result:
n₁ n₂ n₃ : Type v
i : n₁ → n₂
j : n₂ → n₃
S : Scheme
H₁ : reindex (j ∘ i) S ≫ 𝔸(n₁; S) ↘ S = (reindex j S ≫ reindex i S) ≫ 𝔸(n₁; S) ↘ S
H₂ :
  ∀ (k : n₁),
    (ConcreteCategory.hom (Scheme.Hom.appTop (reindex (j ∘ i) S))) (coord S k) =
      (ConcreteCategory.hom (Scheme.Hom.appTop (reindex j S)))
        ((ConcreteCategory.hom (Scheme.Hom.appTop (reindex i S))) (coord S k))
⊢ reindex (j ∘ i) S = reindex j S ≫ reindex i S

Proof state:
n₁ n₂ n₃ : Type v
i : n₁ → n₂
j : n₂ → n₃
S : Scheme
⊢ reindex (j ∘ i) S ≫ 𝔸(n₁; S) ↘ S = (reindex j S ≫ reindex i S) ≫ 𝔸(n₁; S) ↘ S

Tactic:
simp

Result:
no goals

Proof state:
n₁ n₂ n₃ : Type v
i : n₁ → n₂
j : n₂ → n₃
S : Scheme
H₁ : reindex (j ∘ i) S ≫ 𝔸(n₁; S) ↘ S = (reindex j S ≫ reindex i S) ≫ 𝔸(n₁; S) ↘ S
H₂ :
  ∀ (k : n₁),
    (ConcreteCategory.hom (Scheme.Hom.appTop (reindex (j ∘ i) S))) (coord S k) =
      (ConcreteCategory.hom (Scheme.Hom.appTop (reindex j S)))
        ((ConcreteCategory.hom (Scheme.Hom.appTop (reindex i S))) (coord S k))
⊢ reindex (j ∘ i) S = reindex j S ≫ reindex i S

Tactic:
exact hom_ext H₁ H₂

Result:
no goals

Proof state:
n₁ n₂ n₃ : Type v
i : n₁ → n₂
j : n₂ → n₃
S : Scheme
H₁ : reindex (j ∘ i) S ≫ 𝔸(n₁; S) ↘ S = (reindex j S ≫ reindex i S) ≫ 𝔸(n₁; S) ↘ S
k : n₁
⊢ (ConcreteCategory.hom (Scheme.Hom.appTop (reindex (j ∘ i) S))) (coord S k) =
    (ConcreteCategory.hom (Scheme.Hom.appTop (reindex j S)))
      ((ConcreteCategory.hom (Scheme.Hom.appTop (reindex i S))) (coord S k))

Tactic:
rw [reindex_appTop_coord, reindex_appTop_coord, reindex_appTop_coord]

Result:
n₁ n₂ n₃ : Type v
i : n₁ → n₂
j : n₂ → n₃
S : Scheme
H₁ : reindex (j ∘ i) S ≫ 𝔸(n₁; S) ↘ S = (reindex j S ≫ reindex i S) ≫ 𝔸(n₁; S) ↘ S
k : n₁
⊢ coord S ((j ∘ i) k) = coord S (j (i k))
-- Mathlib/Topology/MetricSpace/Dilation.lean
theorem dist_eq {α β F : Type*} [PseudoMetricSpace α] [PseudoMetricSpace β] [FunLike F α β]
    [DilationClass F α β] (f : F) (x y : α) :
    dist (f x) (f y) = ratio f * dist x y

Proof state:
α : Type u_5
β : Type u_6
F : Type u_7
inst✝³ : PseudoMetricSpace α
inst✝² : PseudoMetricSpace β
inst✝¹ : FunLike F α β
inst✝ : DilationClass F α β
f : F
x y : α
⊢ dist (f x) (f y) = ↑(ratio f) * dist x y

Tactic:
simp only [dist_nndist, nndist_eq, NNReal.coe_mul]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Int/Lemmas.lean
theorem add_comm : ∀ a b : Int, a + b = b + a
  | ofNat n, ofNat m => by simp [Nat.add_comm]
  | ofNat _, -[_+1]  => rfl
  | -[_+1],  ofNat _ => rfl
  | -[_+1],  -[_+1]  => by simp [Nat.add_comm]

Proof state:
a✝¹ a✝ : Nat
⊢ -[a✝¹+1] + -[a✝+1] = -[a✝+1] + -[a✝¹+1]

Tactic:
simp [Nat.add_comm]

Result:
no goals

Proof state:
n m : Nat
⊢ ofNat n + ofNat m = ofNat m + ofNat n

Tactic:
simp [Nat.add_comm]

Result:
no goals
-- Mathlib/.lake/packages/batteries/Batteries/Data/HashMap/WF.lean
theorem WF.mk' [BEq α] [Hashable α] (h) : (Buckets.mk n h : Buckets α β).WF

Proof state:
case refine_1
α : Type u_1
β : Type u_2
n : Nat
inst✝³ : BEq α
inst✝² : Hashable α
h✝ : 0 < n
inst✝¹ : LawfulHashable α
inst✝ : PartialEquivBEq α
x✝ : AssocList α β
h : ¬n = 0 ∧ x✝ = AssocList.nil
⊢ List.Pairwise (fun a b => ¬(a.fst == b.fst) = true) x✝.toList

Tactic:
simp [h, List.Pairwise.nil]

Result:
no goals

Proof state:
α : Type u_1
β : Type u_2
n : Nat
inst✝¹ : BEq α
inst✝ : Hashable α
h : 0 < n
⊢ (Buckets.mk n h).WF

Tactic:
refine ⟨fun _ h => ?_, fun i h => ?_⟩

Result:
case refine_1
α : Type u_1
β : Type u_2
n : Nat
inst✝³ : BEq α
inst✝² : Hashable α
h✝ : 0 < n
inst✝¹ : LawfulHashable α
inst✝ : PartialEquivBEq α
x✝ : AssocList α β
h : x✝ ∈ (Buckets.mk n h✝).val.toList
⊢ List.Pairwise (fun a b => ¬(a.fst == b.fst) = true) x✝.toList

case refine_2
α : Type u_1
β : Type u_2
n : Nat
inst✝¹ : BEq α
inst✝ : Hashable α
h✝ : 0 < n
i : Nat
h : i < (Buckets.mk n h✝).val.size
⊢ AssocList.All (fun k x => ((hash k).toUSize % USize.ofNat (Buckets.mk n h✝).val.size).toNat = i)
    (Buckets.mk n h✝).val[i]

Proof state:
case refine_1
α : Type u_1
β : Type u_2
n : Nat
inst✝³ : BEq α
inst✝² : Hashable α
h✝ : 0 < n
inst✝¹ : LawfulHashable α
inst✝ : PartialEquivBEq α
x✝ : AssocList α β
h : x✝ ∈ (Buckets.mk n h✝).val.toList
⊢ List.Pairwise (fun a b => ¬(a.fst == b.fst) = true) x✝.toList

Tactic:
simp only [Buckets.mk, mkArray, List.mem_replicate, ne_eq] at h

Result:
case refine_1
α : Type u_1
β : Type u_2
n : Nat
inst✝³ : BEq α
inst✝² : Hashable α
h✝ : 0 < n
inst✝¹ : LawfulHashable α
inst✝ : PartialEquivBEq α
x✝ : AssocList α β
h : ¬n = 0 ∧ x✝ = AssocList.nil
⊢ List.Pairwise (fun a b => ¬(a.fst == b.fst) = true) x✝.toList

Proof state:
case refine_2
α : Type u_1
β : Type u_2
n : Nat
inst✝¹ : BEq α
inst✝ : Hashable α
h✝ : 0 < n
i : Nat
h : i < (Buckets.mk n h✝).val.size
⊢ AssocList.All (fun k x => ((hash k).toUSize % USize.ofNat (Buckets.mk n h✝).val.size).toNat = i)
    (Buckets.mk n h✝).val[i]

Tactic:
simp [Buckets.mk, empty', Array.getElem_toList, AssocList.All]

Result:
no goals
-- Mathlib/Order/Heyting/Boundary.lean
theorem boundary_inf (a b : α) : ∂ (a ⊓ b) = ∂ a ⊓ b ⊔ a ⊓ ∂ b

Proof state:
α : Type u_1
inst✝ : CoheytingAlgebra α
a b : α
⊢ a ⊓ b ⊓ ￢(a ⊓ b) = a ⊓ ￢a ⊓ b ⊔ a ⊓ (b ⊓ ￢b)

Tactic:
rw [hnot_inf_distrib, inf_sup_left, inf_right_comm, ← inf_assoc]

Result:
no goals

Proof state:
α : Type u_1
inst✝ : CoheytingAlgebra α
a b : α
⊢ ∂ (a ⊓ b) = ∂ a ⊓ b ⊔ a ⊓ ∂ b

Tactic:
unfold boundary

Result:
α : Type u_1
inst✝ : CoheytingAlgebra α
a b : α
⊢ a ⊓ b ⊓ ￢(a ⊓ b) = a ⊓ ￢a ⊓ b ⊔ a ⊓ (b ⊓ ￢b)
-- Mathlib/Data/Finset/Insert.lean
theorem Nontrivial.ne_singleton (hs : s.Nontrivial) : s ≠ {a}

Proof state:
α : Type u_1
s : Finset α
a : α
hs : s.Nontrivial
⊢ s ≠ {a}

Tactic:
rintro rfl

Result:
α : Type u_1
a : α
hs : {a}.Nontrivial
⊢ False

Proof state:
α : Type u_1
a : α
hs : {a}.Nontrivial
⊢ False

Tactic:
exact not_nontrivial_singleton hs

Result:
no goals
-- Mathlib/Geometry/Manifold/MFDeriv/SpecificFunctions.lean
theorem mfderiv_prod_right {x₀ : M} {y₀ : M'} :
    mfderiv I' (I.prod I') (fun y => (x₀, y)) y₀ =
      ContinuousLinearMap.inr 𝕜 (TangentSpace I x₀) (TangentSpace I' y₀)

Proof state:
𝕜 : Type u_1
inst✝¹⁰ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝⁹ : NormedAddCommGroup E
inst✝⁸ : NormedSpace 𝕜 E
H : Type u_3
inst✝⁷ : TopologicalSpace H
I : ModelWithCorners 𝕜 E H
M : Type u_4
inst✝⁶ : TopologicalSpace M
inst✝⁵ : ChartedSpace H M
E' : Type u_5
inst✝⁴ : NormedAddCommGroup E'
inst✝³ : NormedSpace 𝕜 E'
H' : Type u_6
inst✝² : TopologicalSpace H'
I' : ModelWithCorners 𝕜 E' H'
M' : Type u_7
inst✝¹ : TopologicalSpace M'
inst✝ : ChartedSpace H' M'
x₀ : M
y₀ : M'
⊢ (mfderiv I' I (fun x => x₀) y₀).prod (mfderiv I' I' id y₀) =
    ContinuousLinearMap.inr 𝕜 (TangentSpace I x₀) (TangentSpace I' y₀)

Tactic:
rw [mfderiv_id, mfderiv_const, ContinuousLinearMap.inr]

Result:
no goals

Proof state:
𝕜 : Type u_1
inst✝¹⁰ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝⁹ : NormedAddCommGroup E
inst✝⁸ : NormedSpace 𝕜 E
H : Type u_3
inst✝⁷ : TopologicalSpace H
I : ModelWithCorners 𝕜 E H
M : Type u_4
inst✝⁶ : TopologicalSpace M
inst✝⁵ : ChartedSpace H M
E' : Type u_5
inst✝⁴ : NormedAddCommGroup E'
inst✝³ : NormedSpace 𝕜 E'
H' : Type u_6
inst✝² : TopologicalSpace H'
I' : ModelWithCorners 𝕜 E' H'
M' : Type u_7
inst✝¹ : TopologicalSpace M'
inst✝ : ChartedSpace H' M'
x₀ : M
y₀ : M'
⊢ mfderiv I' (I.prod I') (fun y => (x₀, y)) y₀ = ContinuousLinearMap.inr 𝕜 (TangentSpace I x₀) (TangentSpace I' y₀)

Tactic:
refine (mdifferentiableAt_const.mfderiv_prod mdifferentiableAt_id).trans ?_

Result:
𝕜 : Type u_1
inst✝¹⁰ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝⁹ : NormedAddCommGroup E
inst✝⁸ : NormedSpace 𝕜 E
H : Type u_3
inst✝⁷ : TopologicalSpace H
I : ModelWithCorners 𝕜 E H
M : Type u_4
inst✝⁶ : TopologicalSpace M
inst✝⁵ : ChartedSpace H M
E' : Type u_5
inst✝⁴ : NormedAddCommGroup E'
inst✝³ : NormedSpace 𝕜 E'
H' : Type u_6
inst✝² : TopologicalSpace H'
I' : ModelWithCorners 𝕜 E' H'
M' : Type u_7
inst✝¹ : TopologicalSpace M'
inst✝ : ChartedSpace H' M'
x₀ : M
y₀ : M'
⊢ (mfderiv I' I (fun x => x₀) y₀).prod (mfderiv I' I' id y₀) =
    ContinuousLinearMap.inr 𝕜 (TangentSpace I x₀) (TangentSpace I' y₀)
-- Mathlib/MeasureTheory/Measure/Typeclasses.lean
theorem ite_ae_eq_of_measure_compl_zero {γ} (f : α → γ) (g : α → γ)
    (s : Set α) [DecidablePred (· ∈ s)] (hs_zero : μ sᶜ = 0) :
    (fun x => ite (x ∈ s) (f x) (g x)) =ᵐ[μ] f

Proof state:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
γ : Type u_5
f g : α → γ
s : Set α
inst✝ : DecidablePred fun x => x ∈ s
hs_zero : s ∈ ae μ
⊢ (fun x => if x ∈ s then f x else g x) =ᶠ[ae μ] f

Tactic:
filter_upwards [hs_zero]

Result:
case h
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
γ : Type u_5
f g : α → γ
s : Set α
inst✝ : DecidablePred fun x => x ∈ s
hs_zero : s ∈ ae μ
⊢ ∀ a ∈ s, (if a ∈ s then f a else g a) = f a

Proof state:
case h
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
γ : Type u_5
f g : α → γ
s : Set α
inst✝ : DecidablePred fun x => x ∈ s
hs_zero : s ∈ ae μ
⊢ ∀ a ∈ s, (if a ∈ s then f a else g a) = f a

Tactic:
intros

Result:
case h
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
γ : Type u_5
f g : α → γ
s : Set α
inst✝ : DecidablePred fun x => x ∈ s
hs_zero : s ∈ ae μ
a✝¹ : α
a✝ : a✝¹ ∈ s
⊢ (if a✝¹ ∈ s then f a✝¹ else g a✝¹) = f a✝¹

Proof state:
case h
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
γ : Type u_5
f g : α → γ
s : Set α
inst✝ : DecidablePred fun x => x ∈ s
hs_zero : s ∈ ae μ
a✝¹ : α
a✝ : a✝¹ ∈ s
⊢ f a✝¹ = f a✝¹

Tactic:
rfl

Result:
no goals

Proof state:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
γ : Type u_5
f g : α → γ
s : Set α
inst✝ : DecidablePred fun x => x ∈ s
hs_zero : μ sᶜ = 0
⊢ (fun x => if x ∈ s then f x else g x) =ᶠ[ae μ] f

Tactic:
rw [← mem_ae_iff] at hs_zero

Result:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
γ : Type u_5
f g : α → γ
s : Set α
inst✝ : DecidablePred fun x => x ∈ s
hs_zero : s ∈ ae μ
⊢ (fun x => if x ∈ s then f x else g x) =ᶠ[ae μ] f

Proof state:
case h
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
γ : Type u_5
f g : α → γ
s : Set α
inst✝ : DecidablePred fun x => x ∈ s
hs_zero : s ∈ ae μ
a✝¹ : α
a✝ : a✝¹ ∈ s
⊢ (if a✝¹ ∈ s then f a✝¹ else g a✝¹) = f a✝¹

Tactic:
split_ifs

Result:
case h
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
γ : Type u_5
f g : α → γ
s : Set α
inst✝ : DecidablePred fun x => x ∈ s
hs_zero : s ∈ ae μ
a✝¹ : α
a✝ : a✝¹ ∈ s
⊢ f a✝¹ = f a✝¹