harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/Topology/Algebra/SeparationQuotient/Section.lean
theorem postcomp_mkCLM_surjective {L : Type*} [Semiring L] (σ : L →+* K)
    (F : Type*) [AddCommMonoid F] [Module L F] [TopologicalSpace F] :
    Function.Surjective ((mkCLM K E).comp : (F →SL[σ] E) → (F →SL[σ] SeparationQuotient E))

Proof state:
case h
K : Type u_1
E : Type u_2
inst✝⁹ : DivisionRing K
inst✝⁸ : AddCommGroup E
inst✝⁷ : Module K E
inst✝⁶ : TopologicalSpace E
inst✝⁵ : IsTopologicalAddGroup E
inst✝⁴ : ContinuousConstSMul K E
L : Type u_3
inst✝³ : Semiring L
σ : L →+* K
F : Type u_4
inst✝² : AddCommMonoid F
inst✝¹ : Module L F
inst✝ : TopologicalSpace F
f : F →SL[σ] SeparationQuotient E
⊢ (mkCLM K E).comp ((outCLM K E).comp f) = f

Tactic:
rw [← ContinuousLinearMap.comp_assoc, mkCLM_comp_outCLM, ContinuousLinearMap.id_comp]

Result:
no goals

Proof state:
K : Type u_1
E : Type u_2
inst✝⁹ : DivisionRing K
inst✝⁸ : AddCommGroup E
inst✝⁷ : Module K E
inst✝⁶ : TopologicalSpace E
inst✝⁵ : IsTopologicalAddGroup E
inst✝⁴ : ContinuousConstSMul K E
L : Type u_3
inst✝³ : Semiring L
σ : L →+* K
F : Type u_4
inst✝² : AddCommMonoid F
inst✝¹ : Module L F
inst✝ : TopologicalSpace F
⊢ Function.Surjective (mkCLM K E).comp

Tactic:
intro f

Result:
K : Type u_1
E : Type u_2
inst✝⁹ : DivisionRing K
inst✝⁸ : AddCommGroup E
inst✝⁷ : Module K E
inst✝⁶ : TopologicalSpace E
inst✝⁵ : IsTopologicalAddGroup E
inst✝⁴ : ContinuousConstSMul K E
L : Type u_3
inst✝³ : Semiring L
σ : L →+* K
F : Type u_4
inst✝² : AddCommMonoid F
inst✝¹ : Module L F
inst✝ : TopologicalSpace F
f : F →SL[σ] SeparationQuotient E
⊢ ∃ a, (mkCLM K E).comp a = f

Proof state:
K : Type u_1
E : Type u_2
inst✝⁹ : DivisionRing K
inst✝⁸ : AddCommGroup E
inst✝⁷ : Module K E
inst✝⁶ : TopologicalSpace E
inst✝⁵ : IsTopologicalAddGroup E
inst✝⁴ : ContinuousConstSMul K E
L : Type u_3
inst✝³ : Semiring L
σ : L →+* K
F : Type u_4
inst✝² : AddCommMonoid F
inst✝¹ : Module L F
inst✝ : TopologicalSpace F
f : F →SL[σ] SeparationQuotient E
⊢ ∃ a, (mkCLM K E).comp a = f

Tactic:
use (outCLM K E).comp f

Result:
case h
K : Type u_1
E : Type u_2
inst✝⁹ : DivisionRing K
inst✝⁸ : AddCommGroup E
inst✝⁷ : Module K E
inst✝⁶ : TopologicalSpace E
inst✝⁵ : IsTopologicalAddGroup E
inst✝⁴ : ContinuousConstSMul K E
L : Type u_3
inst✝³ : Semiring L
σ : L →+* K
F : Type u_4
inst✝² : AddCommMonoid F
inst✝¹ : Module L F
inst✝ : TopologicalSpace F
f : F →SL[σ] SeparationQuotient E
⊢ (mkCLM K E).comp ((outCLM K E).comp f) = f
-- Mathlib/RingTheory/Lasker.lean
lemma _root_.InfIrred.isPrimary {I : Ideal R} (h : InfIrred I) : I.IsPrimary

Proof state:
case intro.intro.refine_1
R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsNoetherianRing R
I : Ideal R
a b : R
hab : a * b ∈ I
f : ℕ → Ideal R := fun n => Submodule.colon I (span {b ^ n})
hf : Monotone f
n : ℕ
hn : ∀ (m : ℕ), n ≤ m → { toFun := f, monotone' := hf } n = { toFun := f, monotone' := hf } m
h : ∀ ⦃b c : Ideal R⦄, b ⊓ c = I → b = I ∨ c = I
t s : R
hs : s ∈ I
hrb : (t * b ^ n + s) * b ^ n ∈ I
⊢ t * b ^ n ∈ I

Tactic:
have := hn (n + n) (by simp)

