harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/.lake/packages/lean4/src/lean/Init/Omega/Constraint.lean
theorem translate_sat : {c : Constraint} → {v : Int} → sat c v → sat (c.translate t) (v + t)

Proof state:
case mk.some.some
t l u v : Int
w : l ≤ v ∧ v ≤ u
⊢ l + t ≤ v + t ∧ v + t ≤ u + t

Tactic:
rcases w with ⟨w₁, w₂⟩

Result:
case mk.some.some.intro
t l u v : Int
w₁ : l ≤ v
w₂ : v ≤ u
⊢ l + t ≤ v + t ∧ v + t ≤ u + t

Proof state:
case mk.none.some
t u v : Int
w : v ≤ u
⊢ v + t ≤ u + t

Tactic:
exact Int.add_le_add_right w t

Result:
no goals

Proof state:
case mk.some.some.intro.right
t l u v : Int
w₁ : l ≤ v
w₂ : v ≤ u
⊢ v + t ≤ u + t

Tactic:
exact Int.add_le_add_right w₂ t

Result:
no goals

Proof state:
case mk.some.some.intro.left
t l u v : Int
w₁ : l ≤ v
w₂ : v ≤ u
⊢ l + t ≤ v + t

Tactic:
exact Int.add_le_add_right w₁ t

Result:
no goals

Proof state:
case mk.some.some.intro
t l u v : Int
w₁ : l ≤ v
w₂ : v ≤ u
⊢ l + t ≤ v + t ∧ v + t ≤ u + t

Tactic:
constructor

Result:
case mk.some.some.intro.left
t l u v : Int
w₁ : l ≤ v
w₂ : v ≤ u
⊢ l + t ≤ v + t

case mk.some.some.intro.right
t l u v : Int
w₁ : l ≤ v
w₂ : v ≤ u
⊢ v + t ≤ u + t

Proof state:
case mk.some.none
t l v : Int
w : l ≤ v
⊢ l + t ≤ v + t

Tactic:
exact Int.add_le_add_right w t

Result:
no goals

Proof state:
t : Int
⊢ ∀ {c : Constraint} {v : Int}, c.sat v = true → (c.translate t).sat (v + t) = true

Tactic:
rintro ⟨_ | l, _ | u⟩ v w <;> simp_all [sat, translate, map]

Result:
case mk.none.some
t u v : Int
w : v ≤ u
⊢ v + t ≤ u + t

case mk.some.none
t l v : Int
w : l ≤ v
⊢ l + t ≤ v + t

case mk.some.some
t l u v : Int
w : l ≤ v ∧ v ≤ u
⊢ l + t ≤ v + t ∧ v + t ≤ u + t
-- Mathlib/Probability/Kernel/Composition/MapComap.lean
@[simp]
lemma id_comap {f : α → β} (hf : Measurable f) : Kernel.id.comap f hf = deterministic f hf

Proof state:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
f : α → β
hf : Measurable f
⊢ Kernel.id.comap f hf = deterministic f hf

Tactic:
ext

Result:
case h.h
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
f : α → β
hf : Measurable f
a✝¹ : α
s✝ : Set β
a✝ : MeasurableSet s✝
⊢ ((Kernel.id.comap f hf) a✝¹) s✝ = ((deterministic f hf) a✝¹) s✝

Proof state:
case h.h
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
f : α → β
hf : Measurable f
a✝¹ : α
s✝ : Set β
a✝ : MeasurableSet s✝
⊢ ((Kernel.id.comap f hf) a✝¹) s✝ = ((deterministic f hf) a✝¹) s✝

Tactic:
rw [Kernel.comap_apply _ hf, Kernel.deterministic_apply, Kernel.id_apply]

Result:
no goals
-- Mathlib/Order/Filter/AtTopBot/Basic.lean
theorem exists_lt_of_tendsto_atTop [NoMaxOrder β] (h : Tendsto u atTop atTop) (a : α) (b : β) :
    ∃ a' ≥ a, b < u a'

Proof state:
α : Type u_3
β : Type u_4
inst✝³ : Preorder α
inst✝² : IsDirected α fun x1 x2 => x1 ≤ x2
u : α → β
inst✝¹ : Preorder β
inst✝ : NoMaxOrder β
h : Tendsto u atTop atTop
a : α
b : β
⊢ ∃ a' ≥ a, b < u a'

Tactic:
obtain ⟨b', hb'⟩ := exists_gt b

Result:
case intro
α : Type u_3
β : Type u_4
inst✝³ : Preorder α
inst✝² : IsDirected α fun x1 x2 => x1 ≤ x2
u : α → β
inst✝¹ : Preorder β
inst✝ : NoMaxOrder β
h : Tendsto u atTop atTop
a : α
b b' : β
hb' : b < b'
⊢ ∃ a' ≥ a, b < u a'

