harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/NumberTheory/Padics/RingHoms.lean
theorem ker_toZMod : RingHom.ker (toZMod : ℤ_[p] →+* ZMod p) = maximalIdeal ℤ_[p]

Proof state:
case h.mpr.convert_2
p : ℕ
hp_prime : Fact (Nat.Prime p)
x : ℤ_[p]
h : x - 0 ∈ maximalIdeal ℤ_[p]
⊢ x - ↑x.zmodRepr ∈ maximalIdeal ℤ_[p]

Tactic:
apply sub_zmodRepr_mem

Result:
no goals

Proof state:
case h
p : ℕ
hp_prime : Fact (Nat.Prime p)
x : ℤ_[p]
⊢ toZMod x = 0 ↔ x ∈ maximalIdeal ℤ_[p]

Tactic:
constructor

Result:
case h.mp
p : ℕ
hp_prime : Fact (Nat.Prime p)
x : ℤ_[p]
⊢ toZMod x = 0 → x ∈ maximalIdeal ℤ_[p]

case h.mpr
p : ℕ
hp_prime : Fact (Nat.Prime p)
x : ℤ_[p]
⊢ x ∈ maximalIdeal ℤ_[p] → toZMod x = 0

Proof state:
case h.mpr
p : ℕ
hp_prime : Fact (Nat.Prime p)
x : ℤ_[p]
h : x - 0 ∈ maximalIdeal ℤ_[p]
⊢ toZMod x = 0

Tactic:
dsimp [toZMod, toZModHom]

Result:
case h.mpr
p : ℕ
hp_prime : Fact (Nat.Prime p)
x : ℤ_[p]
h : x - 0 ∈ maximalIdeal ℤ_[p]
⊢ ↑x.zmodRepr = 0

Proof state:
case h.mp
p : ℕ
hp_prime : Fact (Nat.Prime p)
x : ℤ_[p]
h : toZMod x = 0
⊢ x ∈ maximalIdeal ℤ_[p]

Tactic:
simpa only [h, ZMod.cast_zero, sub_zero] using toZMod_spec x

Result:
no goals

Proof state:
p : ℕ
hp_prime : Fact (Nat.Prime p)
⊢ RingHom.ker toZMod = maximalIdeal ℤ_[p]

Tactic:
ext x

Result:
case h
p : ℕ
hp_prime : Fact (Nat.Prime p)
x : ℤ_[p]
⊢ x ∈ RingHom.ker toZMod ↔ x ∈ maximalIdeal ℤ_[p]

Proof state:
case h.mp
p : ℕ
hp_prime : Fact (Nat.Prime p)
x : ℤ_[p]
⊢ toZMod x = 0 → x ∈ maximalIdeal ℤ_[p]

Tactic:
intro h

Result:
case h.mp
p : ℕ
hp_prime : Fact (Nat.Prime p)
x : ℤ_[p]
h : toZMod x = 0
⊢ x ∈ maximalIdeal ℤ_[p]

Proof state:
case h.mpr
p : ℕ
hp_prime : Fact (Nat.Prime p)
x : ℤ_[p]
h : x ∈ maximalIdeal ℤ_[p]
⊢ toZMod x = 0

Tactic:
rw [← sub_zero x] at h

Result:
case h.mpr
p : ℕ
hp_prime : Fact (Nat.Prime p)
x : ℤ_[p]
h : x - 0 ∈ maximalIdeal ℤ_[p]
⊢ toZMod x = 0

Proof state:
case h
p : ℕ
hp_prime : Fact (Nat.Prime p)
x : ℤ_[p]
⊢ x ∈ RingHom.ker toZMod ↔ x ∈ maximalIdeal ℤ_[p]

Tactic:
rw [RingHom.mem_ker]

Result:
case h
p : ℕ
hp_prime : Fact (Nat.Prime p)
x : ℤ_[p]
⊢ toZMod x = 0 ↔ x ∈ maximalIdeal ℤ_[p]

Proof state:
case h.mpr
p : ℕ
hp_prime : Fact (Nat.Prime p)
x : ℤ_[p]
⊢ x ∈ maximalIdeal ℤ_[p] → toZMod x = 0

Tactic:
intro h

Result:
case h.mpr
p : ℕ
hp_prime : Fact (Nat.Prime p)
x : ℤ_[p]
h : x ∈ maximalIdeal ℤ_[p]
⊢ toZMod x = 0

Proof state:
case h.mpr
p : ℕ
hp_prime : Fact (Nat.Prime p)
x : ℤ_[p]
h : x - 0 ∈ maximalIdeal ℤ_[p]
⊢ ↑x.zmodRepr = 0

Tactic:
convert zmod_congr_of_sub_mem_max_ideal x _ 0 _ h

Result:
case h.e'_3
p : ℕ
hp_prime : Fact (Nat.Prime p)
x : ℤ_[p]
h : x - 0 ∈ maximalIdeal ℤ_[p]
⊢ 0 = ↑0

case h.mpr.convert_2
p : ℕ
hp_prime : Fact (Nat.Prime p)
x : ℤ_[p]
h : x - 0 ∈ maximalIdeal ℤ_[p]
⊢ x - ↑x.zmodRepr ∈ maximalIdeal ℤ_[p]

