harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/Order/Monotone/Basic.lean
theorem Antitone.eq_of_le_of_le {a₁ a₂ : α} (h_anti : Antitone f) (h_fa : f a₁ = f a₂) {i : α}
    (h₁ : a₁ ≤ i) (h₂ : i ≤ a₂) : f i = f a₁

Proof state:
case a
α : Type u
β : Type v
inst✝¹ : LinearOrder α
inst✝ : PartialOrder β
f : α → β
a₁ a₂ : α
h_anti : Antitone f
h_fa : f a₁ = f a₂
i : α
h₁ : a₁ ≤ i
h₂ : i ≤ a₂
⊢ f a₁ ≤ f i

Tactic:
rw [h_fa]

Result:
case a
α : Type u
β : Type v
inst✝¹ : LinearOrder α
inst✝ : PartialOrder β
f : α → β
a₁ a₂ : α
h_anti : Antitone f
h_fa : f a₁ = f a₂
i : α
h₁ : a₁ ≤ i
h₂ : i ≤ a₂
⊢ f a₂ ≤ f i

Proof state:
case a
α : Type u
β : Type v
inst✝¹ : LinearOrder α
inst✝ : PartialOrder β
f : α → β
a₁ a₂ : α
h_anti : Antitone f
h_fa : f a₁ = f a₂
i : α
h₁ : a₁ ≤ i
h₂ : i ≤ a₂
⊢ f a₂ ≤ f i

Tactic:
exact h_anti h₂

Result:
no goals

Proof state:
α : Type u
β : Type v
inst✝¹ : LinearOrder α
inst✝ : PartialOrder β
f : α → β
a₁ a₂ : α
h_anti : Antitone f
h_fa : f a₁ = f a₂
i : α
h₁ : a₁ ≤ i
h₂ : i ≤ a₂
⊢ f i = f a₁

Tactic:
apply le_antisymm

Result:
case a
α : Type u
β : Type v
inst✝¹ : LinearOrder α
inst✝ : PartialOrder β
f : α → β
a₁ a₂ : α
h_anti : Antitone f
h_fa : f a₁ = f a₂
i : α
h₁ : a₁ ≤ i
h₂ : i ≤ a₂
⊢ f i ≤ f a₁

case a
α : Type u
β : Type v
inst✝¹ : LinearOrder α
inst✝ : PartialOrder β
f : α → β
a₁ a₂ : α
h_anti : Antitone f
h_fa : f a₁ = f a₂
i : α
h₁ : a₁ ≤ i
h₂ : i ≤ a₂
⊢ f a₁ ≤ f i

Proof state:
case a
α : Type u
β : Type v
inst✝¹ : LinearOrder α
inst✝ : PartialOrder β
f : α → β
a₁ a₂ : α
h_anti : Antitone f
h_fa : f a₁ = f a₂
i : α
h₁ : a₁ ≤ i
h₂ : i ≤ a₂
⊢ f i ≤ f a₁

Tactic:
exact h_anti h₁

Result:
no goals
-- Mathlib/Algebra/ContinuedFractions/Computation/CorrectnessTerminating.lean
theorem of_correctness_atTop_of_terminates (terminates : (of v).Terminates) :
    ∀ᶠ n in atTop, v = (of v).convs n

Proof state:
case h
K : Type u_1
inst✝¹ : LinearOrderedField K
v : K
inst✝ : FloorRing K
n : ℕ
terminatedAt_n : (of v).TerminatedAt n
⊢ ∀ b ≥ n, v = (of v).convs b

Tactic:
intro m m_geq_n

Result:
case h
K : Type u_1
inst✝¹ : LinearOrderedField K
v : K
inst✝ : FloorRing K
n : ℕ
terminatedAt_n : (of v).TerminatedAt n
m : ℕ
m_geq_n : m ≥ n
⊢ v = (of v).convs m

Proof state:
case h
K : Type u_1
inst✝¹ : LinearOrderedField K
v : K
inst✝ : FloorRing K
n : ℕ
terminatedAt_n : (of v).TerminatedAt n
m : ℕ
m_geq_n : m ≥ n
⊢ v = (of v).convs m

Tactic:
rw [convs_stable_of_terminated m_geq_n terminatedAt_n]

Result:
case h
K : Type u_1
inst✝¹ : LinearOrderedField K
v : K
inst✝ : FloorRing K
n : ℕ
terminatedAt_n : (of v).TerminatedAt n
m : ℕ
m_geq_n : m ≥ n
⊢ v = (of v).convs n

Proof state:
K : Type u_1
inst✝¹ : LinearOrderedField K
v : K
inst✝ : FloorRing K
terminates : (of v).Terminates
⊢ ∃ a, ∀ b ≥ a, v = (of v).convs b

Tactic:
obtain ⟨n, terminatedAt_n⟩ : ∃ n, (of v).TerminatedAt n := terminates

Result:
case intro
K : Type u_1
inst✝¹ : LinearOrderedField K
v : K
inst✝ : FloorRing K
n : ℕ
terminatedAt_n : (of v).TerminatedAt n
⊢ ∃ a, ∀ b ≥ a, v = (of v).convs b

