harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/Dynamics/TopologicalEntropy/CoverEntropy.lean
lemma coverMincard_finite_of_isCompact_uniformContinuous [UniformSpace X] {T : X → X}
    {F : Set X} (F_comp : IsCompact F) (h : UniformContinuous T) {U : Set (X × X)} (U_uni : U ∈ 𝓤 X)
    (n : ℕ) :
    coverMincard T F U n < ⊤

Proof state:
case intro
X : Type u_1
inst✝ : UniformSpace X
T : X → X
F : Set X
F_comp : IsCompact F
h : UniformContinuous T
U : Set (X × X)
U_uni : U ∈ 𝓤 X
n : ℕ
s : Finset X
s_cover : IsDynCoverOf T F U n ↑s
⊢ coverMincard T F U n < ⊤

Tactic:
exact s_cover.coverMincard_le_card.trans_lt (WithTop.coe_lt_top s.card)

Result:
no goals

Proof state:
X : Type u_1
inst✝ : UniformSpace X
T : X → X
F : Set X
F_comp : IsCompact F
h : UniformContinuous T
U : Set (X × X)
U_uni : U ∈ 𝓤 X
n : ℕ
⊢ coverMincard T F U n < ⊤

Tactic:
rcases exists_isDynCoverOf_of_isCompact_uniformContinuous F_comp h U_uni n with ⟨s, s_cover⟩

Result:
case intro
X : Type u_1
inst✝ : UniformSpace X
T : X → X
F : Set X
F_comp : IsCompact F
h : UniformContinuous T
U : Set (X × X)
U_uni : U ∈ 𝓤 X
n : ℕ
s : Finset X
s_cover : IsDynCoverOf T F U n ↑s
⊢ coverMincard T F U n < ⊤
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/List/Lex.lean
theorem not_lex_total [DecidableEq α] {r : α → α → Prop} [DecidableRel r]
    (h : ∀ x y : α, ¬ r x y ∨ ¬ r y x) (l₁ l₂ : List α) : ¬ Lex r l₁ l₂ ∨ ¬ Lex r l₂ l₁

Proof state:
α : Type u_1
inst✝¹ : DecidableEq α
r : α → α → Prop
inst✝ : DecidableRel r
h : ∀ (x y : α), ¬r x y ∨ ¬r y x
l₁ l₂ : List α
⊢ ¬Lex r l₁ l₂ ∨ ¬Lex r l₂ l₁

Tactic:
rw [Decidable.or_iff_not_imp_left, Decidable.not_not]

Result:
α : Type u_1
inst✝¹ : DecidableEq α
r : α → α → Prop
inst✝ : DecidableRel r
h : ∀ (x y : α), ¬r x y ∨ ¬r y x
l₁ l₂ : List α
⊢ Lex r l₁ l₂ → ¬Lex r l₂ l₁

Proof state:
α : Type u_1
inst✝¹ : DecidableEq α
r : α → α → Prop
inst✝ : DecidableRel r
h : ∀ (x y : α), ¬r x y ∨ ¬r y x
l₁ l₂ : List α
w₁ : Lex r l₁ l₂
w₂ : Lex r l₂ l₁
x : α
tail✝¹ tail✝ : List α
h✝¹ : Lex r tail✝¹ tail✝
h✝ : r x x
⊢ False

Tactic:
obtain (_ | _) := h x x <;> contradiction

Result:
no goals

Proof state:
α : Type u_1
inst✝¹ : DecidableEq α
r : α → α → Prop
inst✝ : DecidableRel r
h : ∀ (x y : α), ¬r x y ∨ ¬r y x
l₁ l₂ : List α
w₁ : Lex r l₁ l₂
w₂ : Lex r l₂ l₁
x : α
tail✝¹ tail✝ : List α
h✝¹ : r x x
h✝ : Lex r tail✝ tail✝¹
⊢ False

Tactic:
obtain (_ | _) := h x x <;> contradiction

Result:
no goals

Proof state:
α : Type u_1
inst✝¹ : DecidableEq α
r : α → α → Prop
inst✝ : DecidableRel r
h : ∀ (x y : α), ¬r x y ∨ ¬r y x
l₁ l₂ : List α
w₁ : Lex r l₁ l₂
w₂ : Lex r l₂ l₁
⊢ False

Tactic:
match l₁, l₂, w₁, w₂ with
| nil, _ :: _, .nil, w₂ => simp at w₂
| x :: _, y :: _, .rel _, .rel _ =>
  obtain (_ | _) := h x y <;> contradiction
| x :: _, _ :: _, .rel _, .cons _ =>
  obtain (_ | _) := h x x <;> contradiction
| x :: _, _ :: _, .cons  _, .rel _ =>
  obtain (_ | _) := h x x <;> contradiction