Proof state:
case h.e'_3
p : ℕ
hp_prime : Fact (Nat.Prime p)
x : ℤ_[p]
h : x - 0 ∈ maximalIdeal ℤ_[p]
⊢ 0 = ↑0

Tactic:
norm_cast

Result:
no goals
-- Mathlib/AlgebraicTopology/FundamentalGroupoid/InducedMaps.lean
theorem heq_path_of_eq_image :
    HEq ((πₘ (TopCat.ofHom f)).map ⟦p⟧) ((πₘ (TopCat.ofHom g)).map ⟦q⟧)

Proof state:
case hp
X₁ X₂ Y : TopCat
f : C(↑X₁, ↑Y)
g : C(↑X₂, ↑Y)
x₀ x₁ : ↑X₁
x₂ x₃ : ↑X₂
p : Path x₀ x₁
q : Path x₂ x₃
hfg : ∀ (t : ↑I), f (p t) = g (q t)
⊢ ∀ (t : ↑I), (p.map ⋯) t = (q.map ⋯) t

Tactic:
exact hfg

Result:
no goals

Proof state:
X₁ X₂ Y : TopCat
f : C(↑X₁, ↑Y)
g : C(↑X₂, ↑Y)
x₀ x₁ : ↑X₁
x₂ x₃ : ↑X₂
p : Path x₀ x₁
q : Path x₂ x₃
hfg : ∀ (t : ↑I), f (p t) = g (q t)
⊢ HEq ⟦p.map ⋯⟧ ⟦q.map ⋯⟧

Tactic:
apply Path.Homotopic.hpath_hext

Result:
case hp
X₁ X₂ Y : TopCat
f : C(↑X₁, ↑Y)
g : C(↑X₂, ↑Y)
x₀ x₁ : ↑X₁
x₂ x₃ : ↑X₂
p : Path x₀ x₁
q : Path x₂ x₃
hfg : ∀ (t : ↑I), f (p t) = g (q t)
⊢ ∀ (t : ↑I), (p.map ⋯) t = (q.map ⋯) t

Proof state:
X₁ X₂ Y : TopCat
f : C(↑X₁, ↑Y)
g : C(↑X₂, ↑Y)
x₀ x₁ : ↑X₁
x₂ x₃ : ↑X₂
p : Path x₀ x₁
q : Path x₂ x₃
hfg : ∀ (t : ↑I), f (p t) = g (q t)
⊢ HEq ((π.map (TopCat.ofHom f)).map ⟦p⟧) ((π.map (TopCat.ofHom g)).map ⟦q⟧)

Tactic:
simp only [map_eq, ← Path.Homotopic.map_lift]

Result:
X₁ X₂ Y : TopCat
f : C(↑X₁, ↑Y)
g : C(↑X₂, ↑Y)
x₀ x₁ : ↑X₁
x₂ x₃ : ↑X₂
p : Path x₀ x₁
q : Path x₂ x₃
hfg : ∀ (t : ↑I), f (p t) = g (q t)
⊢ HEq ⟦p.map ⋯⟧ ⟦q.map ⋯⟧
-- Mathlib/Algebra/Order/Floor.lean
theorem floor_eq_iff : ⌊a⌋ = z ↔ ↑z ≤ a ∧ a < z + 1

Proof state:
α : Type u_2
inst✝¹ : LinearOrderedRing α
inst✝ : FloorRing α
z : ℤ
a : α
⊢ ⌊a⌋ = z ↔ ↑z ≤ a ∧ a < ↑z + 1

Tactic:
rw [le_antisymm_iff, le_floor, ← Int.lt_add_one_iff, floor_lt, Int.cast_add, Int.cast_one,
  and_comm]

Result:
no goals
-- Mathlib/Algebra/Lie/Submodule.lean
theorem map_le_iff_le_comap : map f I ≤ J ↔ I ≤ comap f J

Proof state:
R : Type u
L : Type v
L' : Type w₂
inst✝⁴ : CommRing R
inst✝³ : LieRing L
inst✝² : LieRing L'
inst✝¹ : LieAlgebra R L'
inst✝ : LieAlgebra R L
f : L →ₗ⁅R⁆ L'
I : LieIdeal R L
J : LieIdeal R L'
⊢ map f I ≤ J ↔ I ≤ comap f J

Tactic:
rw [map_le]

Result:
R : Type u
L : Type v
L' : Type w₂
inst✝⁴ : CommRing R
inst✝³ : LieRing L
inst✝² : LieRing L'
inst✝¹ : LieAlgebra R L'
inst✝ : LieAlgebra R L
f : L →ₗ⁅R⁆ L'
I : LieIdeal R L
J : LieIdeal R L'
⊢ ⇑f '' ↑I ⊆ ↑J ↔ I ≤ comap f J

Proof state:
R : Type u
L : Type v
L' : Type w₂
inst✝⁴ : CommRing R
inst✝³ : LieRing L
inst✝² : LieRing L'
inst✝¹ : LieAlgebra R L'
inst✝ : LieAlgebra R L
f : L →ₗ⁅R⁆ L'
I : LieIdeal R L
J : LieIdeal R L'
⊢ ⇑f '' ↑I ⊆ ↑J ↔ I ≤ comap f J

Tactic:
exact Set.image_subset_iff