Proof state:
K : Type u_1
inst✝¹ : LinearOrderedField K
v : K
inst✝ : FloorRing K
terminates : (of v).Terminates
⊢ ∀ᶠ (n : ℕ) in atTop, v = (of v).convs n

Tactic:
rw [eventually_atTop]

Result:
K : Type u_1
inst✝¹ : LinearOrderedField K
v : K
inst✝ : FloorRing K
terminates : (of v).Terminates
⊢ ∃ a, ∀ b ≥ a, v = (of v).convs b

Proof state:
case h
K : Type u_1
inst✝¹ : LinearOrderedField K
v : K
inst✝ : FloorRing K
n : ℕ
terminatedAt_n : (of v).TerminatedAt n
m : ℕ
m_geq_n : m ≥ n
⊢ v = (of v).convs n

Tactic:
exact of_correctness_of_terminatedAt terminatedAt_n

Result:
no goals

Proof state:
case intro
K : Type u_1
inst✝¹ : LinearOrderedField K
v : K
inst✝ : FloorRing K
n : ℕ
terminatedAt_n : (of v).TerminatedAt n
⊢ ∃ a, ∀ b ≥ a, v = (of v).convs b

Tactic:
use n

Result:
case h
K : Type u_1
inst✝¹ : LinearOrderedField K
v : K
inst✝ : FloorRing K
n : ℕ
terminatedAt_n : (of v).TerminatedAt n
⊢ ∀ b ≥ n, v = (of v).convs b
-- Mathlib/RingTheory/FractionalIdeal/Operations.lean
theorem isNoetherian_spanSingleton_inv_to_map_mul (x : R₁) {I : FractionalIdeal R₁⁰ K}
    (hI : IsNoetherian R₁ I) :
    IsNoetherian R₁ (spanSingleton R₁⁰ (algebraMap R₁ K x)⁻¹ * I : FractionalIdeal R₁⁰ K)

Proof state:
R₁ : Type u_3
inst✝⁴ : CommRing R₁
K : Type u_4
inst✝³ : Field K
inst✝² : Algebra R₁ K
inst✝¹ : IsFractionRing R₁ K
inst✝ : IsDomain R₁
x : R₁
I : FractionalIdeal R₁⁰ K
hI : IsNoetherian R₁ ↥↑I
⊢ IsNoetherian R₁ ↥↑(spanSingleton R₁⁰ ((algebraMap R₁ K) x)⁻¹ * I)

Tactic:
by_cases hx : x = 0

Result:
case pos
R₁ : Type u_3
inst✝⁴ : CommRing R₁
K : Type u_4
inst✝³ : Field K
inst✝² : Algebra R₁ K
inst✝¹ : IsFractionRing R₁ K
inst✝ : IsDomain R₁
x : R₁
I : FractionalIdeal R₁⁰ K
hI : IsNoetherian R₁ ↥↑I
hx : x = 0
⊢ IsNoetherian R₁ ↥↑(spanSingleton R₁⁰ ((algebraMap R₁ K) x)⁻¹ * I)

case neg
R₁ : Type u_3
inst✝⁴ : CommRing R₁
K : Type u_4
inst✝³ : Field K
inst✝² : Algebra R₁ K
inst✝¹ : IsFractionRing R₁ K
inst✝ : IsDomain R₁
x : R₁
I : FractionalIdeal R₁⁰ K
hI : IsNoetherian R₁ ↥↑I
hx : ¬x = 0
⊢ IsNoetherian R₁ ↥↑(spanSingleton R₁⁰ ((algebraMap R₁ K) x)⁻¹ * I)
-- Mathlib/NumberTheory/NumberField/Embeddings.lean
theorem embedding_mk_eq_of_isReal {φ : K →+* ℂ} (h : ComplexEmbedding.IsReal φ) :
    embedding (mk φ) = φ

Proof state:
K : Type u_2
inst✝ : Field K
φ : K →+* ℂ
h : ComplexEmbedding.IsReal φ
⊢ (mk φ).embedding = φ

Tactic:
have := embedding_mk_eq φ

Result:
K : Type u_2
inst✝ : Field K
φ : K →+* ℂ
h : ComplexEmbedding.IsReal φ
this : (mk φ).embedding = φ ∨ (mk φ).embedding = ComplexEmbedding.conjugate φ
⊢ (mk φ).embedding = φ

Proof state:
K : Type u_2
inst✝ : Field K
φ : K →+* ℂ
h : ComplexEmbedding.IsReal φ
this : (mk φ).embedding = φ ∨ (mk φ).embedding = ComplexEmbedding.conjugate φ
⊢ (mk φ).embedding = φ

Tactic:
rwa [ComplexEmbedding.isReal_iff.mp h, or_self] at this

Result:
no goals
-- Mathlib/RingTheory/Ideal/Cotangent.lean
lemma Cotangent.smul_eq_zero_of_mem {I : Ideal R}
    {x} (hx : x ∈ I) (m : I.Cotangent) : x • m = 0

Proof state:
case intro
R : Type u
inst✝ : CommRing R
I : Ideal R
x : R
hx : x ∈ I
m : ↥I
⊢ x • I.toCotangent m = 0