Result:
case intro.intro.refine_1
R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsNoetherianRing R
I : Ideal R
a b : R
hab : a * b ∈ I
f : ℕ → Ideal R := fun n => Submodule.colon I (span {b ^ n})
hf : Monotone f
n : ℕ
hn : ∀ (m : ℕ), n ≤ m → { toFun := f, monotone' := hf } n = { toFun := f, monotone' := hf } m
h : ∀ ⦃b c : Ideal R⦄, b ⊓ c = I → b = I ∨ c = I
t s : R
hs : s ∈ I
hrb : (t * b ^ n + s) * b ^ n ∈ I
this : { toFun := f, monotone' := hf } n = { toFun := f, monotone' := hf } (n + n)
⊢ t * b ^ n ∈ I

Proof state:
R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsNoetherianRing R
I : Ideal R
h : InfIrred I
a b : R
hab : a * b ∈ I
f : ℕ → Ideal R := fun n => Submodule.colon I (span {b ^ n})
n m : ℕ
hnm : n ≤ m
⊢ f n ≤ f m

Tactic:
simp_rw [f]

Result:
R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsNoetherianRing R
I : Ideal R
h : InfIrred I
a b : R
hab : a * b ∈ I
f : ℕ → Ideal R := fun n => Submodule.colon I (span {b ^ n})
n m : ℕ
hnm : n ≤ m
⊢ Submodule.colon I (span {b ^ n}) ≤ Submodule.colon I (span {b ^ m})

Proof state:
case intro.intro.refine_3
R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsNoetherianRing R
I : Ideal R
a b : R
hab : a * b ∈ I
f : ℕ → Ideal R := fun n => Submodule.colon I (span {b ^ n})
hf : Monotone f
n : ℕ
hn : ∀ (m : ℕ), n ≤ m → { toFun := f, monotone' := hf } n = { toFun := f, monotone' := hf } m
h : ∀ ⦃b c : Ideal R⦄, b ⊓ c = I → b = I ∨ c = I
⊢ I ≤ I + span {b ^ n}

Tactic:
simp

Result:
no goals
-- Mathlib/Order/Filter/AtTopBot/Prod.lean
theorem tendsto_atTop_diagonal [Preorder α] : Tendsto (fun a : α => (a, a)) atTop atTop

Proof state:
α : Type u_3
inst✝ : Preorder α
⊢ Tendsto (fun a => (a, a)) atTop (atTop ×ˢ atTop)

Tactic:
exact tendsto_id.prod_mk tendsto_id

Result:
no goals

Proof state:
α : Type u_3
inst✝ : Preorder α
⊢ Tendsto (fun a => (a, a)) atTop atTop

Tactic:
rw [← prod_atTop_atTop_eq]

Result:
α : Type u_3
inst✝ : Preorder α
⊢ Tendsto (fun a => (a, a)) atTop (atTop ×ˢ atTop)
-- Mathlib/Analysis/InnerProductSpace/Basic.lean
theorem eq_of_norm_le_re_inner_eq_norm_sq {x y : E} (hle : ‖x‖ ≤ ‖y‖) (h : re ⟪x, y⟫ = ‖y‖ ^ 2) :
    x = y

Proof state:
𝕜 : Type u_1
E : Type u_2
inst✝² : RCLike 𝕜
inst✝¹ : NormedAddCommGroup E
inst✝ : InnerProductSpace 𝕜 E
x y : E
hle : ‖x‖ ≤ ‖y‖
h : re ⟪x, y⟫_𝕜 = ‖y‖ ^ 2
H₁ : ‖x‖ ^ 2 ≤ ‖y‖ ^ 2
H₂ : re ⟪y, x⟫_𝕜 = ‖y‖ ^ 2
⊢ re ⟪x - y, x - y⟫_𝕜 ≤ 0

Tactic:
simpa [inner_sub_left, inner_sub_right, ← norm_sq_eq_inner, h, H₂] using H₁

Result:
no goals

Proof state:
𝕜 : Type u_1
E : Type u_2
inst✝² : RCLike 𝕜
inst✝¹ : NormedAddCommGroup E
inst✝ : InnerProductSpace 𝕜 E
x y : E
hle : ‖x‖ ≤ ‖y‖
h : re ⟪x, y⟫_𝕜 = ‖y‖ ^ 2
⊢ x = y

Tactic:
suffices H : re ⟪x - y, x - y⟫ ≤ 0 by rwa [inner_self_nonpos, sub_eq_zero] at H

Result:
𝕜 : Type u_1
E : Type u_2
inst✝² : RCLike 𝕜
inst✝¹ : NormedAddCommGroup E
inst✝ : InnerProductSpace 𝕜 E
x y : E
hle : ‖x‖ ≤ ‖y‖
h : re ⟪x, y⟫_𝕜 = ‖y‖ ^ 2
⊢ re ⟪x - y, x - y⟫_𝕜 ≤ 0

Proof state:
𝕜 : Type u_1
E : Type u_2
inst✝² : RCLike 𝕜
inst✝¹ : NormedAddCommGroup E
inst✝ : InnerProductSpace 𝕜 E
x y : E
hle : ‖x‖ ≤ ‖y‖
h : re ⟪x, y⟫_𝕜 = ‖y‖ ^ 2
⊢ re ⟪x - y, x - y⟫_𝕜 ≤ 0

Tactic:
have H₁ : ‖x‖ ^ 2 ≤ ‖y‖ ^ 2 := by gcongr