Result:
no goals
-- Mathlib/MeasureTheory/Integral/Asymptotics.lean
theorem IsBigO.set_integral_isBigO
    (hf : f =O[𝓟 s ×ˢ l] (g ∘ Prod.snd)) (hs : MeasurableSet s) (hμ : μ s < ⊤)  :
    (fun x ↦ ∫ i in s, f (i, x) ∂μ) =O[l] g

Proof state:
case intro.intro.intro.intro.intro.intro.intro
α : Type u_1
E : Type u_2
F : Type u_3
inst✝³ : NormedAddCommGroup E
g : α → F
l : Filter α
ι : Type u_4
inst✝² : MeasurableSpace ι
f : ι × α → E
s : Set ι
μ : Measure ι
inst✝¹ : NormedSpace ℝ E
inst✝ : NormedAddCommGroup F
hf : f =O[𝓟 s ×ˢ l] (g ∘ Prod.snd)
hs : MeasurableSet s
hμ : μ s < ⊤
C : ℝ
hC : ∀ᶠ (x : ι × α) in 𝓟 s ×ˢ l, ‖f x‖ ≤ C * ‖(g ∘ Prod.snd) x‖
t : Set (ι × α)
htl : t ∈ 𝓟 s ×ˢ l
ht : ∀ y ∈ t, ‖f y‖ ≤ C * ‖(g ∘ Prod.snd) y‖
u : Set ι
hu : u ∈ 𝓟 s
v : Set α
hv : v ∈ l
huv : u ×ˢ v ⊆ t
x : α
hx : x ∈ v
this : IsFiniteMeasure (μ.restrict s)
⊢ (fun a => ‖f (a, x)‖) ≤ᶠ[ae (μ.restrict s)] fun x_1 => ‖g x‖ • C

Tactic:
filter_upwards [MeasureTheory.self_mem_ae_restrict hs]

Result:
case h
α : Type u_1
E : Type u_2
F : Type u_3
inst✝³ : NormedAddCommGroup E
g : α → F
l : Filter α
ι : Type u_4
inst✝² : MeasurableSpace ι
f : ι × α → E
s : Set ι
μ : Measure ι
inst✝¹ : NormedSpace ℝ E
inst✝ : NormedAddCommGroup F
hf : f =O[𝓟 s ×ˢ l] (g ∘ Prod.snd)
hs : MeasurableSet s
hμ : μ s < ⊤
C : ℝ
hC : ∀ᶠ (x : ι × α) in 𝓟 s ×ˢ l, ‖f x‖ ≤ C * ‖(g ∘ Prod.snd) x‖
t : Set (ι × α)
htl : t ∈ 𝓟 s ×ˢ l
ht : ∀ y ∈ t, ‖f y‖ ≤ C * ‖(g ∘ Prod.snd) y‖
u : Set ι
hu : u ∈ 𝓟 s
v : Set α
hv : v ∈ l
huv : u ×ˢ v ⊆ t
x : α
hx : x ∈ v
this : IsFiniteMeasure (μ.restrict s)
⊢ ∀ a ∈ s, ‖f (a, x)‖ ≤ ‖g x‖ • C
-- Mathlib/RingTheory/MvPolynomial/Symmetric/Defs.lean
theorem esymm_isSymmetric (n : ℕ) : IsSymmetric (esymm σ R n)

Proof state:
σ : Type u_5
R : Type u_6
inst✝¹ : CommSemiring R
inst✝ : Fintype σ
n : ℕ
e✝ : Perm σ
⊢ (rename ⇑e✝) (esymm σ R n) = esymm σ R n

Tactic:
rw [rename_esymm]

Result:
no goals

Proof state:
σ : Type u_5
R : Type u_6
inst✝¹ : CommSemiring R
inst✝ : Fintype σ
n : ℕ
⊢ (esymm σ R n).IsSymmetric

Tactic:
intro

Result:
σ : Type u_5
R : Type u_6
inst✝¹ : CommSemiring R
inst✝ : Fintype σ
n : ℕ
e✝ : Perm σ
⊢ (rename ⇑e✝) (esymm σ R n) = esymm σ R n
-- Mathlib/RingTheory/LocalRing/Basic.lean
theorem of_surjective' [Ring S] [Nontrivial S] (f : R →+* S) (hf : Function.Surjective f) :
    IsLocalRing S :=
  of_isUnit_or_isUnit_one_sub_self (by
    intro b
    obtain ⟨a, rfl⟩ := hf b
    apply (isUnit_or_isUnit_one_sub_self a).imp <| RingHom.isUnit_map _
    rw [← f.map_one, ← f.map_sub]
    apply f.isUnit_map)

Proof state:
R : Type u_1
S : Type u_2
inst✝³ : CommRing R
inst✝² : IsLocalRing R
inst✝¹ : Ring S
inst✝ : Nontrivial S
f : R →+* S
hf : Function.Surjective ⇑f
⊢ ∀ (a : S), IsUnit a ∨ IsUnit (1 - a)

Tactic:
intro b

Result:
R : Type u_1
S : Type u_2
inst✝³ : CommRing R
inst✝² : IsLocalRing R
inst✝¹ : Ring S
inst✝ : Nontrivial S
f : R →+* S
hf : Function.Surjective ⇑f
b : S
⊢ IsUnit b ∨ IsUnit (1 - b)