Tactic:
rw [← map_smul, Ideal.toCotangent_eq_zero, pow_two]

Result:
case intro
R : Type u
inst✝ : CommRing R
I : Ideal R
x : R
hx : x ∈ I
m : ↥I
⊢ ↑(x • m) ∈ I * I

Proof state:
case intro
R : Type u
inst✝ : CommRing R
I : Ideal R
x : R
hx : x ∈ I
m : ↥I
⊢ ↑(x • m) ∈ I * I

Tactic:
exact Ideal.mul_mem_mul hx m.2

Result:
no goals

Proof state:
R : Type u
inst✝ : CommRing R
I : Ideal R
x : R
hx : x ∈ I
m : I.Cotangent
⊢ x • m = 0

Tactic:
obtain ⟨m, rfl⟩ := Ideal.toCotangent_surjective _ m

Result:
case intro
R : Type u
inst✝ : CommRing R
I : Ideal R
x : R
hx : x ∈ I
m : ↥I
⊢ x • I.toCotangent m = 0
-- Mathlib/Algebra/Order/Ring/WithTop.lean
theorem mul_lt_top [LT α] {a b : WithTop α} (ha : a < ⊤) (hb : b < ⊤) : a * b < ⊤

Proof state:
α : Type u_1
inst✝² : DecidableEq α
inst✝¹ : MulZeroClass α
inst✝ : LT α
a b : WithTop α
ha : a ≠ ⊤
hb : b ≠ ⊤
⊢ a * b ≠ ⊤

Tactic:
exact mul_ne_top ha hb

Result:
no goals

Proof state:
α : Type u_1
inst✝² : DecidableEq α
inst✝¹ : MulZeroClass α
inst✝ : LT α
a b : WithTop α
ha : a < ⊤
hb : b < ⊤
⊢ a * b < ⊤

Tactic:
rw [WithTop.lt_top_iff_ne_top] at *

Result:
α : Type u_1
inst✝² : DecidableEq α
inst✝¹ : MulZeroClass α
inst✝ : LT α
a b : WithTop α
ha : a ≠ ⊤
hb : b ≠ ⊤
⊢ a * b ≠ ⊤
-- Mathlib/Combinatorics/SimpleGraph/Regularity/Uniform.lean
@[simp]
lemma mk_mem_sparsePairs (u v : Finset α) (ε : 𝕜) :
    (u, v) ∈ P.sparsePairs G ε ↔ u ∈ P.parts ∧ v ∈ P.parts ∧ u ≠ v ∧ G.edgeDensity u v < ε

Proof state:
α : Type u_1
𝕜 : Type u_2
inst✝² : LinearOrderedField 𝕜
inst✝¹ : DecidableEq α
A : Finset α
P : Finpartition A
G : SimpleGraph α
inst✝ : DecidableRel G.Adj
u v : Finset α
ε : 𝕜
⊢ (u, v) ∈ P.sparsePairs G ε ↔ u ∈ P.parts ∧ v ∈ P.parts ∧ u ≠ v ∧ ↑(G.edgeDensity u v) < ε

Tactic:
rw [sparsePairs, mem_filter, mem_offDiag, and_assoc, and_assoc]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/List/Lemmas.lean
theorem mem_flatten : ∀ {L : List (List α)}, a ∈ L.flatten ↔ ∃ l, l ∈ L ∧ a ∈ l
  | [] => by simp
  | b :: l => by simp [mem_flatten, or_and_right, exists_or]

Proof state:
α : Type u_1
a : α
b : List α
l : List (List α)
⊢ a ∈ (b :: l).flatten ↔ ∃ l_1, l_1 ∈ b :: l ∧ a ∈ l_1

Tactic:
simp [mem_flatten, or_and_right, exists_or]

Result:
no goals

Proof state:
α : Type u_1
a : α
⊢ a ∈ [].flatten ↔ ∃ l, l ∈ [] ∧ a ∈ l

Tactic:
simp

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Std/Tactic/BVDecide/LRAT/Internal/Entails.lean
theorem unsat_of_limplies_and_incompatible (α : Type u) {σ1 : Type v} {σ2 : Type w} [Entails α σ1]
    [Entails α σ2] (f1 : σ1) (f2 : σ2) :
    Limplies α f1 f2 → Incompatible α f1 f2 → Unsatisfiable α f1

Proof state:
α : Type u
σ1 : Type v
σ2 : Type w
inst✝¹ : Entails α σ1
inst✝ : Entails α σ2
f1 : σ1
f2 : σ2
h1 : Limplies α f1 f2
h2 : Incompatible α f1 f2
a : α → Bool
af1 : a ⊨ f1
⊢ False

Tactic:
cases h2 a

Result:
case inl
α : Type u
σ1 : Type v
σ2 : Type w
inst✝¹ : Entails α σ1
inst✝ : Entails α σ2
f1 : σ1
f2 : σ2
h1 : Limplies α f1 f2
h2 : Incompatible α f1 f2
a : α → Bool
af1 : a ⊨ f1
h✝ : ¬(a ⊨ f1)
⊢ False