Proof state:
case intro.intro.intro
α : Type u_3
β : Type u_4
inst✝³ : Preorder α
inst✝² : IsDirected α fun x1 x2 => x1 ≤ x2
u : α → β
inst✝¹ : Preorder β
inst✝ : NoMaxOrder β
h : Tendsto u atTop atTop
a : α
b b' : β
hb' : b < b'
a' : α
ha' : a' ≥ a
ha'' : b' ≤ u a'
⊢ ∃ a' ≥ a, b < u a'

Tactic:
exact ⟨a', ha', lt_of_lt_of_le hb' ha''⟩

Result:
no goals

Proof state:
case intro
α : Type u_3
β : Type u_4
inst✝³ : Preorder α
inst✝² : IsDirected α fun x1 x2 => x1 ≤ x2
u : α → β
inst✝¹ : Preorder β
inst✝ : NoMaxOrder β
h : Tendsto u atTop atTop
a : α
b b' : β
hb' : b < b'
⊢ ∃ a' ≥ a, b < u a'

Tactic:
rcases exists_le_of_tendsto_atTop h a b' with ⟨a', ha', ha''⟩

Result:
case intro.intro.intro
α : Type u_3
β : Type u_4
inst✝³ : Preorder α
inst✝² : IsDirected α fun x1 x2 => x1 ≤ x2
u : α → β
inst✝¹ : Preorder β
inst✝ : NoMaxOrder β
h : Tendsto u atTop atTop
a : α
b b' : β
hb' : b < b'
a' : α
ha' : a' ≥ a
ha'' : b' ≤ u a'
⊢ ∃ a' ≥ a, b < u a'
-- Mathlib/ModelTheory/Equivalence.lean
theorem not {φ ψ : L.BoundedFormula α n} (h : φ ⇔[T] ψ) :
    φ.not ⇔[T] ψ.not

Proof state:
L : Language
T : L.Theory
α : Type w
n : ℕ
φ ψ : L.BoundedFormula α n
h : φ ⇔[T] ψ
⊢ ∀ (M : T.ModelType) (v : α → ↑M) (xs : Fin n → ↑M), ¬φ.Realize v xs ↔ ¬ψ.Realize v xs

Tactic:
exact fun M v xs => not_congr h.realize_bd_iff

Result:
no goals

Proof state:
L : Language
T : L.Theory
α : Type w
n : ℕ
φ ψ : L.BoundedFormula α n
h : φ ⇔[T] ψ
⊢ ∼φ ⇔[T] ∼ψ

Tactic:
simp_rw [Theory.Iff, ModelsBoundedFormula, BoundedFormula.realize_iff,
  BoundedFormula.realize_not]

Result:
L : Language
T : L.Theory
α : Type w
n : ℕ
φ ψ : L.BoundedFormula α n
h : φ ⇔[T] ψ
⊢ ∀ (M : T.ModelType) (v : α → ↑M) (xs : Fin n → ↑M), ¬φ.Realize v xs ↔ ¬ψ.Realize v xs
-- Mathlib/Topology/Algebra/ProperAction/ProperlyDiscontinuous.lean
theorem properlyDiscontinuousSMul_iff_properSMul [T2Space X] [DiscreteTopology G]
    [ContinuousConstSMul G X] [CompactlyGeneratedSpace (X × X)] :
    ProperlyDiscontinuousSMul G X ↔ ProperSMul G X