Result:
𝕜 : Type u_1
E : Type u_2
inst✝² : RCLike 𝕜
inst✝¹ : NormedAddCommGroup E
inst✝ : InnerProductSpace 𝕜 E
x y : E
hle : ‖x‖ ≤ ‖y‖
h : re ⟪x, y⟫_𝕜 = ‖y‖ ^ 2
H₁ : ‖x‖ ^ 2 ≤ ‖y‖ ^ 2
⊢ re ⟪x - y, x - y⟫_𝕜 ≤ 0

Proof state:
𝕜 : Type u_1
E : Type u_2
inst✝² : RCLike 𝕜
inst✝¹ : NormedAddCommGroup E
inst✝ : InnerProductSpace 𝕜 E
x y : E
hle : ‖x‖ ≤ ‖y‖
h : re ⟪x, y⟫_𝕜 = ‖y‖ ^ 2
H₁ : ‖x‖ ^ 2 ≤ ‖y‖ ^ 2
⊢ re ⟪y, x⟫_𝕜 = ‖y‖ ^ 2

Tactic:
rwa [← inner_conj_symm, conj_re]

Result:
no goals

Proof state:
𝕜 : Type u_1
E : Type u_2
inst✝² : RCLike 𝕜
inst✝¹ : NormedAddCommGroup E
inst✝ : InnerProductSpace 𝕜 E
x y : E
hle : ‖x‖ ≤ ‖y‖
h : re ⟪x, y⟫_𝕜 = ‖y‖ ^ 2
H₁ : ‖x‖ ^ 2 ≤ ‖y‖ ^ 2
⊢ re ⟪x - y, x - y⟫_𝕜 ≤ 0

Tactic:
have H₂ : re ⟪y, x⟫ = ‖y‖ ^ 2 := by rwa [← inner_conj_symm, conj_re]

Result:
𝕜 : Type u_1
E : Type u_2
inst✝² : RCLike 𝕜
inst✝¹ : NormedAddCommGroup E
inst✝ : InnerProductSpace 𝕜 E
x y : E
hle : ‖x‖ ≤ ‖y‖
h : re ⟪x, y⟫_𝕜 = ‖y‖ ^ 2
H₁ : ‖x‖ ^ 2 ≤ ‖y‖ ^ 2
H₂ : re ⟪y, x⟫_𝕜 = ‖y‖ ^ 2
⊢ re ⟪x - y, x - y⟫_𝕜 ≤ 0

Proof state:
𝕜 : Type u_1
E : Type u_2
inst✝² : RCLike 𝕜
inst✝¹ : NormedAddCommGroup E
inst✝ : InnerProductSpace 𝕜 E
x y : E
hle : ‖x‖ ≤ ‖y‖
h : re ⟪x, y⟫_𝕜 = ‖y‖ ^ 2
⊢ ‖x‖ ^ 2 ≤ ‖y‖ ^ 2

Tactic:
gcongr

Result:
no goals

Proof state:
𝕜 : Type u_1
E : Type u_2
inst✝² : RCLike 𝕜
inst✝¹ : NormedAddCommGroup E
inst✝ : InnerProductSpace 𝕜 E
x y : E
hle : ‖x‖ ≤ ‖y‖
h : re ⟪x, y⟫_𝕜 = ‖y‖ ^ 2
H : re ⟪x - y, x - y⟫_𝕜 ≤ 0
⊢ x = y

Tactic:
rwa [inner_self_nonpos, sub_eq_zero] at H

Result:
no goals
-- Mathlib/Logic/Equiv/Defs.lean
theorem equivCongr_trans {δ ε ζ} (ab : α ≃ β) (de : δ ≃ ε) (bc : β ≃ γ) (ef : ε ≃ ζ) :
    (ab.equivCongr de).trans (bc.equivCongr ef) = (ab.trans bc).equivCongr (de.trans ef)

Proof state:
α : Sort u
β : Sort v
γ : Sort w
δ : Sort u_1
ε : Sort u_2
ζ : Sort u_3
ab : α ≃ β
de : δ ≃ ε
bc : β ≃ γ
ef : ε ≃ ζ
⊢ (ab.equivCongr de).trans (bc.equivCongr ef) = (ab.trans bc).equivCongr (de.trans ef)

Tactic:
ext

Result:
case H.H
α : Sort u
β : Sort v
γ : Sort w
δ : Sort u_1
ε : Sort u_2
ζ : Sort u_3
ab : α ≃ β
de : δ ≃ ε
bc : β ≃ γ
ef : ε ≃ ζ
x✝¹ : α ≃ δ
x✝ : γ
⊢ (((ab.equivCongr de).trans (bc.equivCongr ef)) x✝¹) x✝ = (((ab.trans bc).equivCongr (de.trans ef)) x✝¹) x✝

Proof state:
case H.H
α : Sort u
β : Sort v
γ : Sort w
δ : Sort u_1
ε : Sort u_2
ζ : Sort u_3
ab : α ≃ β
de : δ ≃ ε
bc : β ≃ γ
ef : ε ≃ ζ
x✝¹ : α ≃ δ
x✝ : γ
⊢ (((ab.equivCongr de).trans (bc.equivCongr ef)) x✝¹) x✝ = (((ab.trans bc).equivCongr (de.trans ef)) x✝¹) x✝