case inr
α : Type u
σ1 : Type v
σ2 : Type w
inst✝¹ : Entails α σ1
inst✝ : Entails α σ2
f1 : σ1
f2 : σ2
h1 : Limplies α f1 f2
h2 : Incompatible α f1 f2
a : α → Bool
af1 : a ⊨ f1
h✝ : ¬(a ⊨ f2)
⊢ False

Proof state:
α : Type u
σ1 : Type v
σ2 : Type w
inst✝¹ : Entails α σ1
inst✝ : Entails α σ2
f1 : σ1
f2 : σ2
h1 : Limplies α f1 f2
h2✝ : Incompatible α f1 f2
a : α → Bool
af1 : a ⊨ f1
h2 : ¬(a ⊨ f2)
⊢ False

Tactic:
exact h2 <| h1 a af1

Result:
no goals

Proof state:
case inl
α : Type u
σ1 : Type v
σ2 : Type w
inst✝¹ : Entails α σ1
inst✝ : Entails α σ2
f1 : σ1
f2 : σ2
h1 : Limplies α f1 f2
h2 : Incompatible α f1 f2
a : α → Bool
af1 : a ⊨ f1
h✝ : ¬(a ⊨ f1)
⊢ False

Tactic:
next h2 =>
exact h2 af1

Result:
no goals

Proof state:
α : Type u
σ1 : Type v
σ2 : Type w
inst✝¹ : Entails α σ1
inst✝ : Entails α σ2
f1 : σ1
f2 : σ2
h1 : Limplies α f1 f2
h2✝ : Incompatible α f1 f2
a : α → Bool
af1 : a ⊨ f1
h2 : ¬(a ⊨ f1)
⊢ False

Tactic:
exact h2 af1

Result:
no goals

Proof state:
case inr
α : Type u
σ1 : Type v
σ2 : Type w
inst✝¹ : Entails α σ1
inst✝ : Entails α σ2
f1 : σ1
f2 : σ2
h1 : Limplies α f1 f2
h2 : Incompatible α f1 f2
a : α → Bool
af1 : a ⊨ f1
h✝ : ¬(a ⊨ f2)
⊢ False

Tactic:
next h2 =>
exact h2 <| h1 a af1

Result:
no goals

Proof state:
α : Type u
σ1 : Type v
σ2 : Type w
inst✝¹ : Entails α σ1
inst✝ : Entails α σ2
f1 : σ1
f2 : σ2
⊢ Limplies α f1 f2 → Incompatible α f1 f2 → Unsatisfiable α f1

Tactic:
intro h1 h2 a af1

Result:
α : Type u
σ1 : Type v
σ2 : Type w
inst✝¹ : Entails α σ1
inst✝ : Entails α σ2
f1 : σ1
f2 : σ2
h1 : Limplies α f1 f2
h2 : Incompatible α f1 f2
a : α → Bool
af1 : a ⊨ f1
⊢ False
-- Mathlib/Combinatorics/SimpleGraph/Basic.lean
theorem ne_of_adj (h : G.Adj a b) : a ≠ b

Proof state:
V : Type u
G : SimpleGraph V
a b : V
h : G.Adj a b
⊢ a ≠ b

Tactic:
rintro rfl

Result:
V : Type u
G : SimpleGraph V
a : V
h : G.Adj a a
⊢ False

Proof state:
V : Type u
G : SimpleGraph V
a : V
h : G.Adj a a
⊢ False

Tactic:
exact G.irrefl h

Result:
no goals
-- Mathlib/RingTheory/Polynomial/Basic.lean
theorem not_finite [Nontrivial R] : ¬ Module.Finite R R[X]

Proof state:
R : Type u
inst✝¹ : Semiring R
inst✝ : Nontrivial R
⊢ ∀ (S : Set R[X]), S.Finite → Submodule.span R S ≠ ⊤

Tactic:
intro s hs contra

Result:
R : Type u
inst✝¹ : Semiring R
inst✝ : Nontrivial R
s : Set R[X]
hs : s.Finite
contra : Submodule.span R s = ⊤
⊢ False

Proof state:
R : Type u
inst✝¹ : Semiring R
inst✝ : Nontrivial R
⊢ ¬∃ S, S.Finite ∧ Submodule.span R S = ⊤

Tactic:
push_neg

Result:
R : Type u
inst✝¹ : Semiring R
inst✝ : Nontrivial R
⊢ ∀ (S : Set R[X]), S.Finite → Submodule.span R S ≠ ⊤

Proof state:
R : Type u
inst✝¹ : Semiring R
inst✝ : Nontrivial R
s : Set R[X]
hs : s.Finite
contra : Submodule.span R s = ⊤
⊢ False

Tactic:
rcases span_le_degreeLE_of_finite hs with ⟨n,hn⟩

Result:
case intro
R : Type u
inst✝¹ : Semiring R
inst✝ : Nontrivial R
s : Set R[X]
hs : s.Finite
contra : Submodule.span R s = ⊤
n : ℕ
hn : Submodule.span R s ≤ degreeLE R ↑n
⊢ False