Proof state:
R : Type u_1
S : Type u_2
inst✝³ : CommRing R
inst✝² : IsLocalRing R
inst✝¹ : Ring S
inst✝ : Nontrivial S
f : R →+* S
hf : Function.Surjective ⇑f
b : S
⊢ IsUnit b ∨ IsUnit (1 - b)

Tactic:
obtain ⟨a, rfl⟩ := hf b

Result:
case intro
R : Type u_1
S : Type u_2
inst✝³ : CommRing R
inst✝² : IsLocalRing R
inst✝¹ : Ring S
inst✝ : Nontrivial S
f : R →+* S
hf : Function.Surjective ⇑f
a : R
⊢ IsUnit (f a) ∨ IsUnit (1 - f a)

Proof state:
case intro
R : Type u_1
S : Type u_2
inst✝³ : CommRing R
inst✝² : IsLocalRing R
inst✝¹ : Ring S
inst✝ : Nontrivial S
f : R →+* S
hf : Function.Surjective ⇑f
a : R
⊢ IsUnit (1 - a) → IsUnit (1 - f a)

Tactic:
rw [← f.map_one, ← f.map_sub]

Result:
case intro
R : Type u_1
S : Type u_2
inst✝³ : CommRing R
inst✝² : IsLocalRing R
inst✝¹ : Ring S
inst✝ : Nontrivial S
f : R →+* S
hf : Function.Surjective ⇑f
a : R
⊢ IsUnit (1 - a) → IsUnit (f (1 - a))

Proof state:
case intro
R : Type u_1
S : Type u_2
inst✝³ : CommRing R
inst✝² : IsLocalRing R
inst✝¹ : Ring S
inst✝ : Nontrivial S
f : R →+* S
hf : Function.Surjective ⇑f
a : R
⊢ IsUnit (1 - a) → IsUnit (f (1 - a))

Tactic:
apply f.isUnit_map

Result:
no goals

Proof state:
case intro
R : Type u_1
S : Type u_2
inst✝³ : CommRing R
inst✝² : IsLocalRing R
inst✝¹ : Ring S
inst✝ : Nontrivial S
f : R →+* S
hf : Function.Surjective ⇑f
a : R
⊢ IsUnit (f a) ∨ IsUnit (1 - f a)

Tactic:
apply (isUnit_or_isUnit_one_sub_self a).imp <| RingHom.isUnit_map _

Result:
case intro
R : Type u_1
S : Type u_2
inst✝³ : CommRing R
inst✝² : IsLocalRing R
inst✝¹ : Ring S
inst✝ : Nontrivial S
f : R →+* S
hf : Function.Surjective ⇑f
a : R
⊢ IsUnit (1 - a) → IsUnit (1 - f a)
-- Mathlib/Order/SymmDiff.lean
theorem symmDiff_symmDiff_self' : a ∆ b ∆ a = b

Proof state:
α : Type u_2
inst✝ : GeneralizedBooleanAlgebra α
a b : α
⊢ a ∆ b ∆ a = b

Tactic:
rw [symmDiff_comm, symmDiff_symmDiff_cancel_left]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Bool.lean
theorem true_bne  : ∀(b : Bool), (true  != b) = !b

Proof state:
⊢ ∀ (b : Bool), (true != b) = !b

Tactic:
decide

Result:
no goals
-- Mathlib/GroupTheory/SpecificGroups/Dihedral.lean
theorem r_one_pow_n : r (1 : ZMod n) ^ n = 1

Proof state:
n : ℕ
⊢ r 1 ^ n = 1

Tactic:
simp

Result:
no goals
-- Mathlib/Data/Subtype.lean
theorem surjective_restrict {α} {β : α → Type*} [ne : ∀ a, Nonempty (β a)] (p : α → Prop) :
    Surjective fun f : ∀ x, β x ↦ restrict p f

Proof state:
α : Sort u_5
β : α → Type u_4
ne : ∀ (a : α), Nonempty (β a)
p : α → Prop
this : DecidablePred p := Classical.decPred p
f : (x : Subtype p) → β ↑x
⊢ ∀ (x : Subtype p), (fun f => restrict p f) (fun x => if h : p x then f ⟨x, h⟩ else ⋯.some) x = f x

Tactic:
rintro ⟨x, hx⟩

Result:
case mk
α : Sort u_5
β : α → Type u_4
ne : ∀ (a : α), Nonempty (β a)
p : α → Prop
this : DecidablePred p := Classical.decPred p
f : (x : Subtype p) → β ↑x
x : α
hx : p x
⊢ (fun f => restrict p f) (fun x => if h : p x then f ⟨x, h⟩ else ⋯.some) ⟨x, hx⟩ = f ⟨x, hx⟩

Proof state:
α : Sort u_5
β : α → Type u_4
ne : ∀ (a : α), Nonempty (β a)
p : α → Prop
this : DecidablePred p := Classical.decPred p
⊢ Surjective fun f => restrict p f

Tactic:
refine fun f ↦ ⟨fun x ↦ if h : p x then f ⟨x, h⟩ else Nonempty.some (ne x), funext <| ?_⟩