Tactic:
rfl

Result:
no goals
-- Mathlib/Algebra/Ring/Defs.lean
theorem mul_neg_one (a : α) : a * -1 = -a

Proof state:
α : Type u
inst✝¹ : MulOneClass α
inst✝ : HasDistribNeg α
a : α
⊢ a * -1 = -a

Tactic:
simp

Result:
no goals
-- Mathlib/Data/List/Sigma.lean
theorem not_mem_keys_kerase (a) {l : List (Sigma β)} (nd : l.NodupKeys) :
    a ∉ (kerase a l).keys

Proof state:
case cons
α : Type u
β : α → Type v
inst✝ : DecidableEq α
a : α
hd : Sigma β
tl : List (Sigma β)
ih : tl.NodupKeys → a ∉ (kerase a tl).keys
nd : (hd :: tl).NodupKeys
⊢ a ∉ (kerase a (hd :: tl)).keys

Tactic:
simp only [nodupKeys_cons] at nd

Result:
case cons
α : Type u
β : α → Type v
inst✝ : DecidableEq α
a : α
hd : Sigma β
tl : List (Sigma β)
ih : tl.NodupKeys → a ∉ (kerase a tl).keys
nd : hd.fst ∉ tl.keys ∧ tl.NodupKeys
⊢ a ∉ (kerase a (hd :: tl)).keys

Proof state:
case neg
α : Type u
β : α → Type v
inst✝ : DecidableEq α
a : α
hd : Sigma β
tl : List (Sigma β)
ih : tl.NodupKeys → a ∉ (kerase a tl).keys
nd : hd.fst ∉ tl.keys ∧ tl.NodupKeys
h : ¬a = hd.fst
⊢ a ∉ (kerase a (hd :: tl)).keys

Tactic:
simp [h, ih nd.2]

Result:
no goals

Proof state:
case cons
α : Type u
β : α → Type v
inst✝ : DecidableEq α
a : α
hd : Sigma β
tl : List (Sigma β)
ih : tl.NodupKeys → a ∉ (kerase a tl).keys
nd : (hd :: tl).NodupKeys
⊢ a ∉ (kerase a (hd :: tl)).keys

Tactic:
simp? at nd says simp only [nodupKeys_cons] at nd

Result:
case cons
α : Type u
β : α → Type v
inst✝ : DecidableEq α
a : α
hd : Sigma β
tl : List (Sigma β)
ih : tl.NodupKeys → a ∉ (kerase a tl).keys
nd : hd.fst ∉ tl.keys ∧ tl.NodupKeys
⊢ a ∉ (kerase a (hd :: tl)).keys

Proof state:
case cons
α : Type u
β : α → Type v
inst✝ : DecidableEq α
a : α
hd : Sigma β
tl : List (Sigma β)
ih : tl.NodupKeys → a ∉ (kerase a tl).keys
nd : hd.fst ∉ tl.keys ∧ tl.NodupKeys
⊢ a ∉ (kerase a (hd :: tl)).keys

Tactic:
by_cases h : a = hd.1

Result:
case pos
α : Type u
β : α → Type v
inst✝ : DecidableEq α
a : α
hd : Sigma β
tl : List (Sigma β)
ih : tl.NodupKeys → a ∉ (kerase a tl).keys
nd : hd.fst ∉ tl.keys ∧ tl.NodupKeys
h : a = hd.fst
⊢ a ∉ (kerase a (hd :: tl)).keys

case neg
α : Type u
β : α → Type v
inst✝ : DecidableEq α
a : α
hd : Sigma β
tl : List (Sigma β)
ih : tl.NodupKeys → a ∉ (kerase a tl).keys
nd : hd.fst ∉ tl.keys ∧ tl.NodupKeys
h : ¬a = hd.fst
⊢ a ∉ (kerase a (hd :: tl)).keys

Proof state:
case nil
α : Type u
β : α → Type v
inst✝ : DecidableEq α
a : α
nd : [].NodupKeys
⊢ a ∉ (kerase a []).keys

Tactic:
simp

Result:
no goals

Proof state:
case pos
α : Type u
β : α → Type v
inst✝ : DecidableEq α
a : α
hd : Sigma β
tl : List (Sigma β)
ih : tl.NodupKeys → a ∉ (kerase a tl).keys
nd : hd.fst ∉ tl.keys ∧ tl.NodupKeys
h : a = hd.fst
⊢ a ∉ (kerase a (hd :: tl)).keys

Tactic:
subst h

Result:
case pos
α : Type u
β : α → Type v
inst✝ : DecidableEq α
hd : Sigma β
tl : List (Sigma β)
nd : hd.fst ∉ tl.keys ∧ tl.NodupKeys
ih : tl.NodupKeys → hd.fst ∉ (kerase hd.fst tl).keys
⊢ hd.fst ∉ (kerase hd.fst (hd :: tl)).keys