Proof state:
case intro
R : Type u
inst✝¹ : Semiring R
inst✝ : Nontrivial R
s : Set R[X]
hs : s.Finite
contra : Submodule.span R s = ⊤
n : ℕ
hn : Submodule.span R s ≤ degreeLE R ↑n
this : X ^ (n + 1) ∈ degreeLE R ↑n
⊢ False

Tactic:
rw [mem_degreeLE, degree_X_pow, Nat.cast_le, add_le_iff_nonpos_right, nonpos_iff_eq_zero] at this

Result:
case intro
R : Type u
inst✝¹ : Semiring R
inst✝ : Nontrivial R
s : Set R[X]
hs : s.Finite
contra : Submodule.span R s = ⊤
n : ℕ
hn : Submodule.span R s ≤ degreeLE R ↑n
this : 1 = 0
⊢ False

Proof state:
R : Type u
inst✝¹ : Semiring R
inst✝ : Nontrivial R
⊢ ¬Module.Finite R R[X]

Tactic:
rw [Module.finite_def, Submodule.fg_def]

Result:
R : Type u
inst✝¹ : Semiring R
inst✝ : Nontrivial R
⊢ ¬∃ S, S.Finite ∧ Submodule.span R S = ⊤

Proof state:
case intro
R : Type u
inst✝¹ : Semiring R
inst✝ : Nontrivial R
s : Set R[X]
hs : s.Finite
contra : Submodule.span R s = ⊤
n : ℕ
hn : Submodule.span R s ≤ degreeLE R ↑n
this : 1 = 0
⊢ False

Tactic:
exact one_ne_zero this

Result:
no goals

Proof state:
R : Type u
inst✝¹ : Semiring R
inst✝ : Nontrivial R
s : Set R[X]
hs : s.Finite
contra : Submodule.span R s = ⊤
n : ℕ
hn : ⊤ ≤ degreeLE R ↑n
⊢ X ^ (n + 1) ∈ degreeLE R ↑n

Tactic:
exact hn Submodule.mem_top

Result:
no goals

Proof state:
case intro
R : Type u
inst✝¹ : Semiring R
inst✝ : Nontrivial R
s : Set R[X]
hs : s.Finite
contra : Submodule.span R s = ⊤
n : ℕ
hn : Submodule.span R s ≤ degreeLE R ↑n
⊢ False

Tactic:
have : ((X : R[X]) ^ (n + 1)) ∈ Polynomial.degreeLE R ↑n := by
  rw [contra] at hn
  exact hn Submodule.mem_top

Result:
case intro
R : Type u
inst✝¹ : Semiring R
inst✝ : Nontrivial R
s : Set R[X]
hs : s.Finite
contra : Submodule.span R s = ⊤
n : ℕ
hn : Submodule.span R s ≤ degreeLE R ↑n
this : X ^ (n + 1) ∈ degreeLE R ↑n
⊢ False

Proof state:
R : Type u
inst✝¹ : Semiring R
inst✝ : Nontrivial R
s : Set R[X]
hs : s.Finite
contra : Submodule.span R s = ⊤
n : ℕ
hn : Submodule.span R s ≤ degreeLE R ↑n
⊢ X ^ (n + 1) ∈ degreeLE R ↑n

Tactic:
rw [contra] at hn

Result:
R : Type u
inst✝¹ : Semiring R
inst✝ : Nontrivial R
s : Set R[X]
hs : s.Finite
contra : Submodule.span R s = ⊤
n : ℕ
hn : ⊤ ≤ degreeLE R ↑n
⊢ X ^ (n + 1) ∈ degreeLE R ↑n
-- Mathlib/Dynamics/OmegaLimit.lean
theorem omegaLimit_subset_of_tendsto {m : τ → τ} {f₁ f₂ : Filter τ} (hf : Tendsto m f₁ f₂) :
    ω f₁ (fun t x ↦ ϕ (m t) x) s ⊆ ω f₂ ϕ s