| _ :: l₁, _ :: l₂, .cons _, .cons _ =>
  obtain (_ | _) := not_lex_total h l₁ l₂ <;> contradiction

Result:
no goals

Proof state:
α : Type u_1
inst✝¹ : DecidableEq α
r : α → α → Prop
inst✝ : DecidableRel r
h : ∀ (x y : α), ¬r x y ∨ ¬r y x
l₁ l₂ : List α
w₁ : Lex r l₁ l₂
w₂ : Lex r l₂ l₁
x : α
tail✝¹ : List α
y : α
tail✝ : List α
h✝¹ : r x y
h✝ : r y x
⊢ False

Tactic:
obtain (_ | _) := h x y <;> contradiction

Result:
no goals

Proof state:
α : Type u_1
inst✝¹ : DecidableEq α
r : α → α → Prop
inst✝ : DecidableRel r
h : ∀ (x y : α), ¬r x y ∨ ¬r y x
l₁✝ l₂✝ : List α
w₁ : Lex r l₁✝ l₂✝
w₂ : Lex r l₂✝ l₁✝
head✝ : α
l₁ l₂ : List α
h✝¹ : Lex r l₁ l₂
h✝ : Lex r l₂ l₁
⊢ False

Tactic:
obtain (_ | _) := not_lex_total h l₁ l₂ <;> contradiction

Result:
no goals

Proof state:
α : Type u_1
inst✝¹ : DecidableEq α
r : α → α → Prop
inst✝ : DecidableRel r
h : ∀ (x y : α), ¬r x y ∨ ¬r y x
l₁ l₂ : List α
w₁ : Lex r l₁ l₂
w₂✝ : Lex r l₂ l₁
head✝ : α
tail✝ : List α
w₂ : Lex r (head✝ :: tail✝) []
⊢ False

Tactic:
simp at w₂

Result:
no goals

Proof state:
α : Type u_1
inst✝¹ : DecidableEq α
r : α → α → Prop
inst✝ : DecidableRel r
h : ∀ (x y : α), ¬r x y ∨ ¬r y x
l₁ l₂ : List α
⊢ Lex r l₁ l₂ → ¬Lex r l₂ l₁

Tactic:
intro w₁ w₂

Result:
α : Type u_1
inst✝¹ : DecidableEq α
r : α → α → Prop
inst✝ : DecidableRel r
h : ∀ (x y : α), ¬r x y ∨ ¬r y x
l₁ l₂ : List α
w₁ : Lex r l₁ l₂
w₂ : Lex r l₂ l₁
⊢ False
-- Mathlib/Order/Filter/Partial.lean
theorem tendsto_iff_rtendsto (l₁ : Filter α) (l₂ : Filter β) (f : α → β) :
    Tendsto f l₁ l₂ ↔ RTendsto (Function.graph f) l₁ l₂

Proof state:
α : Type u
β : Type v
l₁ : Filter α
l₂ : Filter β
f : α → β
⊢ Tendsto f l₁ l₂ ↔ RTendsto (Function.graph f) l₁ l₂