Proof state:
case h
G : Type u_1
X : Type u_2
inst✝⁷ : Group G
inst✝⁶ : MulAction G X
inst✝⁵ : TopologicalSpace G
inst✝⁴ : TopologicalSpace X
inst✝³ : T2Space X
inst✝² : DiscreteTopology G
inst✝¹ : ContinuousConstSMul G X
inst✝ : CompactlyGeneratedSpace (X × X)
h : ProperSMul G X
K L : Set X
hK : IsCompact K
hL : IsCompact L
this : IsProperMap fun gx => (gx.1⁻¹ • gx.2, gx.2)
g : G
⊢ g ∈ {g | ∃ x, x ∈ (fun x => g • x) '' K ∩ L} ↔ g ∈ fst '' ((fun gx => (gx.1⁻¹ • gx.2, gx.2)) ⁻¹' K ×ˢ L)

Tactic:
constructor

Result:
case h.mp
G : Type u_1
X : Type u_2
inst✝⁷ : Group G
inst✝⁶ : MulAction G X
inst✝⁵ : TopologicalSpace G
inst✝⁴ : TopologicalSpace X
inst✝³ : T2Space X
inst✝² : DiscreteTopology G
inst✝¹ : ContinuousConstSMul G X
inst✝ : CompactlyGeneratedSpace (X × X)
h : ProperSMul G X
K L : Set X
hK : IsCompact K
hL : IsCompact L
this : IsProperMap fun gx => (gx.1⁻¹ • gx.2, gx.2)
g : G
⊢ g ∈ {g | ∃ x, x ∈ (fun x => g • x) '' K ∩ L} → g ∈ fst '' ((fun gx => (gx.1⁻¹ • gx.2, gx.2)) ⁻¹' K ×ˢ L)

case h.mpr
G : Type u_1
X : Type u_2
inst✝⁷ : Group G
inst✝⁶ : MulAction G X
inst✝⁵ : TopologicalSpace G
inst✝⁴ : TopologicalSpace X
inst✝³ : T2Space X
inst✝² : DiscreteTopology G
inst✝¹ : ContinuousConstSMul G X
inst✝ : CompactlyGeneratedSpace (X × X)
h : ProperSMul G X
K L : Set X
hK : IsCompact K
hL : IsCompact L
this : IsProperMap fun gx => (gx.1⁻¹ • gx.2, gx.2)
g : G
⊢ g ∈ fst '' ((fun gx => (gx.1⁻¹ • gx.2, gx.2)) ⁻¹' K ×ˢ L) → g ∈ {g | ∃ x, x ∈ (fun x => g • x) '' K ∩ L}

Proof state:
case mp
G : Type u_1
X : Type u_2
inst✝⁷ : Group G
inst✝⁶ : MulAction G X
inst✝⁵ : TopologicalSpace G
inst✝⁴ : TopologicalSpace X
inst✝³ : T2Space X
inst✝² : DiscreteTopology G
inst✝¹ : ContinuousConstSMul G X
inst✝ : CompactlyGeneratedSpace (X × X)
h : ProperlyDiscontinuousSMul G X
K : Set (X × X)
hK : IsCompact K
K' : Set X := fst '' K ∪ snd '' K
⊢ IsCompact ((fun gx => (gx.1 • gx.2, gx.2)) ⁻¹' K)

Tactic:
have hK' : IsCompact K' := (hK.image continuous_fst).union (hK.image continuous_snd)

Result:
case mp
G : Type u_1
X : Type u_2
inst✝⁷ : Group G
inst✝⁶ : MulAction G X
inst✝⁵ : TopologicalSpace G
inst✝⁴ : TopologicalSpace X
inst✝³ : T2Space X
inst✝² : DiscreteTopology G
inst✝¹ : ContinuousConstSMul G X
inst✝ : CompactlyGeneratedSpace (X × X)
h : ProperlyDiscontinuousSMul G X
K : Set (X × X)
hK : IsCompact K
K' : Set X := fst '' K ∪ snd '' K
hK' : IsCompact K'
⊢ IsCompact ((fun gx => (gx.1 • gx.2, gx.2)) ⁻¹' K)
-- Mathlib/Combinatorics/SimpleGraph/Walk.lean
lemma snd_cons {u v w} (q : G.Walk v w) (hadj : G.Adj u v) :
    (q.cons hadj).snd = v

Proof state:
V : Type u
G : SimpleGraph V
u v w : V
q : G.Walk v w
hadj : G.Adj u v
⊢ (cons hadj q).snd = v

Tactic:
simp

Result:
no goals
-- Mathlib/Analysis/Convolution.lean
theorem convolution_eq_right' {x₀ : G} {R : ℝ} (hf : support f ⊆ ball (0 : G) R)
    (hg : ∀ x ∈ ball x₀ R, g x = g x₀) : (f ⋆[L, μ] g) x₀ = ∫ t, L (f t) (g x₀) ∂μ

Proof state:
case pos
𝕜 : Type u𝕜
G : Type uG
E : Type uE
E' : Type uE'
F : Type uF
inst✝⁹ : NormedAddCommGroup E
inst✝⁸ : NormedAddCommGroup E'
inst✝⁷ : NormedAddCommGroup F
f : G → E
g : G → E'
inst✝⁶ : NontriviallyNormedField 𝕜
inst✝⁵ : NormedSpace 𝕜 E
inst✝⁴ : NormedSpace 𝕜 E'
inst✝³ : NormedSpace 𝕜 F
L : E →L[𝕜] E' →L[𝕜] F
inst✝² : MeasurableSpace G
μ : Measure G
inst✝¹ : NormedSpace ℝ F
inst✝ : SeminormedAddCommGroup G
x₀ : G
R : ℝ
hf : support f ⊆ ball 0 R
t : G
ht : t ∈ support f
h2t : ‖t‖ < R
hg : ‖t‖ < R → g (x₀ - t) = g x₀
⊢ (L (f t)) (g (x₀ - t)) = (L (f t)) (g x₀)

Tactic:
rw [hg h2t]

Result:
no goals

Proof state:
case pos
𝕜 : Type u𝕜
G : Type uG
E : Type uE
E' : Type uE'
F : Type uF
inst✝⁹ : NormedAddCommGroup E
inst✝⁸ : NormedAddCommGroup E'
inst✝⁷ : NormedAddCommGroup F
f : G → E
g : G → E'
inst✝⁶ : NontriviallyNormedField 𝕜
inst✝⁵ : NormedSpace 𝕜 E
inst✝⁴ : NormedSpace 𝕜 E'
inst✝³ : NormedSpace 𝕜 F
L : E →L[𝕜] E' →L[𝕜] F
inst✝² : MeasurableSpace G
μ : Measure G
inst✝¹ : NormedSpace ℝ F
inst✝ : SeminormedAddCommGroup G
x₀ : G
R : ℝ
hf : support f ⊆ ball 0 R
hg : ∀ x ∈ ball x₀ R, g x = g x₀
t : G
ht : t ∈ support f
h2t : t ∈ ball 0 R
⊢ (L (f t)) (g (x₀ - t)) = (L (f t)) (g x₀)

Tactic:
rw [mem_ball_zero_iff] at h2t

Result:
case pos
𝕜 : Type u𝕜
G : Type uG
E : Type uE
E' : Type uE'
F : Type uF
inst✝⁹ : NormedAddCommGroup E
inst✝⁸ : NormedAddCommGroup E'
inst✝⁷ : NormedAddCommGroup F
f : G → E
g : G → E'
inst✝⁶ : NontriviallyNormedField 𝕜
inst✝⁵ : NormedSpace 𝕜 E
inst✝⁴ : NormedSpace 𝕜 E'
inst✝³ : NormedSpace 𝕜 F
L : E →L[𝕜] E' →L[𝕜] F
inst✝² : MeasurableSpace G
μ : Measure G
inst✝¹ : NormedSpace ℝ F
inst✝ : SeminormedAddCommGroup G
x₀ : G
R : ℝ
hf : support f ⊆ ball 0 R
hg : ∀ x ∈ ball x₀ R, g x = g x₀
t : G
ht : t ∈ support f
h2t : ‖t‖ < R
⊢ (L (f t)) (g (x₀ - t)) = (L (f t)) (g x₀)
-- Mathlib/Order/Filter/CountablyGenerated.lean
theorem isCountablyGenerated_iff_exists_antitone_basis {f : Filter α} :
    IsCountablyGenerated f ↔ ∃ x : ℕ → Set α, f.HasAntitoneBasis x

Proof state:
case mp
α : Type u_1
f : Filter α
h : f.IsCountablyGenerated
⊢ ∃ x, f.HasAntitoneBasis x

Tactic:
exact f.exists_antitone_basis

Result:
no goals

Proof state:
case mp
α : Type u_1
f : Filter α
⊢ f.IsCountablyGenerated → ∃ x, f.HasAntitoneBasis x

Tactic:
intro h

Result:
case mp
α : Type u_1
f : Filter α
h : f.IsCountablyGenerated
⊢ ∃ x, f.HasAntitoneBasis x

Proof state:
case mpr.intro
α : Type u_1
f : Filter α
x : ℕ → Set α
h : f.HasAntitoneBasis x
⊢ f.IsCountablyGenerated

Tactic:
rw [h.1.eq_iInf]

Result:
case mpr.intro
α : Type u_1
f : Filter α
x : ℕ → Set α
h : f.HasAntitoneBasis x
⊢ (⨅ i, 𝓟 (x i)).IsCountablyGenerated

Proof state:
α : Type u_1
f : Filter α
⊢ f.IsCountablyGenerated ↔ ∃ x, f.HasAntitoneBasis x

Tactic:
constructor

Result:
case mp
α : Type u_1
f : Filter α
⊢ f.IsCountablyGenerated → ∃ x, f.HasAntitoneBasis x

case mpr
α : Type u_1
f : Filter α
⊢ (∃ x, f.HasAntitoneBasis x) → f.IsCountablyGenerated

Proof state:
case mpr
α : Type u_1
f : Filter α
⊢ (∃ x, f.HasAntitoneBasis x) → f.IsCountablyGenerated

Tactic:
rintro ⟨x, h⟩

Result:
case mpr.intro
α : Type u_1
f : Filter α
x : ℕ → Set α
h : f.HasAntitoneBasis x
⊢ f.IsCountablyGenerated

Proof state:
case mpr.intro
α : Type u_1
f : Filter α
x : ℕ → Set α
h : f.HasAntitoneBasis x
⊢ (⨅ i, 𝓟 (x i)).IsCountablyGenerated

Tactic:
exact isCountablyGenerated_seq x

Result:
no goals
-- Mathlib/Combinatorics/Hindman.lean
theorem exists_idempotent_ultrafilter_le_FP {M} [Semigroup M] (a : Stream' M) :
    ∃ U : Ultrafilter M, U * U = U ∧ ∀ᶠ m in U, m ∈ FP a

Proof state:
case refine_2.htcl
M : Type u_1
inst✝ : Semigroup M
a : Stream' M
S : Set (Ultrafilter M) := ⋂ n, {U | ∀ᶠ (m : M) in ↑U, m ∈ FP (Stream'.drop n a)}
⊢ ∀ (i : ℕ), IsClosed {U | ∀ᶠ (m : M) in ↑U, m ∈ FP (Stream'.drop i a)}

Tactic:
intro n

Result:
case refine_2.htcl
M : Type u_1
inst✝ : Semigroup M
a : Stream' M
S : Set (Ultrafilter M) := ⋂ n, {U | ∀ᶠ (m : M) in ↑U, m ∈ FP (Stream'.drop n a)}
n : ℕ
⊢ IsClosed {U | ∀ᶠ (m : M) in ↑U, m ∈ FP (Stream'.drop n a)}

Proof state:
case h.a
M : Type u_1
inst✝ : Semigroup M
a : Stream' M
S : Set (Ultrafilter M) := ⋂ n, {U | ∀ᶠ (m : M) in ↑U, m ∈ FP (Stream'.drop n a)}
U : Ultrafilter M
hU : ∀ (i : ℕ), U ∈ {U | ∀ᶠ (m : M) in ↑U, m ∈ FP (Stream'.drop i a)}
V : Ultrafilter M
hV : ∀ (i : ℕ), V ∈ {U | ∀ᶠ (m : M) in ↑U, m ∈ FP (Stream'.drop i a)}
n : ℕ
m : M
hm : m ∈ FP (Stream'.drop n a)
n' : ℕ
hn : ∀ m' ∈ FP (Stream'.drop n' (Stream'.drop n a)), m * m' ∈ FP (Stream'.drop n a)
m' : M
hm' : m' ∈ FP (Stream'.drop (n' + n) a)
⊢ m' ∈ FP (Stream'.drop n' (Stream'.drop n a))

Tactic:
simpa only [Stream'.drop_drop, add_comm] using hm'

Result:
no goals
-- Mathlib/MeasureTheory/MeasurableSpace/CountablyGenerated.lean
theorem CountablyGenerated.comap [m : MeasurableSpace β] [h : CountablyGenerated β] (f : α → β) :
    @CountablyGenerated α (.comap f m)

Proof state:
case mk.intro.intro
α : Type u_1
β : Type u_2
f : α → β
b : Set (Set β)
hbc : b.Countable
this : MeasurableSpace α := generateFrom (preimage f '' b)
⊢ CountablyGenerated α

Tactic:
exact ⟨_, hbc.image _, rfl⟩

Result:
no goals

Proof state:
α : Type u_1
β : Type u_2
m : MeasurableSpace β
h : CountablyGenerated β
f : α → β
⊢ CountablyGenerated α

Tactic:
rcases h with ⟨⟨b, hbc, rfl⟩⟩

Result:
case mk.intro.intro
α : Type u_1
β : Type u_2
f : α → β
b : Set (Set β)
hbc : b.Countable
⊢ CountablyGenerated α

Proof state:
case mk.intro.intro
α : Type u_1
β : Type u_2
f : α → β
b : Set (Set β)
hbc : b.Countable
⊢ CountablyGenerated α

Tactic:
letI := generateFrom (preimage f '' b)

Result:
case mk.intro.intro
α : Type u_1
β : Type u_2
f : α → β
b : Set (Set β)
hbc : b.Countable
this : MeasurableSpace α := generateFrom (preimage f '' b)
⊢ CountablyGenerated α
-- Mathlib/Algebra/MvPolynomial/Supported.lean
theorem supported_univ : supported R (Set.univ : Set σ) = ⊤

Proof state:
σ : Type u_1
R : Type u
inst✝ : CommSemiring R
⊢ supported R Set.univ = ⊤

Tactic:
simp [Algebra.eq_top_iff, mem_supported]

Result:
no goals
-- Mathlib/LinearAlgebra/Determinant.lean
theorem Basis.det_isEmpty [IsEmpty ι] : e.det = AlternatingMap.constOfIsEmpty R M ι 1

Proof state:
R : Type u_1
inst✝⁵ : CommRing R
M : Type u_2
inst✝⁴ : AddCommGroup M
inst✝³ : Module R M
ι : Type u_4
inst✝² : DecidableEq ι
inst✝¹ : Fintype ι
e : Basis ι R M
inst✝ : IsEmpty ι
⊢ e.det = AlternatingMap.constOfIsEmpty R M ι 1

Tactic:
ext v

Result:
case H
R : Type u_1
inst✝⁵ : CommRing R
M : Type u_2
inst✝⁴ : AddCommGroup M
inst✝³ : Module R M
ι : Type u_4
inst✝² : DecidableEq ι
inst✝¹ : Fintype ι
e : Basis ι R M
inst✝ : IsEmpty ι
v : ι → M
⊢ e.det v = (AlternatingMap.constOfIsEmpty R M ι 1) v

Proof state:
case H
R : Type u_1
inst✝⁵ : CommRing R
M : Type u_2
inst✝⁴ : AddCommGroup M
inst✝³ : Module R M
ι : Type u_4
inst✝² : DecidableEq ι
inst✝¹ : Fintype ι
e : Basis ι R M
inst✝ : IsEmpty ι
v : ι → M
⊢ e.det v = (AlternatingMap.constOfIsEmpty R M ι 1) v

Tactic:
exact Matrix.det_isEmpty

Result:
no goals
-- Mathlib/Analysis/SpecialFunctions/Pow/Real.lean
theorem le_rpow_add {x : ℝ} (hx : 0 ≤ x) (y z : ℝ) : x ^ y * x ^ z ≤ x ^ (y + z)

Proof state:
case pos
x : ℝ
hx : 0 ≤ x
y z : ℝ
H : 0 = x
h : y + z = 0
⊢ 0 ^ y * 0 ^ z ≤ 1

Tactic:
calc
  (0 : ℝ) ^ y * 0 ^ z ≤ 1 * 1 :=
    mul_le_mul (zero_rpow_le_one y) (zero_rpow_le_one z) (zero_rpow_nonneg z) zero_le_one
  _ = 1 := by simp

Result:
no goals

Proof state:
case inl
x : ℝ
hx : 0 ≤ x
y z : ℝ
H : 0 = x
⊢ x ^ y * x ^ z ≤ x ^ (y + z)

Tactic:
by_cases h : y + z = 0

Result:
case pos
x : ℝ
hx : 0 ≤ x
y z : ℝ
H : 0 = x
h : y + z = 0
⊢ x ^ y * x ^ z ≤ x ^ (y + z)

case neg
x : ℝ
hx : 0 ≤ x
y z : ℝ
H : 0 = x
h : ¬y + z = 0
⊢ x ^ y * x ^ z ≤ x ^ (y + z)

Proof state:
case pos
x : ℝ
hx : 0 ≤ x
y z : ℝ
H : 0 = x
h : y + z = 0
⊢ x ^ y * x ^ z ≤ x ^ (y + z)

Tactic:
simp only [H.symm, h, rpow_zero]

Result:
case pos
x : ℝ
hx : 0 ≤ x
y z : ℝ
H : 0 = x
h : y + z = 0
⊢ 0 ^ y * 0 ^ z ≤ 1

Proof state:
case neg
x : ℝ
hx : 0 ≤ x
y z : ℝ
H : 0 = x
h : ¬y + z = 0
⊢ x ^ y * x ^ z ≤ x ^ (y + z)

Tactic:
simp [rpow_add', ← H, h]

Result:
no goals

Proof state:
case inr
x : ℝ
hx : 0 ≤ x
y z : ℝ
pos : 0 < x
⊢ x ^ y * x ^ z ≤ x ^ (y + z)

Tactic:
simp [rpow_add pos]

Result:
no goals

Proof state:
x : ℝ
hx : 0 ≤ x
y z : ℝ
⊢ x ^ y * x ^ z ≤ x ^ (y + z)

Tactic:
rcases le_iff_eq_or_lt.1 hx with (H | pos)

Result:
case inl
x : ℝ
hx : 0 ≤ x
y z : ℝ
H : 0 = x
⊢ x ^ y * x ^ z ≤ x ^ (y + z)

case inr
x : ℝ
hx : 0 ≤ x
y z : ℝ
pos : 0 < x
⊢ x ^ y * x ^ z ≤ x ^ (y + z)

Proof state:
x : ℝ
hx : 0 ≤ x
y z : ℝ
H : 0 = x
h : y + z = 0
⊢ 1 * 1 = 1

Tactic:
simp

Result:
no goals
-- Mathlib/NumberTheory/NumberField/Embeddings.lean
lemma IsUnramifiedAtInfinitePlaces.card_infinitePlace [NumberField k] [NumberField K]
    [IsGalois k K] [IsUnramifiedAtInfinitePlaces k K] :
    Fintype.card (InfinitePlace K) = Fintype.card (InfinitePlace k) * finrank k K

Proof state:
k : Type u_1
inst✝⁶ : Field k
K : Type u_2
inst✝⁵ : Field K
inst✝⁴ : Algebra k K
inst✝³ : NumberField k
inst✝² : NumberField K
inst✝¹ : IsGalois k K
inst✝ : IsUnramifiedAtInfinitePlaces k K
⊢ Fintype.card (InfinitePlace K) = Fintype.card (InfinitePlace k) * finrank k K

Tactic:
rw [InfinitePlace.card_eq_card_isUnramifiedIn (k := k) (K := K), Finset.filter_true_of_mem,
  Finset.card_univ, Finset.card_eq_zero.mpr, zero_mul, add_zero]

Result:
k : Type u_1
inst✝⁶ : Field k
K : Type u_2
inst✝⁵ : Field K
inst✝⁴ : Algebra k K
inst✝³ : NumberField k
inst✝² : NumberField K
inst✝¹ : IsGalois k K
inst✝ : IsUnramifiedAtInfinitePlaces k K
⊢ Finset.univᶜ = ∅

k : Type u_1
inst✝⁶ : Field k
K : Type u_2
inst✝⁵ : Field K
inst✝⁴ : Algebra k K
inst✝³ : NumberField k
inst✝² : NumberField K
inst✝¹ : IsGalois k K
inst✝ : IsUnramifiedAtInfinitePlaces k K
⊢ ∀ x ∈ Finset.univ, InfinitePlace.IsUnramifiedIn K x

Proof state:
k : Type u_1
inst✝⁶ : Field k
K : Type u_2
inst✝⁵ : Field K
inst✝⁴ : Algebra k K
inst✝³ : NumberField k
inst✝² : NumberField K
inst✝¹ : IsGalois k K
inst✝ : IsUnramifiedAtInfinitePlaces k K
⊢ ∀ x ∈ Finset.univ, InfinitePlace.IsUnramifiedIn K x

Tactic:
simp only [Finset.mem_univ, forall_true_left, Finset.filter_eq_empty_iff]

Result:
k : Type u_1
inst✝⁶ : Field k
K : Type u_2
inst✝⁵ : Field K
inst✝⁴ : Algebra k K
inst✝³ : NumberField k
inst✝² : NumberField K
inst✝¹ : IsGalois k K
inst✝ : IsUnramifiedAtInfinitePlaces k K
⊢ ∀ (x : InfinitePlace k), InfinitePlace.IsUnramifiedIn K x

Proof state:
k : Type u_1
inst✝⁶ : Field k
K : Type u_2
inst✝⁵ : Field K
inst✝⁴ : Algebra k K
inst✝³ : NumberField k
inst✝² : NumberField K
inst✝¹ : IsGalois k K
inst✝ : IsUnramifiedAtInfinitePlaces k K
⊢ ∀ (x : InfinitePlace k), InfinitePlace.IsUnramifiedIn K x

Tactic:
exact InfinitePlace.isUnramifiedIn K

Result:
no goals

Proof state:
k : Type u_1
inst✝⁶ : Field k
K : Type u_2
inst✝⁵ : Field K
inst✝⁴ : Algebra k K
inst✝³ : NumberField k
inst✝² : NumberField K
inst✝¹ : IsGalois k K
inst✝ : IsUnramifiedAtInfinitePlaces k K
⊢ Finset.univᶜ = ∅

Tactic:
exact Finset.compl_univ

Result:
no goals
-- Mathlib/NumberTheory/Padics/RingHoms.lean
theorem appr_spec (n : ℕ) : ∀ x : ℤ_[p], x - appr x n ∈ Ideal.span {(p : ℤ_[p]) ^ n}

Proof state:
case neg.intro.h.inr
p : ℕ
hp_prime : Fact (Nat.Prime p)
n : ℕ
ih : ∀ (x : ℤ_[p]), ↑p ^ n ∣ x - ↑(x.appr n)
x : ℤ_[p]
h : ¬x - ↑(x.appr n) = 0
c : ℤ_[p]
hc : x - ↑(x.appr n) = ↑p ^ n * c
hc' : c ≠ 0
hc0 : c.valuation ≠ 0
⊢ ↑p ∣ c

Tactic:
rw [unitCoeff_spec hc']

Result:
case neg.intro.h.inr
p : ℕ
hp_prime : Fact (Nat.Prime p)
n : ℕ
ih : ∀ (x : ℤ_[p]), ↑p ^ n ∣ x - ↑(x.appr n)
x : ℤ_[p]
h : ¬x - ↑(x.appr n) = 0
c : ℤ_[p]
hc : x - ↑(x.appr n) = ↑p ^ n * c
hc' : c ≠ 0
hc0 : c.valuation ≠ 0
⊢ ↑p ∣ ↑(unitCoeff hc') * ↑p ^ c.valuation

Proof state:
case pos
p : ℕ
hp_prime : Fact (Nat.Prime p)
n : ℕ
ih : ∀ (x : ℤ_[p]), ↑p ^ n ∣ x - ↑(x.appr n)
x : ℤ_[p]
h : x - ↑(x.appr n) = 0
⊢ ↑p ^ (n + 1) ∣ x - ↑(x.appr n)

Tactic:
rw [h]

Result:
case pos
p : ℕ
hp_prime : Fact (Nat.Prime p)
n : ℕ
ih : ∀ (x : ℤ_[p]), ↑p ^ n ∣ x - ↑(x.appr n)
x : ℤ_[p]
h : x - ↑(x.appr n) = 0
⊢ ↑p ^ (n + 1) ∣ 0

Proof state:
case neg.intro
p : ℕ
hp_prime : Fact (Nat.Prime p)
n : ℕ
ih : ∀ (x : ℤ_[p]), ↑p ^ n ∣ x - ↑(x.appr n)
x : ℤ_[p]
h : ¬x - ↑(x.appr n) = 0
c : ℤ_[p]
hc : x - ↑(x.appr n) = ↑p ^ n * c
⊢ ↑p ^ (n + 1) ∣
    x - ↑(x.appr n) - ↑p ^ n * ↑(toZMod (↑(unitCoeff h) * ↑p ^ (↑(x - ↑(x.appr n)).valuation - ↑n).natAbs)).val

Tactic:
simp only [map_natCast, ZMod.natCast_self, RingHom.map_pow, RingHom.map_mul, ZMod.natCast_val]

Result:
case neg.intro
p : ℕ
hp_prime : Fact (Nat.Prime p)
n : ℕ
ih : ∀ (x : ℤ_[p]), ↑p ^ n ∣ x - ↑(x.appr n)
x : ℤ_[p]
h : ¬x - ↑(x.appr n) = 0
c : ℤ_[p]
hc : x - ↑(x.appr n) = ↑p ^ n * c
⊢ ↑p ^ (n + 1) ∣
    x - ↑(x.appr n) - ↑p ^ n * (toZMod ↑(unitCoeff h) * 0 ^ (↑(x - ↑(x.appr n)).valuation - ↑n).natAbs).cast

Proof state:
p : ℕ
hp_prime : Fact (Nat.Prime p)
n : ℕ
ih : ∀ (x : ℤ_[p]), ↑p ^ n ∣ x - ↑(x.appr n)
x : ℤ_[p]
h : ¬x - ↑(x.appr n) = 0
c : ℤ_[p]
hc : x - ↑(x.appr n) = ↑p ^ n * c
hc' : c ≠ 0
⊢ (x - ↑(x.appr n)).valuation = (↑p ^ n * c).valuation

Tactic:
rw [hc]

Result:
no goals

Proof state:
case neg.intro
p : ℕ
hp_prime : Fact (Nat.Prime p)
n : ℕ
ih : ∀ (x : ℤ_[p]), ↑p ^ n ∣ x - ↑(x.appr n)
x : ℤ_[p]
h : ¬x - ↑(x.appr n) = 0
c : ℤ_[p]
hc : x - ↑(x.appr n) = ↑p ^ n * c
hc' : c ≠ 0
⊢ ↑p ^ n * ↑p ∣ ↑p ^ n * (c - (toZMod ↑(unitCoeff h) * 0 ^ (↑c.valuation).natAbs).cast)

Tactic:
apply mul_dvd_mul_left

Result:
case neg.intro.h
p : ℕ
hp_prime : Fact (Nat.Prime p)
n : ℕ
ih : ∀ (x : ℤ_[p]), ↑p ^ n ∣ x - ↑(x.appr n)
x : ℤ_[p]
h : ¬x - ↑(x.appr n) = 0
c : ℤ_[p]
hc : x - ↑(x.appr n) = ↑p ^ n * c
hc' : c ≠ 0
⊢ ↑p ∣ c - (toZMod ↑(unitCoeff h) * 0 ^ (↑c.valuation).natAbs).cast