Proof state:
case pos
α : Type u
β : α → Type v
inst✝ : DecidableEq α
hd : Sigma β
tl : List (Sigma β)
nd : hd.fst ∉ tl.keys ∧ tl.NodupKeys
ih : tl.NodupKeys → hd.fst ∉ (kerase hd.fst tl).keys
⊢ hd.fst ∉ (kerase hd.fst (hd :: tl)).keys

Tactic:
simp [nd.1]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Nat/Div/Basic.lean
theorem sub_mod_add_mod_cancel (a b : Nat) [NeZero a] : a - b % a + b % a = a

Proof state:
a b : Nat
inst✝ : NeZero a
⊢ b % a ≤ a

Tactic:
cases a with
| zero => simp_all
| succ a =>
  exact Nat.le_of_lt (mod_lt b (zero_lt_succ a))

Result:
no goals

Proof state:
case succ
b a : Nat
inst✝ : NeZero (a + 1)
⊢ b % (a + 1) ≤ a + 1

Tactic:
exact Nat.le_of_lt (mod_lt b (zero_lt_succ a))

Result:
no goals

Proof state:
a b : Nat
inst✝ : NeZero a
⊢ a - b % a + b % a = a

Tactic:
rw [Nat.sub_add_cancel]

Result:
a b : Nat
inst✝ : NeZero a
⊢ b % a ≤ a

Proof state:
case zero
b : Nat
inst✝ : NeZero 0
⊢ b % 0 ≤ 0

Tactic:
simp_all

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Nat/Fold.lean
theorem allTR_loop_congr {n m : Nat} (w : n = m) (f : (i : Nat) → i < n → Bool) (j : Nat) (h : j ≤ n) : allTR.loop n f j h = allTR.loop m (fun i h => f i (by omega)) j (by omega)

Proof state:
n m : Nat
w : n = m
f : (i : Nat) → i < n → Bool
j : Nat
h : j ≤ n
⊢ j ≤ m

Tactic:
omega

Result:
no goals

Proof state:
n m : Nat
w : n = m
f : (i : Nat) → i < n → Bool
j : Nat
h : j ≤ n
⊢ allTR.loop n f j h = allTR.loop m (fun i h => f i ⋯) j ⋯

Tactic:
subst m

Result:
n : Nat
f : (i : Nat) → i < n → Bool
j : Nat
h : j ≤ n
⊢ allTR.loop n f j h = allTR.loop n (fun i h => f i ⋯) j ⋯

Proof state:
n : Nat
f : (i : Nat) → i < n → Bool
j : Nat
h : j ≤ n
⊢ allTR.loop n f j h = allTR.loop n (fun i h => f i ⋯) j ⋯

Tactic:
rfl

Result:
no goals

Proof state:
n m : Nat
w : n = m
f : (i : Nat) → i < n → Bool
j : Nat
h✝ : j ≤ n
i : Nat
h : i < m
⊢ i < n

Tactic:
omega

Result:
no goals
-- Mathlib/AlgebraicGeometry/RationalMap.lean
lemma RationalMap.eq_of_fromFunctionField_eq [IsIntegral X] (f g : X.RationalMap Y)
    (H : f.fromFunctionField = g.fromFunctionField) : f = g

Proof state:
case intro.intro
X Y : Scheme
inst✝ : IsIntegral X
f g : X.PartialMap Y
H : f.toRationalMap.fromFunctionField = g.toRationalMap.fromFunctionField
⊢ f.toRationalMap = g.toRationalMap

Tactic:
refine PartialMap.toRationalMap_eq_iff.mpr ?_

Result:
case intro.intro
X Y : Scheme
inst✝ : IsIntegral X
f g : X.PartialMap Y
H : f.toRationalMap.fromFunctionField = g.toRationalMap.fromFunctionField
⊢ f.equiv g

Proof state:
case intro.intro
X Y : Scheme
inst✝ : IsIntegral X
f g : X.PartialMap Y
H : f.toRationalMap.fromFunctionField = g.toRationalMap.fromFunctionField
⊢ f.equiv g

Tactic:
exact PartialMap.equiv_of_fromSpecStalkOfMem_eq _ _ _ _ H

Result:
no goals

Proof state:
X Y : Scheme
inst✝ : IsIntegral X
f g : X ⤏ Y
H : f.fromFunctionField = g.fromFunctionField
⊢ f = g

Tactic:
obtain ⟨f, rfl⟩ := f.exists_rep

Result:
case intro
X Y : Scheme
inst✝ : IsIntegral X
g : X ⤏ Y
f : X.PartialMap Y
H : f.toRationalMap.fromFunctionField = g.fromFunctionField
⊢ f.toRationalMap = g

Proof state:
case intro
X Y : Scheme
inst✝ : IsIntegral X
g : X ⤏ Y
f : X.PartialMap Y
H : f.toRationalMap.fromFunctionField = g.fromFunctionField
⊢ f.toRationalMap = g

Tactic:
obtain ⟨g, rfl⟩ := g.exists_rep