Tactic:
simp [tendsto_def, Function.graph, rtendsto_def, Rel.core, Set.preimage]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/BitVec/Lemmas.lean
theorem and_cast {x y : BitVec w} (h : w = w') : x.cast h &&& y.cast h = (x &&& y).cast h

Proof state:
case pred
w w' : Nat
x y : BitVec w
h : w = w'
i✝ : Nat
a✝ : i✝ < w'
⊢ (BitVec.cast h x &&& BitVec.cast h y).getLsbD i✝ = (BitVec.cast h (x &&& y)).getLsbD i✝

Tactic:
simp_all [lt_of_getLsbD]

Result:
no goals

Proof state:
w w' : Nat
x y : BitVec w
h : w = w'
⊢ BitVec.cast h x &&& BitVec.cast h y = BitVec.cast h (x &&& y)

Tactic:
ext

Result:
case pred
w w' : Nat
x y : BitVec w
h : w = w'
i✝ : Nat
a✝ : i✝ < w'
⊢ (BitVec.cast h x &&& BitVec.cast h y).getLsbD i✝ = (BitVec.cast h (x &&& y)).getLsbD i✝
-- Mathlib/Probability/Distributions/Gamma.lean
/-- The gamma pdf is positive for all positive reals -/
lemma gammaPDFReal_pos {x a r : ℝ} (ha : 0 < a) (hr : 0 < r) (hx : 0 < x) :
    0 < gammaPDFReal a r x

Proof state:
x a r : ℝ
ha : 0 < a
hr : 0 < r
hx : 0 < x
⊢ 0 < gammaPDFReal a r x

Tactic:
simp only [gammaPDFReal, if_pos hx.le]

Result:
x a r : ℝ
ha : 0 < a
hr : 0 < r
hx : 0 < x
⊢ 0 < r ^ a / Gamma a * x ^ (a - 1) * rexp (-(r * x))

Proof state:
x a r : ℝ
ha : 0 < a
hr : 0 < r
hx : 0 < x
⊢ 0 < r ^ a / Gamma a * x ^ (a - 1) * rexp (-(r * x))

Tactic:
positivity

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/BitVec/Lemmas.lean
theorem sshiftRight_or_distrib (x y : BitVec w) (n : Nat) :
    (x ||| y).sshiftRight n = (x.sshiftRight n) ||| (y.sshiftRight n)

Proof state:
case pred
w : Nat
x y : BitVec w
n i : Nat
a✝ : i < w
⊢ ((x ||| y).sshiftRight n).getLsbD i = (x.sshiftRight n ||| y.sshiftRight n).getLsbD i

Tactic:
simp only [getLsbD_sshiftRight, getLsbD_or, msb_or]

Result:
case pred
w : Nat
x y : BitVec w
n i : Nat
a✝ : i < w
⊢ (!decide (w ≤ i) && if n + i < w then x.getLsbD (n + i) || y.getLsbD (n + i) else x.msb || y.msb) =
    ((!decide (w ≤ i) && if n + i < w then x.getLsbD (n + i) else x.msb) ||
      !decide (w ≤ i) && if n + i < w then y.getLsbD (n + i) else y.msb)

Proof state:
w : Nat
x y : BitVec w
n : Nat
⊢ (x ||| y).sshiftRight n = x.sshiftRight n ||| y.sshiftRight n

Tactic:
ext i

Result:
case pred
w : Nat
x y : BitVec w
n i : Nat
a✝ : i < w
⊢ ((x ||| y).sshiftRight n).getLsbD i = (x.sshiftRight n ||| y.sshiftRight n).getLsbD i

Proof state:
case pred
w : Nat
x y : BitVec w
n i : Nat
a✝ : i < w
⊢ (!decide (w ≤ i) && if n + i < w then x.getLsbD (n + i) || y.getLsbD (n + i) else x.msb || y.msb) =
    ((!decide (w ≤ i) && if n + i < w then x.getLsbD (n + i) else x.msb) ||
      !decide (w ≤ i) && if n + i < w then y.getLsbD (n + i) else y.msb)

Tactic:
split
  <;> by_cases w ≤ i
  <;> simp [*]

Result:
no goals
-- Mathlib/NumberTheory/FLT/Three.lean
theorem fermatLastTheoremThree_of_three_dvd_only_c
    (H : ∀ a b c : ℤ, c ≠ 0 → ¬ 3 ∣ a → ¬ 3 ∣ b  → 3 ∣ c → IsCoprime a b → a ^ 3 + b ^ 3 ≠ c ^ 3) :
    FermatLastTheoremFor 3

Proof state:
case pos
H : ∀ (a b c : ℤ), c ≠ 0 → ¬3 ∣ a → ¬3 ∣ b → 3 ∣ c → IsCoprime a b → a ^ 3 + b ^ 3 ≠ c ^ 3
a b c : ℤ
ha : a ≠ 0
hb : b ≠ 0
hc : c ≠ 0
Hgcd : {a, b, c}.gcd id = 1
hF : a ^ 3 + b ^ 3 = c ^ 3
h1 : 3 ∣ a * b * c
⊢ False

case neg
H : ∀ (a b c : ℤ), c ≠ 0 → ¬3 ∣ a → ¬3 ∣ b → 3 ∣ c → IsCoprime a b → a ^ 3 + b ^ 3 ≠ c ^ 3
a b c : ℤ
ha : a ≠ 0
hb : b ≠ 0
hc : c ≠ 0
Hgcd : {a, b, c}.gcd id = 1
hF : a ^ 3 + b ^ 3 = c ^ 3
h1 : ¬3 ∣ a * b * c
⊢ False

Tactic:
swap

Result:
case neg
H : ∀ (a b c : ℤ), c ≠ 0 → ¬3 ∣ a → ¬3 ∣ b → 3 ∣ c → IsCoprime a b → a ^ 3 + b ^ 3 ≠ c ^ 3
a b c : ℤ
ha : a ≠ 0
hb : b ≠ 0
hc : c ≠ 0
Hgcd : {a, b, c}.gcd id = 1
hF : a ^ 3 + b ^ 3 = c ^ 3
h1 : ¬3 ∣ a * b * c
⊢ False

case pos
H : ∀ (a b c : ℤ), c ≠ 0 → ¬3 ∣ a → ¬3 ∣ b → 3 ∣ c → IsCoprime a b → a ^ 3 + b ^ 3 ≠ c ^ 3
a b c : ℤ
ha : a ≠ 0
hb : b ≠ 0
hc : c ≠ 0
Hgcd : {a, b, c}.gcd id = 1
hF : a ^ 3 + b ^ 3 = c ^ 3
h1 : 3 ∣ a * b * c
⊢ False

Proof state:
case pos.inl.inr
H : ∀ (a b c : ℤ), c ≠ 0 → ¬3 ∣ a → ¬3 ∣ b → 3 ∣ c → IsCoprime a b → a ^ 3 + b ^ 3 ≠ c ^ 3
a b c : ℤ
ha : a ≠ 0
hb : b ≠ 0
hc : c ≠ 0
Hgcd : {a, b, c}.gcd id = 1
hF : a ^ 3 + b ^ 3 + (-c) ^ 3 = 0
h3b : 3 ∣ b
⊢ False

Tactic:
rw [add_comm (a ^ 3)] at hF

Result:
case pos.inl.inr
H : ∀ (a b c : ℤ), c ≠ 0 → ¬3 ∣ a → ¬3 ∣ b → 3 ∣ c → IsCoprime a b → a ^ 3 + b ^ 3 ≠ c ^ 3
a b c : ℤ
ha : a ≠ 0
hb : b ≠ 0
hc : c ≠ 0
Hgcd : {a, b, c}.gcd id = 1
hF : b ^ 3 + a ^ 3 + (-c) ^ 3 = 0
h3b : 3 ∣ b
⊢ False

Proof state:
case pos.inl.inr
H : ∀ (a b c : ℤ), c ≠ 0 → ¬3 ∣ a → ¬3 ∣ b → 3 ∣ c → IsCoprime a b → a ^ 3 + b ^ 3 ≠ c ^ 3
a b c : ℤ
ha : a ≠ 0
hb : b ≠ 0
hc : c ≠ 0
Hgcd : {a, b, c}.gcd id = 1
hF : b ^ 3 + a ^ 3 + (-c) ^ 3 = 0
h3b : 3 ∣ b
⊢ False

Tactic:
refine fermatLastTheoremThree_of_dvd_a_of_gcd_eq_one_of_case2 hb h3b ?_ H hF

Result:
case pos.inl.inr
H : ∀ (a b c : ℤ), c ≠ 0 → ¬3 ∣ a → ¬3 ∣ b → 3 ∣ c → IsCoprime a b → a ^ 3 + b ^ 3 ≠ c ^ 3
a b c : ℤ
ha : a ≠ 0
hb : b ≠ 0
hc : c ≠ 0
Hgcd : {a, b, c}.gcd id = 1
hF : b ^ 3 + a ^ 3 + (-c) ^ 3 = 0
h3b : 3 ∣ b
⊢ {b, a, -c}.gcd id = 1

Proof state:
case pos
H : ∀ (a b c : ℤ), c ≠ 0 → ¬3 ∣ a → ¬3 ∣ b → 3 ∣ c → IsCoprime a b → a ^ 3 + b ^ 3 ≠ c ^ 3
a b c : ℤ
ha : a ≠ 0
hb : b ≠ 0
hc : c ≠ 0
Hgcd : {a, b, c}.gcd id = 1
hF : a ^ 3 + b ^ 3 = c ^ 3
h1 : 3 ∣ a * b * c
⊢ False

Tactic:
rw [(prime_three).dvd_mul, (prime_three).dvd_mul] at h1

Result:
case pos
H : ∀ (a b c : ℤ), c ≠ 0 → ¬3 ∣ a → ¬3 ∣ b → 3 ∣ c → IsCoprime a b → a ^ 3 + b ^ 3 ≠ c ^ 3
a b c : ℤ
ha : a ≠ 0
hb : b ≠ 0
hc : c ≠ 0
Hgcd : {a, b, c}.gcd id = 1
hF : a ^ 3 + b ^ 3 = c ^ 3
h1 : (3 ∣ a ∨ 3 ∣ b) ∨ 3 ∣ c
⊢ False
-- Mathlib/Algebra/Ring/Parity.lean
lemma neg_one_pow_eq_ite {R : Type*} [Monoid R] [HasDistribNeg R] {n : ℕ} :
    (-1 : R) ^ n = ite (Even n) 1 (-1)

Proof state:
case inr
R : Type u_4
inst✝¹ : Monoid R
inst✝ : HasDistribNeg R
n : ℕ
h : Odd n
⊢ (-1) ^ n = if Even n then 1 else -1

Tactic:
rw [h.neg_one_pow, if_neg (by simpa using h)]

Result:
no goals

Proof state:
R : Type u_4
inst✝¹ : Monoid R
inst✝ : HasDistribNeg R
n : ℕ
⊢ (-1) ^ n = if Even n then 1 else -1

Tactic:
cases even_or_odd n with
| inl h => rw [h.neg_one_pow, if_pos h]
| inr h => rw [h.neg_one_pow, if_neg (by simpa using h)]

Result:
no goals

Proof state:
case inl
R : Type u_4
inst✝¹ : Monoid R
inst✝ : HasDistribNeg R
n : ℕ
h : Even n
⊢ (-1) ^ n = if Even n then 1 else -1

Tactic:
rw [h.neg_one_pow, if_pos h]

Result:
no goals

Proof state:
R : Type u_4
inst✝¹ : Monoid R
inst✝ : HasDistribNeg R
n : ℕ
h : Odd n
⊢ ¬Even n

Tactic:
simpa using h

Result:
no goals
-- Mathlib/Analysis/SpecialFunctions/Gamma/Beta.lean
theorem GammaSeq_tendsto_Gamma (s : ℝ) : Tendsto (GammaSeq s) atTop (𝓝 <| Gamma s)

Proof state:
case h.e'_3
s : ℝ
⊢ Complex.ofReal ∘ s.GammaSeq = (↑s).GammaSeq

Tactic:
ext1 n

Result:
case h.e'_3.h
s : ℝ
n : ℕ
⊢ (Complex.ofReal ∘ s.GammaSeq) n = (↑s).GammaSeq n

Proof state:
case h.e'_3.h
s : ℝ
n : ℕ
⊢ ↑(↑n ^ s * ↑n ! / ∏ j ∈ Finset.range (n + 1), (s + ↑j)) = ↑n ^ ↑s * ↑n ! / ∏ j ∈ Finset.range (n + 1), (↑s + ↑j)

Tactic:
push_cast

Result:
case h.e'_3.h
s : ℝ
n : ℕ
⊢ ↑(↑n ^ s) * ↑n ! / ∏ x ∈ Finset.range (n + 1), (↑s + ↑x) = ↑n ^ ↑s * ↑n ! / ∏ x ∈ Finset.range (n + 1), (↑s + ↑x)

Proof state:
s : ℝ
this : Tendsto (Complex.ofReal ∘ s.GammaSeq) atTop (𝓝 (Complex.Gamma ↑s))
⊢ Tendsto s.GammaSeq atTop (𝓝 (Gamma s))

Tactic:
exact (Complex.continuous_re.tendsto (Complex.Gamma ↑s)).comp this

Result:
no goals

Proof state:
case h.e'_3.h
s : ℝ
n : ℕ
⊢ (Complex.ofReal ∘ s.GammaSeq) n = (↑s).GammaSeq n

Tactic:
dsimp only [GammaSeq, Function.comp_apply, Complex.GammaSeq]

Result:
case h.e'_3.h
s : ℝ
n : ℕ
⊢ ↑(↑n ^ s * ↑n ! / ∏ j ∈ Finset.range (n + 1), (s + ↑j)) = ↑n ^ ↑s * ↑n ! / ∏ j ∈ Finset.range (n + 1), (↑s + ↑j)

Proof state:
s : ℝ
⊢ Tendsto (Complex.ofReal ∘ s.GammaSeq) atTop (𝓝 (Complex.Gamma ↑s))

Tactic:
convert Complex.GammaSeq_tendsto_Gamma s

Result:
case h.e'_3
s : ℝ
⊢ Complex.ofReal ∘ s.GammaSeq = (↑s).GammaSeq

Proof state:
case h.e'_3.h
s : ℝ
n : ℕ
⊢ ↑(↑n ^ s) * ↑n ! / ∏ x ∈ Finset.range (n + 1), (↑s + ↑x) = ↑n ^ ↑s * ↑n ! / ∏ x ∈ Finset.range (n + 1), (↑s + ↑x)

Tactic:
rw [Complex.ofReal_cpow n.cast_nonneg, Complex.ofReal_natCast]

Result:
no goals

Proof state:
s : ℝ
⊢ Tendsto s.GammaSeq atTop (𝓝 (Gamma s))

Tactic:
suffices Tendsto ((↑) ∘ GammaSeq s : ℕ → ℂ) atTop (𝓝 <| Complex.Gamma s) by
  exact (Complex.continuous_re.tendsto (Complex.Gamma ↑s)).comp this

Result:
s : ℝ
⊢ Tendsto (Complex.ofReal ∘ s.GammaSeq) atTop (𝓝 (Complex.Gamma ↑s))
-- Mathlib/Topology/ContinuousMap/StoneWeierstrass.lean
lemma adjoin_id_eq_span_one_add (s : Set 𝕜) :
    ((StarAlgebra.adjoin 𝕜 {(restrict s (.id 𝕜) : C(s, 𝕜))}) : Set C(s, 𝕜)) =
      (span 𝕜 {(1 : C(s, 𝕜))} : Set C(s, 𝕜)) + (adjoin 𝕜 {(restrict s (.id 𝕜) : C(s, 𝕜))})

Proof state:
case h
𝕜 : Type u_1
inst✝ : RCLike 𝕜
s : Set 𝕜
x : C(↑s, 𝕜)
⊢ x ∈ ↑(StarAlgebra.adjoin 𝕜 {restrict s (ContinuousMap.id 𝕜)}) ↔
    x ∈ ↑(span 𝕜 {1}) + ↑(adjoin 𝕜 {restrict s (ContinuousMap.id 𝕜)})

Tactic:
rw [SetLike.mem_coe, ← StarAlgebra.adjoin_nonUnitalStarSubalgebra,
  ← StarSubalgebra.mem_toSubalgebra, ← Subalgebra.mem_toSubmodule,
  StarAlgebra.adjoin_nonUnitalStarSubalgebra_eq_span, mem_sup]

Result:
case h
𝕜 : Type u_1
inst✝ : RCLike 𝕜
s : Set 𝕜
x : C(↑s, 𝕜)
⊢ (∃ y ∈ span 𝕜 {1}, ∃ z ∈ (adjoin 𝕜 {restrict s (ContinuousMap.id 𝕜)}).toSubmodule, y + z = x) ↔
    x ∈ ↑(span 𝕜 {1}) + ↑(adjoin 𝕜 {restrict s (ContinuousMap.id 𝕜)})

Proof state:
𝕜 : Type u_1
inst✝ : RCLike 𝕜
s : Set 𝕜
⊢ ↑(StarAlgebra.adjoin 𝕜 {restrict s (ContinuousMap.id 𝕜)}) =
    ↑(span 𝕜 {1}) + ↑(adjoin 𝕜 {restrict s (ContinuousMap.id 𝕜)})

Tactic:
ext x

Result:
case h
𝕜 : Type u_1
inst✝ : RCLike 𝕜
s : Set 𝕜
x : C(↑s, 𝕜)
⊢ x ∈ ↑(StarAlgebra.adjoin 𝕜 {restrict s (ContinuousMap.id 𝕜)}) ↔
    x ∈ ↑(span 𝕜 {1}) + ↑(adjoin 𝕜 {restrict s (ContinuousMap.id 𝕜)})

Proof state:
case h
𝕜 : Type u_1
inst✝ : RCLike 𝕜
s : Set 𝕜
x : C(↑s, 𝕜)
⊢ (∃ y ∈ span 𝕜 {1}, ∃ z ∈ (adjoin 𝕜 {restrict s (ContinuousMap.id 𝕜)}).toSubmodule, y + z = x) ↔
    x ∈ ↑(span 𝕜 {1}) + ↑(adjoin 𝕜 {restrict s (ContinuousMap.id 𝕜)})

Tactic:
simp [Set.mem_add]

Result:
no goals
-- Mathlib/RingTheory/Smooth/StandardSmoothCotangent.lean
lemma cotangentComplexAux_surjective : Function.Surjective P.cotangentComplexAux

Proof state:
case h.h
R : Type u_1
S : Type u_2
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
P : SubmersivePresentation R S
i j : P.rels
⊢ P.cotangentComplexAux (Cotangent.mk ⟨P.relation i, ⋯⟩) j = P.basisDeriv i j

Tactic:
rw [P.cotangentComplexAux_apply]

Result:
case h.h
R : Type u_1
S : Type u_2
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
P : SubmersivePresentation R S
i j : P.rels
⊢ (aeval P.val) ((pderiv (P.map j)) ↑⟨P.relation i, ⋯⟩) = P.basisDeriv i j

Proof state:
R : Type u_1
S : Type u_2
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
P : SubmersivePresentation R S
⊢ Function.Surjective ⇑P.cotangentComplexAux

Tactic:
rw [← LinearMap.range_eq_top, _root_.eq_top_iff, ← P.basisDeriv.span_eq, Submodule.span_le]

Result:
R : Type u_1
S : Type u_2
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
P : SubmersivePresentation R S
⊢ Set.range ⇑P.basisDeriv ⊆ ↑(LinearMap.range P.cotangentComplexAux)

Proof state:
case h
R : Type u_1
S : Type u_2
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
P : SubmersivePresentation R S
i : P.rels
⊢ P.cotangentComplexAux (Cotangent.mk ⟨P.relation i, ⋯⟩) = P.basisDeriv i

Tactic:
ext j

Result:
case h.h
R : Type u_1
S : Type u_2
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
P : SubmersivePresentation R S
i j : P.rels
⊢ P.cotangentComplexAux (Cotangent.mk ⟨P.relation i, ⋯⟩) j = P.basisDeriv i j

Proof state:
case h.h
R : Type u_1
S : Type u_2
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
P : SubmersivePresentation R S
i j : P.rels
⊢ (aeval P.val) ((pderiv (P.map j)) ↑⟨P.relation i, ⋯⟩) = P.basisDeriv i j

Tactic:
simp

Result:
no goals

Proof state:
case intro
R : Type u_1
S : Type u_2
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
P : SubmersivePresentation R S
i : P.rels
⊢ P.basisDeriv i ∈ ↑(LinearMap.range P.cotangentComplexAux)

Tactic:
use Cotangent.mk ⟨P.relation i, P.relation_mem_ker i⟩

Result:
case h
R : Type u_1
S : Type u_2
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
P : SubmersivePresentation R S
i : P.rels
⊢ P.cotangentComplexAux (Cotangent.mk ⟨P.relation i, ⋯⟩) = P.basisDeriv i

Proof state:
R : Type u_1
S : Type u_2
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
P : SubmersivePresentation R S
⊢ Set.range ⇑P.basisDeriv ⊆ ↑(LinearMap.range P.cotangentComplexAux)

Tactic:
rintro - ⟨i, rfl⟩

Result:
case intro
R : Type u_1
S : Type u_2
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
P : SubmersivePresentation R S
i : P.rels
⊢ P.basisDeriv i ∈ ↑(LinearMap.range P.cotangentComplexAux)
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Nat/Power2.lean
theorem mul2_isPowerOfTwo_of_isPowerOfTwo (h : isPowerOfTwo n) : isPowerOfTwo (n * 2) :=
  have ⟨k, h⟩ := h
  ⟨k+1, by simp [h, Nat.pow_succ]⟩

Proof state:
n : Nat
h✝ : n.isPowerOfTwo
k : Nat
h : n = 2 ^ k
⊢ n * 2 = 2 ^ (k + 1)

Tactic:
simp [h, Nat.pow_succ]

Result:
no goals
-- Mathlib/Topology/UniformSpace/Basic.lean
theorem interior_mem_uniformity {s : Set (α × α)} (hs : s ∈ 𝓤 α) : interior s ∈ 𝓤 α

Proof state:
α : Type ua
inst✝ : UniformSpace α
s : Set (α × α)
hs : s ∈ 𝓤 α
⊢ interior s ∈ 𝓤 α

Tactic:
rw [uniformity_eq_uniformity_interior]

Result:
α : Type ua
inst✝ : UniformSpace α
s : Set (α × α)
hs : s ∈ 𝓤 α
⊢ interior s ∈ (𝓤 α).lift' interior

Proof state:
α : Type ua
inst✝ : UniformSpace α
s : Set (α × α)
hs : s ∈ 𝓤 α
⊢ interior s ∈ (𝓤 α).lift' interior

Tactic:
exact mem_lift' hs

Result:
no goals
-- Mathlib/Data/Set/Prod.lean
theorem prod_eq_prod_iff_of_nonempty (h : (s ×ˢ t).Nonempty) :
    s ×ˢ t = s₁ ×ˢ t₁ ↔ s = s₁ ∧ t = t₁

Proof state:
case mp
α : Type u_1
β : Type u_2
s s₁ : Set α
t t₁ : Set β
h : s.Nonempty ∧ t.Nonempty
heq : s ×ˢ t = s₁ ×ˢ t₁
h₁ : s₁.Nonempty ∧ t₁.Nonempty
⊢ s = s₁ ∧ t = t₁

Tactic:
rw [← fst_image_prod s h.2, ← fst_image_prod s₁ h₁.2, heq, eq_self_iff_true, true_and, ←
  snd_image_prod h.1 t, ← snd_image_prod h₁.1 t₁, heq]

Result:
no goals

Proof state:
α : Type u_1
β : Type u_2
s s₁ : Set α
t t₁ : Set β
h : (s ×ˢ t).Nonempty
⊢ s ×ˢ t = s₁ ×ˢ t₁ ↔ s = s₁ ∧ t = t₁

Tactic:
constructor

Result:
case mp
α : Type u_1
β : Type u_2
s s₁ : Set α
t t₁ : Set β
h : (s ×ˢ t).Nonempty
⊢ s ×ˢ t = s₁ ×ˢ t₁ → s = s₁ ∧ t = t₁

case mpr
α : Type u_1
β : Type u_2
s s₁ : Set α
t t₁ : Set β
h : (s ×ˢ t).Nonempty
⊢ s = s₁ ∧ t = t₁ → s ×ˢ t = s₁ ×ˢ t₁

Proof state:
case mpr.intro
α : Type u_1
β : Type u_2
s : Set α
t : Set β
h : (s ×ˢ t).Nonempty
⊢ s ×ˢ t = s ×ˢ t

Tactic:
rfl

Result:
no goals

Proof state:
case mp
α : Type u_1
β : Type u_2
s s₁ : Set α
t t₁ : Set β
h : (s ×ˢ t).Nonempty
heq : s ×ˢ t = s₁ ×ˢ t₁
⊢ s = s₁ ∧ t = t₁

Tactic:
have h₁ : (s₁ ×ˢ t₁ : Set _).Nonempty := by rwa [← heq]

Result:
case mp
α : Type u_1
β : Type u_2
s s₁ : Set α
t t₁ : Set β
h : (s ×ˢ t).Nonempty
heq : s ×ˢ t = s₁ ×ˢ t₁
h₁ : (s₁ ×ˢ t₁).Nonempty
⊢ s = s₁ ∧ t = t₁

Proof state:
case mp
α : Type u_1
β : Type u_2
s s₁ : Set α
t t₁ : Set β
h : (s ×ˢ t).Nonempty
⊢ s ×ˢ t = s₁ ×ˢ t₁ → s = s₁ ∧ t = t₁

Tactic:
intro heq

Result:
case mp
α : Type u_1
β : Type u_2
s s₁ : Set α
t t₁ : Set β
h : (s ×ˢ t).Nonempty
heq : s ×ˢ t = s₁ ×ˢ t₁
⊢ s = s₁ ∧ t = t₁

Proof state:
α : Type u_1
β : Type u_2
s s₁ : Set α
t t₁ : Set β
h : (s ×ˢ t).Nonempty
heq : s ×ˢ t = s₁ ×ˢ t₁
⊢ (s₁ ×ˢ t₁).Nonempty

Tactic:
rwa [← heq]

Result:
no goals

Proof state:
case mp
α : Type u_1
β : Type u_2
s s₁ : Set α
t t₁ : Set β
h : (s ×ˢ t).Nonempty
heq : s ×ˢ t = s₁ ×ˢ t₁
h₁ : (s₁ ×ˢ t₁).Nonempty
⊢ s = s₁ ∧ t = t₁

Tactic:
rw [prod_nonempty_iff] at h h₁

Result:
case mp
α : Type u_1
β : Type u_2
s s₁ : Set α
t t₁ : Set β
h : s.Nonempty ∧ t.Nonempty
heq : s ×ˢ t = s₁ ×ˢ t₁
h₁ : s₁.Nonempty ∧ t₁.Nonempty
⊢ s = s₁ ∧ t = t₁

Proof state:
case mpr
α : Type u_1
β : Type u_2
s s₁ : Set α
t t₁ : Set β
h : (s ×ˢ t).Nonempty
⊢ s = s₁ ∧ t = t₁ → s ×ˢ t = s₁ ×ˢ t₁

Tactic:
rintro ⟨rfl, rfl⟩

Result:
case mpr.intro
α : Type u_1
β : Type u_2
s : Set α
t : Set β
h : (s ×ˢ t).Nonempty
⊢ s ×ˢ t = s ×ˢ t
-- Mathlib/.lake/packages/lean4/src/lean/Std/Data/DHashMap/Internal/RawLemmas.lean
theorem getD_insert_self [EquivBEq α] [LawfulHashable α] (h : m.1.WF) {k : α} {fallback v : β} :
    getD (m.insert k v) k fallback = v

Proof state:
α : Type u
inst✝³ : BEq α
inst✝² : Hashable α
β : Type v
m : Raw₀ α fun x => β
inst✝¹ : EquivBEq α
inst✝ : LawfulHashable α
h : m.val.WF
k : α
fallback v : β
⊢ getD (m.insert k v) k fallback = v

Tactic:
simp_to_model [insert] using List.getValueD_insertEntry_self

Result:
no goals
-- Mathlib/MeasureTheory/MeasurableSpace/Invariants.lean
theorem measurable_invariants_dom {f : α → α} {g : α → β} :
    Measurable[invariants f] g ↔ Measurable g ∧ ∀ s, MeasurableSet s → (g ∘ f) ⁻¹' s = g ⁻¹' s

Proof state:
α : Type u_1
inst✝¹ : MeasurableSpace α
β : Type u_2
inst✝ : MeasurableSpace β
f : α → α
g : α → β
⊢ Measurable g ↔ Measurable g ∧ ∀ (s : Set β), MeasurableSet s → g ∘ f ⁻¹' s = g ⁻¹' s

Tactic:
simp only [Measurable, ← forall_and]

Result:
α : Type u_1
inst✝¹ : MeasurableSpace α
β : Type u_2
inst✝ : MeasurableSpace β
f : α → α
g : α → β
⊢ (∀ ⦃t : Set β⦄, MeasurableSet t → MeasurableSet (g ⁻¹' t)) ↔
    ∀ (x : Set β), MeasurableSet x → MeasurableSet (g ⁻¹' x) ∧ g ∘ f ⁻¹' x = g ⁻¹' x

Proof state:
α : Type u_1
inst✝¹ : MeasurableSpace α
β : Type u_2
inst✝ : MeasurableSpace β
f : α → α
g : α → β
⊢ (∀ ⦃t : Set β⦄, MeasurableSet t → MeasurableSet (g ⁻¹' t)) ↔
    ∀ (x : Set β), MeasurableSet x → MeasurableSet (g ⁻¹' x) ∧ g ∘ f ⁻¹' x = g ⁻¹' x

Tactic:
rfl

Result:
no goals