Result:
α : Sort u_5
β : α → Type u_4
ne : ∀ (a : α), Nonempty (β a)
p : α → Prop
this : DecidablePred p := Classical.decPred p
f : (x : Subtype p) → β ↑x
⊢ ∀ (x : Subtype p), (fun f => restrict p f) (fun x => if h : p x then f ⟨x, h⟩ else ⋯.some) x = f x

Proof state:
α : Sort u_5
β : α → Type u_4
ne : ∀ (a : α), Nonempty (β a)
p : α → Prop
⊢ Surjective fun f => restrict p f

Tactic:
letI := Classical.decPred p

Result:
α : Sort u_5
β : α → Type u_4
ne : ∀ (a : α), Nonempty (β a)
p : α → Prop
this : DecidablePred p := Classical.decPred p
⊢ Surjective fun f => restrict p f

Proof state:
case mk
α : Sort u_5
β : α → Type u_4
ne : ∀ (a : α), Nonempty (β a)
p : α → Prop
this : DecidablePred p := Classical.decPred p
f : (x : Subtype p) → β ↑x
x : α
hx : p x
⊢ (fun f => restrict p f) (fun x => if h : p x then f ⟨x, h⟩ else ⋯.some) ⟨x, hx⟩ = f ⟨x, hx⟩

Tactic:
exact dif_pos hx

Result:
no goals
-- Mathlib/Analysis/Convex/Function.lean
theorem StrictConvexOn.convex_lt (hf : StrictConvexOn 𝕜 s f) (r : β) :
    Convex 𝕜 ({ x ∈ s | f x < r }) :=
  convex_iff_pairwise_pos.2 fun x hx y hy hxy a b ha hb hab =>
    ⟨hf.1 hx.1 hy.1 ha.le hb.le hab,
      calc
        f (a • x + b • y) < a • f x + b • f y := hf.2 hx.1 hy.1 hxy ha hb hab
        _ ≤ a • r + b • r

Proof state:
case h₁.hb
𝕜 : Type u_1
E : Type u_2
β : Type u_5
inst✝⁵ : OrderedSemiring 𝕜
inst✝⁴ : AddCommMonoid E
inst✝³ : OrderedAddCommMonoid β
inst✝² : Module 𝕜 E
inst✝¹ : Module 𝕜 β
inst✝ : OrderedSMul 𝕜 β
s : Set E
f : E → β
hf : StrictConvexOn 𝕜 s f
r : β
x : E
hx : x ∈ {x | x ∈ s ∧ f x < r}
y : E
hy : y ∈ {x | x ∈ s ∧ f x < r}
hxy : x ≠ y
a b : 𝕜
ha : 0 < a
hb : 0 < b
hab : a + b = 1
⊢ f x ≤ r

Tactic:
exact hx.2.le

Result:
no goals

Proof state:
case h₂.hb
𝕜 : Type u_1
E : Type u_2
β : Type u_5
inst✝⁵ : OrderedSemiring 𝕜
inst✝⁴ : AddCommMonoid E
inst✝³ : OrderedAddCommMonoid β
inst✝² : Module 𝕜 E
inst✝¹ : Module 𝕜 β
inst✝ : OrderedSMul 𝕜 β
s : Set E
f : E → β
hf : StrictConvexOn 𝕜 s f
r : β
x : E
hx : x ∈ {x | x ∈ s ∧ f x < r}
y : E
hy : y ∈ {x | x ∈ s ∧ f x < r}
hxy : x ≠ y
a b : 𝕜
ha : 0 < a
hb : 0 < b
hab : a + b = 1
⊢ f y ≤ r

Tactic:
exact hy.2.le

Result:
no goals

Proof state:
𝕜 : Type u_1
E : Type u_2
β : Type u_5
inst✝⁵ : OrderedSemiring 𝕜
inst✝⁴ : AddCommMonoid E
inst✝³ : OrderedAddCommMonoid β
inst✝² : Module 𝕜 E
inst✝¹ : Module 𝕜 β
inst✝ : OrderedSMul 𝕜 β
s : Set E
f : E → β
hf : StrictConvexOn 𝕜 s f
r : β
x : E
hx : x ∈ {x | x ∈ s ∧ f x < r}
y : E
hy : y ∈ {x | x ∈ s ∧ f x < r}
hxy : x ≠ y
a b : 𝕜
ha : 0 < a
hb : 0 < b
hab : a + b = 1
⊢ a • f x + b • f y ≤ a • r + b • r

Tactic:
gcongr

Result:
case h₁.hb
𝕜 : Type u_1
E : Type u_2
β : Type u_5
inst✝⁵ : OrderedSemiring 𝕜
inst✝⁴ : AddCommMonoid E
inst✝³ : OrderedAddCommMonoid β
inst✝² : Module 𝕜 E
inst✝¹ : Module 𝕜 β
inst✝ : OrderedSMul 𝕜 β
s : Set E
f : E → β
hf : StrictConvexOn 𝕜 s f
r : β
x : E
hx : x ∈ {x | x ∈ s ∧ f x < r}
y : E
hy : y ∈ {x | x ∈ s ∧ f x < r}
hxy : x ≠ y
a b : 𝕜
ha : 0 < a
hb : 0 < b
hab : a + b = 1
⊢ f x ≤ r