Proof state:
τ : Type u_1
α : Type u_2
β : Type u_3
inst✝ : TopologicalSpace β
ϕ : τ → α → β
s : Set α
m : τ → τ
f₁ f₂ : Filter τ
hf : Tendsto m f₁ f₂
u : Set τ
hu : u ∈ f₂
⊢ closure (image2 ϕ (m '' (m ⁻¹' u)) s) ⊆ closure (image2 ϕ u s)

Tactic:
exact closure_mono (image2_subset (image_preimage_subset _ _) Subset.rfl)

Result:
no goals

Proof state:
τ : Type u_1
α : Type u_2
β : Type u_3
inst✝ : TopologicalSpace β
ϕ : τ → α → β
s : Set α
m : τ → τ
f₁ f₂ : Filter τ
hf : Tendsto m f₁ f₂
u : Set τ
hu : u ∈ f₂
⊢ closure (image2 (fun t x => ϕ (m t) x) (m ⁻¹' u) s) ⊆ closure (image2 ϕ u s)

Tactic:
rw [← image2_image_left]

Result:
τ : Type u_1
α : Type u_2
β : Type u_3
inst✝ : TopologicalSpace β
ϕ : τ → α → β
s : Set α
m : τ → τ
f₁ f₂ : Filter τ
hf : Tendsto m f₁ f₂
u : Set τ
hu : u ∈ f₂
⊢ closure (image2 ϕ (m '' (m ⁻¹' u)) s) ⊆ closure (image2 ϕ u s)

Proof state:
τ : Type u_1
α : Type u_2
β : Type u_3
inst✝ : TopologicalSpace β
ϕ : τ → α → β
s : Set α
m : τ → τ
f₁ f₂ : Filter τ
hf : Tendsto m f₁ f₂
⊢ ω f₁ (fun t x => ϕ (m t) x) s ⊆ ω f₂ ϕ s

Tactic:
refine iInter₂_mono' fun u hu ↦ ⟨m ⁻¹' u, tendsto_def.mp hf _ hu, ?_⟩

Result:
τ : Type u_1
α : Type u_2
β : Type u_3
inst✝ : TopologicalSpace β
ϕ : τ → α → β
s : Set α
m : τ → τ
f₁ f₂ : Filter τ
hf : Tendsto m f₁ f₂
u : Set τ
hu : u ∈ f₂
⊢ closure (image2 (fun t x => ϕ (m t) x) (m ⁻¹' u) s) ⊆ closure (image2 ϕ u s)
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Nat/Bitwise/Lemmas.lean
theorem testBit_mod_two_pow (x j i : Nat) :
    testBit (x % 2^j) i = (decide (i < j) && testBit x i)

Proof state:
case ind.inl.inr
x : Nat
hyp : ∀ (m : Nat), m < x → ∀ (j i : Nat), (m % 2 ^ j).testBit i = (decide (i < j) && m.testBit i)
j i : Nat
x_lt_j : x < 2 ^ j
not_j_le_x : ¬2 ^ j ≤ x
i_ge_j : i ≥ j
x_lt : x < 2 ^ i
⊢ x.testBit i = true → i < j

Tactic:
simp [Nat.testBit_lt_two_pow x_lt]

Result:
no goals

Proof state:
case ind.inr
x : Nat
hyp : ∀ (m : Nat), m < x → ∀ (j i : Nat), (m % 2 ^ j).testBit i = (decide (i < j) && m.testBit i)
j i : Nat
x_ge_j : x ≥ 2 ^ j
y : Nat
y_eq : x - 2 ^ j = y
x_eq : x = y + 2 ^ j
⊢ (y % 2 ^ j).testBit i = (decide (i < j) && (y + 2 ^ j).testBit i)

Tactic:
have y_lt_x : y < x := by
  simp only [x_eq, Nat.lt_add_right_iff_pos]
  exact Nat.two_pow_pos j

Result:
case ind.inr
x : Nat
hyp : ∀ (m : Nat), m < x → ∀ (j i : Nat), (m % 2 ^ j).testBit i = (decide (i < j) && m.testBit i)
j i : Nat
x_ge_j : x ≥ 2 ^ j
y : Nat
y_eq : x - 2 ^ j = y
x_eq : x = y + 2 ^ j
y_lt_x : y < x
⊢ (y % 2 ^ j).testBit i = (decide (i < j) && (y + 2 ^ j).testBit i)

Proof state:
case ind
x : Nat
hyp : ∀ (m : Nat), m < x → ∀ (j i : Nat), (m % 2 ^ j).testBit i = (decide (i < j) && m.testBit i)
j i : Nat
⊢ (if 0 < 2 ^ j ∧ 2 ^ j ≤ x then (x - 2 ^ j) % 2 ^ j else x).testBit i = (decide (i < j) && x.testBit i)

Tactic:
rcases Nat.lt_or_ge x (2^j) with x_lt_j | x_ge_j

Result:
case ind.inl
x : Nat
hyp : ∀ (m : Nat), m < x → ∀ (j i : Nat), (m % 2 ^ j).testBit i = (decide (i < j) && m.testBit i)
j i : Nat
x_lt_j : x < 2 ^ j
⊢ (if 0 < 2 ^ j ∧ 2 ^ j ≤ x then (x - 2 ^ j) % 2 ^ j else x).testBit i = (decide (i < j) && x.testBit i)

case ind.inr
x : Nat
hyp : ∀ (m : Nat), m < x → ∀ (j i : Nat), (m % 2 ^ j).testBit i = (decide (i < j) && m.testBit i)
j i : Nat
x_ge_j : x ≥ 2 ^ j
⊢ (if 0 < 2 ^ j ∧ 2 ^ j ≤ x then (x - 2 ^ j) % 2 ^ j else x).testBit i = (decide (i < j) && x.testBit i)
-- Mathlib/MeasureTheory/Function/LpSeminorm/Basic.lean
theorem eLpNorm_neg (f : α → F) (p : ℝ≥0∞) (μ : Measure α) : eLpNorm (-f) p μ = eLpNorm f p μ

Proof state:
case neg
α : Type u_1
F : Type u_4
m0 : MeasurableSpace α
inst✝ : NormedAddCommGroup F
f : α → F
p : ℝ≥0∞
μ : Measure α
h0 : ¬p = 0
h_top : ¬p = ⊤
⊢ eLpNorm (-f) p μ = eLpNorm f p μ

Tactic:
simp [eLpNorm_eq_eLpNorm' h0 h_top]

Result:
no goals

Proof state:
case neg
α : Type u_1
F : Type u_4
m0 : MeasurableSpace α
inst✝ : NormedAddCommGroup F
f : α → F
p : ℝ≥0∞
μ : Measure α
h0 : ¬p = 0
⊢ eLpNorm (-f) p μ = eLpNorm f p μ

Tactic:
by_cases h_top : p = ∞

Result:
case pos
α : Type u_1
F : Type u_4
m0 : MeasurableSpace α
inst✝ : NormedAddCommGroup F
f : α → F
p : ℝ≥0∞
μ : Measure α
h0 : ¬p = 0
h_top : p = ⊤
⊢ eLpNorm (-f) p μ = eLpNorm f p μ

case neg
α : Type u_1
F : Type u_4
m0 : MeasurableSpace α
inst✝ : NormedAddCommGroup F
f : α → F
p : ℝ≥0∞
μ : Measure α
h0 : ¬p = 0
h_top : ¬p = ⊤
⊢ eLpNorm (-f) p μ = eLpNorm f p μ

Proof state:
case pos
α : Type u_1
F : Type u_4
m0 : MeasurableSpace α
inst✝ : NormedAddCommGroup F
f : α → F
p : ℝ≥0∞
μ : Measure α
h0 : p = 0
⊢ eLpNorm (-f) p μ = eLpNorm f p μ

Tactic:
simp [h0]

Result:
no goals

Proof state:
α : Type u_1
F : Type u_4
m0 : MeasurableSpace α
inst✝ : NormedAddCommGroup F
f : α → F
p : ℝ≥0∞
μ : Measure α
⊢ eLpNorm (-f) p μ = eLpNorm f p μ

Tactic:
by_cases h0 : p = 0

Result:
case pos
α : Type u_1
F : Type u_4
m0 : MeasurableSpace α
inst✝ : NormedAddCommGroup F
f : α → F
p : ℝ≥0∞
μ : Measure α
h0 : p = 0
⊢ eLpNorm (-f) p μ = eLpNorm f p μ

case neg
α : Type u_1
F : Type u_4
m0 : MeasurableSpace α
inst✝ : NormedAddCommGroup F
f : α → F
p : ℝ≥0∞
μ : Measure α
h0 : ¬p = 0
⊢ eLpNorm (-f) p μ = eLpNorm f p μ

Proof state:
case pos
α : Type u_1
F : Type u_4
m0 : MeasurableSpace α
inst✝ : NormedAddCommGroup F
f : α → F
p : ℝ≥0∞
μ : Measure α
h0 : ¬p = 0
h_top : p = ⊤
⊢ eLpNorm (-f) p μ = eLpNorm f p μ

Tactic:
simp [h_top, eLpNormEssSup_eq_essSup_enorm]

Result:
no goals
-- Mathlib/Analysis/SpecialFunctions/Pow/Complex.lean
theorem cpow_add {x : ℂ} (y z : ℂ) (hx : x ≠ 0) : x ^ (y + z) = x ^ y * x ^ z

Proof state:
x y z : ℂ
hx : x ≠ 0
⊢ (if x = 0 then if y + z = 0 then 1 else 0 else cexp (log x * (y + z))) =
    if x = 0 then
      if z = 0 then if x = 0 then if y = 0 then 1 * 1 else 0 * 1 else cexp (log x * y) * 1
      else if x = 0 then if y = 0 then 1 * 0 else 0 * 0 else cexp (log x * y) * 0
    else
      if x = 0 then if y = 0 then 1 * cexp (log x * z) else 0 * cexp (log x * z)
      else cexp (log x * y) * cexp (log x * z)

Tactic:
simp_all [exp_add, mul_add]

Result:
no goals

Proof state:
x y z : ℂ
hx : x ≠ 0
⊢ x ^ (y + z) = x ^ y * x ^ z

Tactic:
simp only [cpow_def, ite_mul, boole_mul, mul_ite, mul_boole]

Result:
x y z : ℂ
hx : x ≠ 0
⊢ (if x = 0 then if y + z = 0 then 1 else 0 else cexp (log x * (y + z))) =
    if x = 0 then
      if z = 0 then if x = 0 then if y = 0 then 1 * 1 else 0 * 1 else cexp (log x * y) * 1
      else if x = 0 then if y = 0 then 1 * 0 else 0 * 0 else cexp (log x * y) * 0
    else
      if x = 0 then if y = 0 then 1 * cexp (log x * z) else 0 * cexp (log x * z)
      else cexp (log x * y) * cexp (log x * z)
-- Mathlib/LinearAlgebra/AffineSpace/Pointwise.lean
theorem map_pointwise_vadd (f : P₁ →ᵃ[k] P₂) (v : V₁) (s : AffineSubspace k P₁) :
    (v +ᵥ s).map f = f.linear v +ᵥ s.map f

Proof state:
k : Type u_2
V₁ : Type u_5
P₁ : Type u_6
V₂ : Type u_7
P₂ : Type u_8
inst✝⁶ : Ring k
inst✝⁵ : AddCommGroup V₁
inst✝⁴ : Module k V₁
inst✝³ : AffineSpace V₁ P₁
inst✝² : AddCommGroup V₂
inst✝¹ : Module k V₂
inst✝ : AffineSpace V₂ P₂
f : P₁ →ᵃ[k] P₂
v : V₁
s : AffineSubspace k P₁
⊢ map (f.comp ↑(AffineEquiv.constVAdd k P₁ v)) s = map ((↑(AffineEquiv.constVAdd k P₂ (f.linear v))).comp f) s

Tactic:
congr 1

Result:
case e_f
k : Type u_2
V₁ : Type u_5
P₁ : Type u_6
V₂ : Type u_7
P₂ : Type u_8
inst✝⁶ : Ring k
inst✝⁵ : AddCommGroup V₁
inst✝⁴ : Module k V₁
inst✝³ : AffineSpace V₁ P₁
inst✝² : AddCommGroup V₂
inst✝¹ : Module k V₂
inst✝ : AffineSpace V₂ P₂
f : P₁ →ᵃ[k] P₂
v : V₁
s : AffineSubspace k P₁
⊢ f.comp ↑(AffineEquiv.constVAdd k P₁ v) = (↑(AffineEquiv.constVAdd k P₂ (f.linear v))).comp f

Proof state:
case e_f.h
k : Type u_2
V₁ : Type u_5
P₁ : Type u_6
V₂ : Type u_7
P₂ : Type u_8
inst✝⁶ : Ring k
inst✝⁵ : AddCommGroup V₁
inst✝⁴ : Module k V₁
inst✝³ : AffineSpace V₁ P₁
inst✝² : AddCommGroup V₂
inst✝¹ : Module k V₂
inst✝ : AffineSpace V₂ P₂
f : P₁ →ᵃ[k] P₂
v : V₁
s : AffineSubspace k P₁
p✝ : P₁
⊢ (f.comp ↑(AffineEquiv.constVAdd k P₁ v)) p✝ = ((↑(AffineEquiv.constVAdd k P₂ (f.linear v))).comp f) p✝

Tactic:
exact f.map_vadd _ _

Result:
no goals

Proof state:
k : Type u_2
V₁ : Type u_5
P₁ : Type u_6
V₂ : Type u_7
P₂ : Type u_8
inst✝⁶ : Ring k
inst✝⁵ : AddCommGroup V₁
inst✝⁴ : Module k V₁
inst✝³ : AffineSpace V₁ P₁
inst✝² : AddCommGroup V₂
inst✝¹ : Module k V₂
inst✝ : AffineSpace V₂ P₂
f : P₁ →ᵃ[k] P₂
v : V₁
s : AffineSubspace k P₁
⊢ map f (v +ᵥ s) = f.linear v +ᵥ map f s

Tactic:
rw [pointwise_vadd_eq_map, pointwise_vadd_eq_map, map_map, map_map]

Result:
k : Type u_2
V₁ : Type u_5
P₁ : Type u_6
V₂ : Type u_7
P₂ : Type u_8
inst✝⁶ : Ring k
inst✝⁵ : AddCommGroup V₁
inst✝⁴ : Module k V₁
inst✝³ : AffineSpace V₁ P₁
inst✝² : AddCommGroup V₂
inst✝¹ : Module k V₂
inst✝ : AffineSpace V₂ P₂
f : P₁ →ᵃ[k] P₂
v : V₁
s : AffineSubspace k P₁
⊢ map (f.comp ↑(AffineEquiv.constVAdd k P₁ v)) s = map ((↑(AffineEquiv.constVAdd k P₂ (f.linear v))).comp f) s

Proof state:
case e_f
k : Type u_2
V₁ : Type u_5
P₁ : Type u_6
V₂ : Type u_7
P₂ : Type u_8
inst✝⁶ : Ring k
inst✝⁵ : AddCommGroup V₁
inst✝⁴ : Module k V₁
inst✝³ : AffineSpace V₁ P₁
inst✝² : AddCommGroup V₂
inst✝¹ : Module k V₂
inst✝ : AffineSpace V₂ P₂
f : P₁ →ᵃ[k] P₂
v : V₁
s : AffineSubspace k P₁
⊢ f.comp ↑(AffineEquiv.constVAdd k P₁ v) = (↑(AffineEquiv.constVAdd k P₂ (f.linear v))).comp f

Tactic:
ext

Result:
case e_f.h
k : Type u_2
V₁ : Type u_5
P₁ : Type u_6
V₂ : Type u_7
P₂ : Type u_8
inst✝⁶ : Ring k
inst✝⁵ : AddCommGroup V₁
inst✝⁴ : Module k V₁
inst✝³ : AffineSpace V₁ P₁
inst✝² : AddCommGroup V₂
inst✝¹ : Module k V₂
inst✝ : AffineSpace V₂ P₂
f : P₁ →ᵃ[k] P₂
v : V₁
s : AffineSubspace k P₁
p✝ : P₁
⊢ (f.comp ↑(AffineEquiv.constVAdd k P₁ v)) p✝ = ((↑(AffineEquiv.constVAdd k P₂ (f.linear v))).comp f) p✝