Result:
case intro.intro
X Y : Scheme
inst✝ : IsIntegral X
f g : X.PartialMap Y
H : f.toRationalMap.fromFunctionField = g.toRationalMap.fromFunctionField
⊢ f.toRationalMap = g.toRationalMap
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/List/Pairwise.lean
theorem Pairwise.imp_of_mem {S : α → α → Prop}
    (H : ∀ {a b}, a ∈ l → b ∈ l → R a b → S a b) (p : Pairwise R l) : Pairwise S l

Proof state:
case nil
α : Type u_1
l : List α
R S : α → α → Prop
H : ∀ {a b : α}, a ∈ [] → b ∈ [] → R a b → S a b
⊢ Pairwise S []

Tactic:
constructor

Result:
no goals

Proof state:
case cons
α : Type u_1
l✝ : List α
R S : α → α → Prop
a : α
l : List α
r : ∀ (a' : α), a' ∈ l → R a a'
a✝ : Pairwise R l
ih : (∀ {a b : α}, a ∈ l → b ∈ l → R a b → S a b) → Pairwise S l
H : ∀ {a_1 b : α}, a_1 ∈ a :: l → b ∈ a :: l → R a_1 b → S a_1 b
⊢ Pairwise S (a :: l)

Tactic:
constructor

Result:
case cons.a
α : Type u_1
l✝ : List α
R S : α → α → Prop
a : α
l : List α
r : ∀ (a' : α), a' ∈ l → R a a'
a✝ : Pairwise R l
ih : (∀ {a b : α}, a ∈ l → b ∈ l → R a b → S a b) → Pairwise S l
H : ∀ {a_1 b : α}, a_1 ∈ a :: l → b ∈ a :: l → R a_1 b → S a_1 b
⊢ ∀ (a' : α), a' ∈ l → S a a'

case cons.a
α : Type u_1
l✝ : List α
R S : α → α → Prop
a : α
l : List α
r : ∀ (a' : α), a' ∈ l → R a a'
a✝ : Pairwise R l
ih : (∀ {a b : α}, a ∈ l → b ∈ l → R a b → S a b) → Pairwise S l
H : ∀ {a_1 b : α}, a_1 ∈ a :: l → b ∈ a :: l → R a_1 b → S a_1 b
⊢ Pairwise S l

Proof state:
case cons.a
α : Type u_1
l✝ : List α
R S : α → α → Prop
a : α
l : List α
r : ∀ (a' : α), a' ∈ l → R a a'
a✝ : Pairwise R l
ih : (∀ {a b : α}, a ∈ l → b ∈ l → R a b → S a b) → Pairwise S l
H : ∀ {a_1 b : α}, a_1 ∈ a :: l → b ∈ a :: l → R a_1 b → S a_1 b
⊢ Pairwise S l

Tactic:
exact ih fun m m' => H (mem_cons_of_mem _ m) (mem_cons_of_mem _ m')

Result:
no goals

Proof state:
case cons.a
α : Type u_1
l✝ : List α
R S : α → α → Prop
a : α
l : List α
r : ∀ (a' : α), a' ∈ l → R a a'
a✝ : Pairwise R l
ih : (∀ {a b : α}, a ∈ l → b ∈ l → R a b → S a b) → Pairwise S l
H : ∀ {a_1 b : α}, a_1 ∈ a :: l → b ∈ a :: l → R a_1 b → S a_1 b
⊢ ∀ (a' : α), a' ∈ l → S a a'

Tactic:
exact fun x h => H (mem_cons_self ..) (mem_cons_of_mem _ h) <| r x h

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Array/Find.lean
theorem idxOf?_eq_map_finIdxOf?_val [BEq α] {xs : Array α} {a : α} :
    xs.idxOf? a = (xs.finIdxOf? a).map (·.val)

Proof state:
α : Type u_1
inst✝ : BEq α
xs : Array α
a : α
⊢ xs.idxOf? a = Option.map (fun x => ↑x) (xs.finIdxOf? a)

Tactic:
simp [idxOf?, finIdxOf?, findIdx?_eq_map_findFinIdx?_val]

Result:
no goals
-- Mathlib/Analysis/Normed/Group/Seminorm.lean
theorem mul_bddBelow_range_add {p q : GroupSeminorm E} {x : E} :
    BddBelow (range fun y => p y + q (x / y)) :=
  ⟨0, by
    rintro _ ⟨x, rfl⟩
    dsimp
    positivity⟩

Proof state:
E : Type u_3
inst✝ : CommGroup E
p q : GroupSeminorm E
x : E
⊢ 0 ∈ lowerBounds (range fun y => p y + q (x / y))

Tactic:
rintro _ ⟨x, rfl⟩

Result:
case intro
E : Type u_3
inst✝ : CommGroup E
p q : GroupSeminorm E
x✝ x : E
⊢ 0 ≤ (fun y => p y + q (x✝ / y)) x

Proof state:
case intro
E : Type u_3
inst✝ : CommGroup E
p q : GroupSeminorm E
x✝ x : E
⊢ 0 ≤ (fun y => p y + q (x✝ / y)) x

Tactic:
dsimp

Result:
case intro
E : Type u_3
inst✝ : CommGroup E
p q : GroupSeminorm E
x✝ x : E
⊢ 0 ≤ p x + q (x✝ / x)

Proof state:
case intro
E : Type u_3
inst✝ : CommGroup E
p q : GroupSeminorm E
x✝ x : E
⊢ 0 ≤ p x + q (x✝ / x)

Tactic:
positivity

Result:
no goals
-- Mathlib/Order/Interval/Finset/Basic.lean
theorem right_mem_Ioc : b ∈ Ioc a b ↔ a < b

Proof state:
α : Type u_2
a b : α
inst✝¹ : Preorder α
inst✝ : LocallyFiniteOrder α
⊢ b ∈ Ioc a b ↔ a < b

Tactic:
simp only [mem_Ioc, and_true, le_rfl]

Result:
no goals
-- Mathlib/GroupTheory/EckmannHilton.lean
theorem mul_assoc : Std.Associative m₂ :=
  ⟨fun a b c => by simpa [mul h₁ h₂ distrib, h₂.left_id, h₂.right_id] using distrib a b e₂ c⟩

Proof state:
X : Type u
m₁ m₂ : X → X → X
e₁ e₂ : X
h₁ : IsUnital m₁ e₁
h₂ : IsUnital m₂ e₂
distrib : ∀ (a b c d : X), m₁ (m₂ a b) (m₂ c d) = m₂ (m₁ a c) (m₁ b d)
a b c : X
⊢ m₂ (m₂ a b) c = m₂ a (m₂ b c)

Tactic:
simpa [mul h₁ h₂ distrib, h₂.left_id, h₂.right_id] using distrib a b e₂ c

Result:
no goals
-- Mathlib/FieldTheory/Laurent.lean
theorem laurent_laurent : laurent r (laurent s f) = laurent (r + s) f

Proof state:
case f
R : Type u
inst✝¹ : CommRing R
r s : R
f : RatFunc R
inst✝ : IsDomain R
p✝ q✝ : R[X]
x✝ : q✝ ≠ 0
⊢ (laurent r) ((laurent s) ((algebraMap R[X] (RatFunc R)) p✝ / (algebraMap R[X] (RatFunc R)) q✝)) =
    (laurent (r + s)) ((algebraMap R[X] (RatFunc R)) p✝ / (algebraMap R[X] (RatFunc R)) q✝)

Tactic:
simp_rw [laurent_div, taylor_taylor]

Result:
no goals

Proof state:
R : Type u
inst✝¹ : CommRing R
r s : R
f : RatFunc R
inst✝ : IsDomain R
⊢ (laurent r) ((laurent s) f) = (laurent (r + s)) f

Tactic:
induction f using RatFunc.induction_on

Result:
case f
R : Type u
inst✝¹ : CommRing R
r s : R
f : RatFunc R
inst✝ : IsDomain R
p✝ q✝ : R[X]
x✝ : q✝ ≠ 0
⊢ (laurent r) ((laurent s) ((algebraMap R[X] (RatFunc R)) p✝ / (algebraMap R[X] (RatFunc R)) q✝)) =
    (laurent (r + s)) ((algebraMap R[X] (RatFunc R)) p✝ / (algebraMap R[X] (RatFunc R)) q✝)
-- Mathlib/Analysis/Normed/Group/Seminorm.lean
theorem toZeroHom_eq_coe : ⇑p.toZeroHom = p

Proof state:
E : Type u_3
inst✝ : AddGroup E
p : NonarchAddGroupSeminorm E
⊢ ⇑p.toZeroHom = ⇑p

Tactic:
rfl

Result:
no goals
-- Mathlib/CategoryTheory/Limits/Shapes/Kernels.lean
theorem kernelIsoOfEq_refl {h : f = f} : kernelIsoOfEq h = Iso.refl (kernel f)

Proof state:
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : HasZeroMorphisms C
X Y : C
f : X ⟶ Y
inst✝ : HasKernel f
h : f = f
⊢ kernelIsoOfEq h = Iso.refl (kernel f)

Tactic:
ext

Result:
case w.h
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : HasZeroMorphisms C
X Y : C
f : X ⟶ Y
inst✝ : HasKernel f
h : f = f
⊢ (kernelIsoOfEq h).hom ≫ equalizer.ι f 0 = (Iso.refl (kernel f)).hom ≫ equalizer.ι f 0

Proof state:
case w.h
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : HasZeroMorphisms C
X Y : C
f : X ⟶ Y
inst✝ : HasKernel f
h : f = f
⊢ (kernelIsoOfEq h).hom ≫ equalizer.ι f 0 = (Iso.refl (kernel f)).hom ≫ equalizer.ι f 0

Tactic:
simp [kernelIsoOfEq]

Result:
no goals
-- Mathlib/Data/Real/Sqrt.lean
theorem sqrt_eq_cases : √x = y ↔ y * y = x ∧ 0 ≤ y ∨ x < 0 ∧ y = 0

Proof state:
case mpr
x y : ℝ
⊢ y * y = x ∧ 0 ≤ y ∨ x < 0 ∧ y = 0 → √x = y

Tactic:
rintro (⟨rfl, hy⟩ | ⟨hx, rfl⟩)

Result:
case mpr.inl.intro
y : ℝ
hy : 0 ≤ y
⊢ √(y * y) = y

case mpr.inr.intro
x : ℝ
hx : x < 0
⊢ √x = 0

Proof state:
case mp
x : ℝ
⊢ √x * √x = x ∧ 0 ≤ √x ∨ x < 0 ∧ √x = 0

Tactic:
rcases le_or_lt 0 x with hle | hlt

Result:
case mp.inl
x : ℝ
hle : 0 ≤ x
⊢ √x * √x = x ∧ 0 ≤ √x ∨ x < 0 ∧ √x = 0

case mp.inr
x : ℝ
hlt : x < 0
⊢ √x * √x = x ∧ 0 ≤ √x ∨ x < 0 ∧ √x = 0

Proof state:
case mpr.inl.intro
y : ℝ
hy : 0 ≤ y
⊢ √(y * y) = y

case mpr.inr.intro
x : ℝ
hx : x < 0
⊢ √x = 0

Tactic:
exacts [sqrt_mul_self hy, sqrt_eq_zero_of_nonpos hx.le]

Result:
no goals

Proof state:
case mp.inr
x : ℝ
hlt : x < 0
⊢ √x * √x = x ∧ 0 ≤ √x ∨ x < 0 ∧ √x = 0

Tactic:
exact Or.inr ⟨hlt, sqrt_eq_zero_of_nonpos hlt.le⟩

Result:
no goals

Proof state:
case mp.inl
x : ℝ
hle : 0 ≤ x
⊢ √x * √x = x ∧ 0 ≤ √x ∨ x < 0 ∧ √x = 0

Tactic:
exact Or.inl ⟨mul_self_sqrt hle, sqrt_nonneg x⟩

Result:
no goals

Proof state:
case mp
x y : ℝ
⊢ √x = y → y * y = x ∧ 0 ≤ y ∨ x < 0 ∧ y = 0

Tactic:
rintro rfl

Result:
case mp
x : ℝ
⊢ √x * √x = x ∧ 0 ≤ √x ∨ x < 0 ∧ √x = 0

Proof state:
x y : ℝ
⊢ √x = y ↔ y * y = x ∧ 0 ≤ y ∨ x < 0 ∧ y = 0

Tactic:
constructor

Result:
case mp
x y : ℝ
⊢ √x = y → y * y = x ∧ 0 ≤ y ∨ x < 0 ∧ y = 0

case mpr
x y : ℝ
⊢ y * y = x ∧ 0 ≤ y ∨ x < 0 ∧ y = 0 → √x = y
-- Mathlib/Analysis/NormedSpace/PiTensorProduct/InjectiveSeminorm.lean
theorem toDualContinuousMultilinearMap_le_projectiveSeminorm (x : ⨂[𝕜] i, E i) :
    ‖toDualContinuousMultilinearMap F x‖ ≤ projectiveSeminorm x

Proof state:
ι : Type uι
inst✝⁵ : Fintype ι
𝕜 : Type u𝕜
inst✝⁴ : NontriviallyNormedField 𝕜
E : ι → Type uE
inst✝³ : (i : ι) → SeminormedAddCommGroup (E i)
inst✝² : (i : ι) → NormedSpace 𝕜 (E i)
F : Type uF
inst✝¹ : SeminormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
x : ⨂[𝕜] (i : ι), E i
⊢ ‖(toDualContinuousMultilinearMap F) x‖ ≤ projectiveSeminorm x

Tactic:
simp only [toDualContinuousMultilinearMap, LinearMap.coe_mk, AddHom.coe_mk]

Result:
ι : Type uι
inst✝⁵ : Fintype ι
𝕜 : Type u𝕜
inst✝⁴ : NontriviallyNormedField 𝕜
E : ι → Type uE
inst✝³ : (i : ι) → SeminormedAddCommGroup (E i)
inst✝² : (i : ι) → NormedSpace 𝕜 (E i)
F : Type uF
inst✝¹ : SeminormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
x : ⨂[𝕜] (i : ι), E i
⊢ ‖((↑lift).flip x ∘ₗ ContinuousMultilinearMap.toMultilinearMapLinear).mkContinuous (projectiveSeminorm x) ⋯‖ ≤
    projectiveSeminorm x

Proof state:
ι : Type uι
inst✝⁵ : Fintype ι
𝕜 : Type u𝕜
inst✝⁴ : NontriviallyNormedField 𝕜
E : ι → Type uE
inst✝³ : (i : ι) → SeminormedAddCommGroup (E i)
inst✝² : (i : ι) → NormedSpace 𝕜 (E i)
F : Type uF
inst✝¹ : SeminormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
x : ⨂[𝕜] (i : ι), E i
⊢ ‖((↑lift).flip x ∘ₗ ContinuousMultilinearMap.toMultilinearMapLinear).mkContinuous (projectiveSeminorm x) ⋯‖ ≤
    projectiveSeminorm x

Tactic:
apply LinearMap.mkContinuous_norm_le _ (apply_nonneg _ _)

Result:
no goals