case h₂.hb
𝕜 : Type u_1
E : Type u_2
β : Type u_5
inst✝⁵ : OrderedSemiring 𝕜
inst✝⁴ : AddCommMonoid E
inst✝³ : OrderedAddCommMonoid β
inst✝² : Module 𝕜 E
inst✝¹ : Module 𝕜 β
inst✝ : OrderedSMul 𝕜 β
s : Set E
f : E → β
hf : StrictConvexOn 𝕜 s f
r : β
x : E
hx : x ∈ {x | x ∈ s ∧ f x < r}
y : E
hy : y ∈ {x | x ∈ s ∧ f x < r}
hxy : x ≠ y
a b : 𝕜
ha : 0 < a
hb : 0 < b
hab : a + b = 1
⊢ f y ≤ r
-- Mathlib/Combinatorics/SimpleGraph/Path.lean
theorem toDeleteEdges_copy {v u u' v' : V} (s : Set (Sym2 V))
    (p : G.Walk u v) (hu : u = u') (hv : v = v') (h) :
    (p.copy hu hv).toDeleteEdges s h =
      (p.toDeleteEdges s (by subst_vars; exact h)).copy hu hv

Proof state:
V : Type u
G : SimpleGraph V
v u u' v' : V
s : Set (Sym2 V)
p : G.Walk u v
hu : u = u'
hv : v = v'
h : ∀ e ∈ (p.copy hu hv).edges, e ∉ s
⊢ toDeleteEdges s (p.copy hu hv) h = (toDeleteEdges s p ⋯).copy hu hv

Tactic:
subst_vars

Result:
V : Type u
G : SimpleGraph V
u' v' : V
s : Set (Sym2 V)
p : G.Walk u' v'
h : ∀ e ∈ (p.copy ⋯ ⋯).edges, e ∉ s
⊢ toDeleteEdges s (p.copy ⋯ ⋯) h = (toDeleteEdges s p ⋯).copy ⋯ ⋯

Proof state:
V : Type u
V' : Type v
V'' : Type w
G : SimpleGraph V
G' : SimpleGraph V'
G'' : SimpleGraph V''
v w u' v' : V
s : Set (Sym2 V)
p : G.Walk u' v'
h : ∀ e ∈ (p.copy ⋯ ⋯).edges, e ∉ s
⊢ ∀ e ∈ p.edges, e ∉ s

Tactic:
exact h

Result:
no goals

Proof state:
V : Type u
G : SimpleGraph V
u' v' : V
s : Set (Sym2 V)
p : G.Walk u' v'
h : ∀ e ∈ (p.copy ⋯ ⋯).edges, e ∉ s
⊢ toDeleteEdges s (p.copy ⋯ ⋯) h = (toDeleteEdges s p ⋯).copy ⋯ ⋯

Tactic:
rfl

Result:
no goals

Proof state:
V : Type u
V' : Type v
V'' : Type w
G : SimpleGraph V
G' : SimpleGraph V'
G'' : SimpleGraph V''
v✝ w v u u' v' : V
s : Set (Sym2 V)
p : G.Walk u v
hu : u = u'
hv : v = v'
h : ∀ e ∈ (p.copy hu hv).edges, e ∉ s
⊢ ∀ e ∈ p.edges, e ∉ s

Tactic:
subst_vars

Result:
V : Type u
V' : Type v
V'' : Type w
G : SimpleGraph V
G' : SimpleGraph V'
G'' : SimpleGraph V''
v w u' v' : V
s : Set (Sym2 V)
p : G.Walk u' v'
h : ∀ e ∈ (p.copy ⋯ ⋯).edges, e ∉ s
⊢ ∀ e ∈ p.edges, e ∉ s
-- Mathlib/MeasureTheory/Function/SimpleFuncDenseLp.lean
theorem memLp_approxOn [BorelSpace E] {f : β → E} {μ : Measure β} (fmeas : Measurable f)
    (hf : MemLp f p μ) {s : Set E} {y₀ : E} (h₀ : y₀ ∈ s) [SeparableSpace s]
    (hi₀ : MemLp (fun _ => y₀) p μ) (n : ℕ) : MemLp (approxOn f fmeas s y₀ h₀ n) p μ

Proof state:
β : Type u_2
E : Type u_4
inst✝⁴ : MeasurableSpace β
inst✝³ : MeasurableSpace E
inst✝² : NormedAddCommGroup E
p : ℝ≥0∞
inst✝¹ : BorelSpace E
f : β → E
μ : Measure β
fmeas : Measurable f
hf : MemLp f p μ
s : Set E
y₀ : E
h₀ : y₀ ∈ s
inst✝ : SeparableSpace ↑s
hi₀ : MemLp (fun x => y₀) p μ
n : ℕ
hf' : MemLp (fun x => ‖f x - y₀‖) p μ
⊢ eLpNorm (fun x => (approxOn f fmeas s y₀ h₀ n) x - y₀) p μ < ⊤

Tactic:
have : ∀ᵐ x ∂μ, ‖approxOn f fmeas s y₀ h₀ n x - y₀‖ ≤ ‖‖f x - y₀‖ + ‖f x - y₀‖‖ := by
  filter_upwards with x
  convert norm_approxOn_y₀_le fmeas h₀ x n using 1
  rw [Real.norm_eq_abs, abs_of_nonneg]
  positivity

Result:
β : Type u_2
E : Type u_4
inst✝⁴ : MeasurableSpace β
inst✝³ : MeasurableSpace E
inst✝² : NormedAddCommGroup E
p : ℝ≥0∞
inst✝¹ : BorelSpace E
f : β → E
μ : Measure β
fmeas : Measurable f
hf : MemLp f p μ
s : Set E
y₀ : E
h₀ : y₀ ∈ s
inst✝ : SeparableSpace ↑s
hi₀ : MemLp (fun x => y₀) p μ
n : ℕ
hf' : MemLp (fun x => ‖f x - y₀‖) p μ
this : ∀ᵐ (x : β) ∂μ, ‖(approxOn f fmeas s y₀ h₀ n) x - y₀‖ ≤ ‖‖f x - y₀‖ + ‖f x - y₀‖‖
⊢ eLpNorm (fun x => (approxOn f fmeas s y₀ h₀ n) x - y₀) p μ < ⊤

Proof state:
β : Type u_2
E : Type u_4
inst✝⁴ : MeasurableSpace β
inst✝³ : MeasurableSpace E
inst✝² : NormedAddCommGroup E
p : ℝ≥0∞
inst✝¹ : BorelSpace E
f : β → E
μ : Measure β
fmeas : Measurable f
hf : MemLp f p μ
s : Set E
y₀ : E
h₀ : y₀ ∈ s
inst✝ : SeparableSpace ↑s
hi₀ : MemLp (fun x => y₀) p μ
n : ℕ
hf' : MemLp (fun x => ‖f x - y₀‖) p μ
⊢ ∀ᵐ (x : β) ∂μ, ‖(approxOn f fmeas s y₀ h₀ n) x - y₀‖ ≤ ‖‖f x - y₀‖ + ‖f x - y₀‖‖

Tactic:
filter_upwards with x

Result:
case h
β : Type u_2
E : Type u_4
inst✝⁴ : MeasurableSpace β
inst✝³ : MeasurableSpace E
inst✝² : NormedAddCommGroup E
p : ℝ≥0∞
inst✝¹ : BorelSpace E
f : β → E
μ : Measure β
fmeas : Measurable f
hf : MemLp f p μ
s : Set E
y₀ : E
h₀ : y₀ ∈ s
inst✝ : SeparableSpace ↑s
hi₀ : MemLp (fun x => y₀) p μ
n : ℕ
hf' : MemLp (fun x => ‖f x - y₀‖) p μ
x : β
⊢ ‖(approxOn f fmeas s y₀ h₀ n) x - y₀‖ ≤ ‖‖f x - y₀‖ + ‖f x - y₀‖‖
-- Mathlib/SetTheory/Ordinal/Arithmetic.lean
theorem card_sInf_range_compl_le_lift {ι : Type u} (f : ι → Ordinal.{max u v}) :
    (sInf (range f)ᶜ).card ≤ Cardinal.lift.{v} #ι

Proof state:
ι : Type u
f : ι → Ordinal.{max u v}
⊢ Cardinal.lift.{(max u v) + 1, max u v} (sInf (range f)ᶜ).card ≤ Cardinal.lift.{max v (u + 1) (v + 1), u} #ι

Tactic:
apply (lift_card_sInf_compl_le _).trans

Result:
ι : Type u
f : ι → Ordinal.{max u v}
⊢ #↑(range f) ≤ Cardinal.lift.{max v (u + 1) (v + 1), u} #ι

Proof state:
ι : Type u
f : ι → Ordinal.{max u v}
⊢ #↑(range f) ≤ Cardinal.lift.{max v (u + 1) (v + 1), u} #ι

Tactic:
rw [← Cardinal.lift_id'.{u, max u v + 1} #(range _)]

Result:
ι : Type u
f : ι → Ordinal.{max u v}
⊢ Cardinal.lift.{u, max u ((max u v) + 1)} #↑(range f) ≤ Cardinal.lift.{max v (u + 1) (v + 1), u} #ι

Proof state:
ι : Type u
f : ι → Ordinal.{max u v}
⊢ (sInf (range f)ᶜ).card ≤ Cardinal.lift.{v, u} #ι

Tactic:
rw [← Cardinal.lift_le.{max u v + 1}, Cardinal.lift_lift]

Result:
ι : Type u
f : ι → Ordinal.{max u v}
⊢ Cardinal.lift.{(max u v) + 1, max u v} (sInf (range f)ᶜ).card ≤ Cardinal.lift.{max v (u + 1) (v + 1), u} #ι

Proof state:
ι : Type u
f : ι → Ordinal.{max u v}
⊢ Cardinal.lift.{u, max u ((max u v) + 1)} #↑(range f) ≤ Cardinal.lift.{max v (u + 1) (v + 1), u} #ι

Tactic:
exact mk_range_le_lift

Result:
no goals
-- Mathlib/Algebra/Polynomial/Basic.lean
theorem smul_X_eq_monomial {n} : a • X ^ n = monomial n (a : R)

Proof state:
R : Type u
a : R
inst✝ : Semiring R
n : ℕ
⊢ a • X ^ n = (monomial n) a

Tactic:
rw [X_pow_eq_monomial, smul_monomial, smul_eq_mul, mul_one]

Result:
no goals
-- Mathlib/Analysis/Normed/Field/Basic.lean
theorem nnnorm_mul_toNNReal (x : ℝ) {y : ℝ} (hy : 0 ≤ y) : ‖x‖₊ * y.toNNReal = ‖x * y‖₊

Proof state:
x y : ℝ
hy : 0 ≤ y
⊢ ‖x‖₊ * y.toNNReal = ‖x * y‖₊

Tactic:
rw [mul_comm, mul_comm x, toNNReal_mul_nnnorm x hy]

Result:
no goals
-- Mathlib/CategoryTheory/Triangulated/Pretriangulated.lean
lemma isZero₃_of_isZero₁₂ (h₁ : IsZero T.obj₁) (h₂ : IsZero T.obj₂) : IsZero T.obj₃ :=
  isZero₂_of_isZero₁₃ _ (rot_of_distTriang _ hT) h₂ (by
    dsimp
    simp only [IsZero.iff_id_eq_zero] at h₁ ⊢
    rw [← Functor.map_id, h₁, Functor.map_zero])

Proof state:
C : Type u
inst✝⁴ : Category.{v, u} C
inst✝³ : HasZeroObject C
inst✝² : HasShift C ℤ
inst✝¹ : Preadditive C
inst✝ : ∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive
hC : Pretriangulated C
T : Triangle C
hT : T ∈ distinguishedTriangles
h₁ : IsZero T.obj₁
h₂ : IsZero T.obj₂
⊢ IsZero ((CategoryTheory.shiftFunctor C 1).obj T.obj₁)

Tactic:
simp only [IsZero.iff_id_eq_zero] at h₁ ⊢

Result:
C : Type u
inst✝⁴ : Category.{v, u} C
inst✝³ : HasZeroObject C
inst✝² : HasShift C ℤ
inst✝¹ : Preadditive C
inst✝ : ∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive
hC : Pretriangulated C
T : Triangle C
hT : T ∈ distinguishedTriangles
h₂ : IsZero T.obj₂
h₁ : 𝟙 T.obj₁ = 0
⊢ 𝟙 ((CategoryTheory.shiftFunctor C 1).obj T.obj₁) = 0

Proof state:
C : Type u
inst✝⁴ : Category.{v, u} C
inst✝³ : HasZeroObject C
inst✝² : HasShift C ℤ
inst✝¹ : Preadditive C
inst✝ : ∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive
hC : Pretriangulated C
T : Triangle C
hT : T ∈ distinguishedTriangles
h₁ : IsZero T.obj₁
h₂ : IsZero T.obj₂
⊢ IsZero T.rotate.obj₃

Tactic:
dsimp

Result:
C : Type u
inst✝⁴ : Category.{v, u} C
inst✝³ : HasZeroObject C
inst✝² : HasShift C ℤ
inst✝¹ : Preadditive C
inst✝ : ∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive
hC : Pretriangulated C
T : Triangle C
hT : T ∈ distinguishedTriangles
h₁ : IsZero T.obj₁
h₂ : IsZero T.obj₂
⊢ IsZero ((CategoryTheory.shiftFunctor C 1).obj T.obj₁)

Proof state:
C : Type u
inst✝⁴ : Category.{v, u} C
inst✝³ : HasZeroObject C
inst✝² : HasShift C ℤ
inst✝¹ : Preadditive C
inst✝ : ∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive
hC : Pretriangulated C
T : Triangle C
hT : T ∈ distinguishedTriangles
h₂ : IsZero T.obj₂
h₁ : 𝟙 T.obj₁ = 0
⊢ 𝟙 ((CategoryTheory.shiftFunctor C 1).obj T.obj₁) = 0

Tactic:
rw [← Functor.map_id, h₁, Functor.map_zero]

Result:
no goals
-- Mathlib/GroupTheory/GroupAction/Defs.lean
@[to_additive]
lemma orbitRel.Quotient.orbit_injective :
    Injective (orbitRel.Quotient.orbit : orbitRel.Quotient G α → Set α)

Proof state:
G : Type u_1
α : Type u_2
inst✝¹ : Group G
inst✝ : MulAction G α
⊢ Injective orbit

Tactic:
intro x y h

Result:
G : Type u_1
α : Type u_2
inst✝¹ : Group G
inst✝ : MulAction G α
x y : Quotient G α
h : x.orbit = y.orbit
⊢ x = y

Proof state:
G : Type u_1
α : Type u_2
inst✝¹ : Group G
inst✝ : MulAction G α
x y : Quotient G α
h : (orbitRel G α) (Quotient.out x) (Quotient.out y)
⊢ x = y

Tactic:
simpa [← Quotient.eq''] using h

Result:
no goals

Proof state:
G : Type u_1
α : Type u_2
inst✝¹ : Group G
inst✝ : MulAction G α
x y : Quotient G α
h : x.orbit = y.orbit
⊢ x = y

Tactic:
simp_rw [orbitRel.Quotient.orbit_eq_orbit_out _ Quotient.out_eq', orbit_eq_iff,
  ← orbitRel_apply] at h

Result:
G : Type u_1
α : Type u_2
inst✝¹ : Group G
inst✝ : MulAction G α
x y : Quotient G α
h : (orbitRel G α) (Quotient.out x) (Quotient.out y)
⊢ x = y