harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/Data/Nat/Bitwise.lean
theorem bitwise_comm {f : Bool → Bool → Bool} (hf : ∀ b b', f b b' = f b' b) (n m : ℕ) :
    bitwise f n m = bitwise f m n :=
  suffices bitwise f = swap (bitwise f) by conv_lhs => rw [this]
  calc
    bitwise f = bitwise (swap f) := congr_arg _ <| funext fun _ => funext <| hf _
    _ = swap (bitwise f) := bitwise_swap

Proof state:
f : Bool → Bool → Bool
hf : ∀ (b b' : Bool), f b b' = f b' b
n m : ℕ
this : bitwise f = swap (bitwise f)
⊢ bitwise f n m = bitwise f m n

Tactic:
conv_lhs => rw [this]

Result:
no goals
-- Mathlib/Algebra/Homology/ShortComplex/Exact.lean
/-- Given a morphism of short complexes `φ : S₁ ⟶ S₂` in an abelian category, if `S₁.f`
and `S₁.g` are zero (e.g. when `S₁` is of the form `0 ⟶ S₁.X₂ ⟶ 0`) and `S₂.f = 0`
(e.g when `S₂` is of the form `0 ⟶ S₂.X₂ ⟶ S₂.X₃`), then `φ` is a quasi-isomorphism iff
the obvious short complex `S₁.X₂ ⟶ S₂.X₂ ⟶ S₂.X₃` is exact and `φ.τ₂` is a mono). -/
lemma quasiIso_iff_of_zeros {S₁ S₂ : ShortComplex C} (φ : S₁ ⟶ S₂)
    (hf₁ : S₁.f = 0) (hg₁ : S₁.g = 0) (hf₂ : S₂.f = 0) :
    QuasiIso φ ↔
      (ShortComplex.mk φ.τ₂ S₂.g (by rw [φ.comm₂₃, hg₁, zero_comp])).Exact ∧ Mono φ.τ₂

Proof state:
case mp
C : Type u_1
inst✝¹ : Category.{u_3, u_1} C
inst✝ : Abelian C
S₁ S₂ : ShortComplex C
φ : S₁ ⟶ S₂
hf₁ : S₁.f = 0
hg₁ : S₁.g = 0
hf₂ : S₂.f = 0
w : φ.τ₂ ≫ S₂.g = 0
h : IsIso (S₂.liftCycles φ.τ₂ ⋯)
this : Mono φ.τ₂
⊢ (mk φ.τ₂ S₂.g ⋯).Exact ∧ Mono φ.τ₂

Tactic:
refine ⟨?_, this⟩

Result:
case mp
C : Type u_1
inst✝¹ : Category.{u_3, u_1} C
inst✝ : Abelian C
S₁ S₂ : ShortComplex C
φ : S₁ ⟶ S₂
hf₁ : S₁.f = 0
hg₁ : S₁.g = 0
hf₂ : S₂.f = 0
w : φ.τ₂ ≫ S₂.g = 0
h : IsIso (S₂.liftCycles φ.τ₂ ⋯)
this : Mono φ.τ₂
⊢ (mk φ.τ₂ S₂.g ⋯).Exact

Proof state:
C : Type u_1
inst✝¹ : Category.{u_3, u_1} C
inst✝ : Abelian C
S₁ S₂ : ShortComplex C
φ : S₁ ⟶ S₂
hf₁ : S₁.f = 0
hg₁ : S₁.g = 0
hf₂ : S₂.f = 0
w : φ.τ₂ ≫ S₂.g = 0
h : IsIso (S₂.liftCycles φ.τ₂ ⋯)
⊢ Mono φ.τ₂

Tactic:
rw [← S₂.liftCycles_i φ.τ₂ w]

Result:
C : Type u_1
inst✝¹ : Category.{u_3, u_1} C
inst✝ : Abelian C
S₁ S₂ : ShortComplex C
φ : S₁ ⟶ S₂
hf₁ : S₁.f = 0
hg₁ : S₁.g = 0
hf₂ : S₂.f = 0
w : φ.τ₂ ≫ S₂.g = 0
h : IsIso (S₂.liftCycles φ.τ₂ ⋯)
⊢ Mono (S₂.liftCycles φ.τ₂ w ≫ S₂.iCycles)

Proof state:
C : Type u_1
inst✝¹ : Category.{u_3, u_1} C
inst✝ : Abelian C
S₁ S₂ : ShortComplex C
φ : S₁ ⟶ S₂
hf₁ : S₁.f = 0
hg₁ : S₁.g = 0
hf₂ : S₂.f = 0
w : φ.τ₂ ≫ S₂.g = 0
h₁ : (mk φ.τ₂ S₂.g ⋯).Exact
h₂ : Mono φ.τ₂
⊢ S₂.iCycles ≫ (mk φ.τ₂ S₂.g ⋯).g = 0

Tactic:
simp

Result:
no goals
-- Mathlib/Topology/Instances/AddCircle.lean
theorem continuousAt_equivIoc (hx : x ≠ a) : ContinuousAt (equivIoc p a) x

Proof state:
case H
𝕜 : Type u_1
inst✝³ : LinearOrderedAddCommGroup 𝕜
p : 𝕜
hp : Fact (0 < p)
a : 𝕜
inst✝² : Archimedean 𝕜
inst✝¹ : TopologicalSpace 𝕜
inst✝ : OrderTopology 𝕜
x : AddCircle p
z✝ : 𝕜
hx : ↑z✝ ≠ ↑a
⊢ Filter.map (⇑(equivIoc p a) ∘ QuotientAddGroup.mk) (𝓝 z✝) ≤ 𝓝 ((equivIoc p a) ↑z✝)

Tactic:
exact (continuousAt_toIocMod hp.out a hx).codRestrict _

Result:
no goals

Proof state:
𝕜 : Type u_1
inst✝³ : LinearOrderedAddCommGroup 𝕜
p : 𝕜
hp : Fact (0 < p)
a : 𝕜
inst✝² : Archimedean 𝕜
inst✝¹ : TopologicalSpace 𝕜
inst✝ : OrderTopology 𝕜
x : AddCircle p
hx : x ≠ ↑a
⊢ ContinuousAt (⇑(equivIoc p a)) x

Tactic:
induction x using QuotientAddGroup.induction_on

Result:
case H
𝕜 : Type u_1
inst✝³ : LinearOrderedAddCommGroup 𝕜
p : 𝕜
hp : Fact (0 < p)
a : 𝕜
inst✝² : Archimedean 𝕜
inst✝¹ : TopologicalSpace 𝕜
inst✝ : OrderTopology 𝕜
x : AddCircle p
z✝ : 𝕜
hx : ↑z✝ ≠ ↑a
⊢ ContinuousAt ⇑(equivIoc p a) ↑z✝

Proof state:
case H
𝕜 : Type u_1
inst✝³ : LinearOrderedAddCommGroup 𝕜
p : 𝕜
hp : Fact (0 < p)
a : 𝕜
inst✝² : Archimedean 𝕜
inst✝¹ : TopologicalSpace 𝕜
inst✝ : OrderTopology 𝕜
x : AddCircle p
z✝ : 𝕜
hx : ↑z✝ ≠ ↑a
⊢ ContinuousAt ⇑(equivIoc p a) ↑z✝

Tactic:
rw [ContinuousAt, Filter.Tendsto, QuotientAddGroup.nhds_eq, Filter.map_map]

Result:
case H
𝕜 : Type u_1
inst✝³ : LinearOrderedAddCommGroup 𝕜
p : 𝕜
hp : Fact (0 < p)
a : 𝕜
inst✝² : Archimedean 𝕜
inst✝¹ : TopologicalSpace 𝕜
inst✝ : OrderTopology 𝕜
x : AddCircle p
z✝ : 𝕜
hx : ↑z✝ ≠ ↑a
⊢ Filter.map (⇑(equivIoc p a) ∘ QuotientAddGroup.mk) (𝓝 z✝) ≤ 𝓝 ((equivIoc p a) ↑z✝)
-- Mathlib/MeasureTheory/Measure/FiniteMeasure.lean
theorem tendsto_of_forall_integral_tendsto {γ : Type*} {F : Filter γ} {μs : γ → FiniteMeasure Ω}
    {μ : FiniteMeasure Ω}
    (h : ∀ f : Ω →ᵇ ℝ,
          Tendsto (fun i ↦ ∫ x, f x ∂(μs i : Measure Ω)) F (𝓝 (∫ x, f x ∂(μ : Measure Ω)))) :
    Tendsto μs F (𝓝 μ)

Proof state:
Ω : Type u_1
inst✝² : MeasurableSpace Ω
inst✝¹ : TopologicalSpace Ω
inst✝ : OpensMeasurableSpace Ω
γ : Type u_2
F : Filter γ
μs : γ → FiniteMeasure Ω
μ : FiniteMeasure Ω
h : ∀ (f : Ω →ᵇ ℝ), Tendsto (fun i => ∫ (x : Ω), f x ∂↑(μs i)) F (𝓝 (∫ (x : Ω), f x ∂↑μ))
f : Ω →ᵇ ℝ≥0
lip : LipschitzWith 1 NNReal.toReal
⊢ Tendsto (fun n => (∫⁻ (x : Ω), ↑(f x) ∂↑(μs n)).toReal) F (𝓝 (∫⁻ (x : Ω), ↑(f x) ∂↑μ).toReal)

Tactic:
set f₀ := BoundedContinuousFunction.comp _ lip f with _def_f₀

Result:
Ω : Type u_1
inst✝² : MeasurableSpace Ω
inst✝¹ : TopologicalSpace Ω
inst✝ : OpensMeasurableSpace Ω
γ : Type u_2
F : Filter γ
μs : γ → FiniteMeasure Ω
μ : FiniteMeasure Ω
h : ∀ (f : Ω →ᵇ ℝ), Tendsto (fun i => ∫ (x : Ω), f x ∂↑(μs i)) F (𝓝 (∫ (x : Ω), f x ∂↑μ))
f : Ω →ᵇ ℝ≥0
lip : LipschitzWith 1 NNReal.toReal
f₀ : Ω →ᵇ ℝ := comp NNReal.toReal lip f
_def_f₀ : f₀ = comp NNReal.toReal lip f
⊢ Tendsto (fun n => (∫⁻ (x : Ω), ↑(f x) ∂↑(μs n)).toReal) F (𝓝 (∫⁻ (x : Ω), ↑(f x) ∂↑μ).toReal)
-- Mathlib/Data/Set/Lattice.lean
theorem compl_iUnion₂ (s : ∀ i, κ i → Set α) : (⋃ (i) (j), s i j)ᶜ = ⋂ (i) (j), (s i j)ᶜ

Proof state:
α : Type u_1
ι : Sort u_5
κ : ι → Sort u_8
s : (i : ι) → κ i → Set α
⊢ (⋃ i, ⋃ j, s i j)ᶜ = ⋂ i, ⋂ j, (s i j)ᶜ

Tactic:
simp_rw [compl_iUnion]

Result:
no goals
-- Mathlib/Data/Nat/Digits.lean
theorem ofDigits_monotone {p q : ℕ} (L : List ℕ) (h : p ≤ q) : ofDigits p L ≤ ofDigits q L

Proof state:
case cons
p q : ℕ
h : p ≤ q
head✝ : ℕ
tail✝ : List ℕ
hi : ofDigits p tail✝ ≤ ofDigits q tail✝
⊢ p * ofDigits p tail✝ ≤ q * ofDigits q tail✝

Tactic:
exact Nat.mul_le_mul h hi

Result:
no goals

Proof state:
case cons
p q : ℕ
h : p ≤ q
head✝ : ℕ
tail✝ : List ℕ
hi : ofDigits p tail✝ ≤ ofDigits q tail✝
⊢ ofDigits p (head✝ :: tail✝) ≤ ofDigits q (head✝ :: tail✝)

Tactic:
simp only [ofDigits, cast_id, add_le_add_iff_left]

Result:
case cons
p q : ℕ
h : p ≤ q
head✝ : ℕ
tail✝ : List ℕ
hi : ofDigits p tail✝ ≤ ofDigits q tail✝
⊢ p * ofDigits p tail✝ ≤ q * ofDigits q tail✝

Proof state:
p q : ℕ
L : List ℕ
h : p ≤ q
⊢ ofDigits p L ≤ ofDigits q L

Tactic:
induction L with
| nil => rfl
| cons _ _ hi =>
  simp only [ofDigits, cast_id, add_le_add_iff_left]
  exact Nat.mul_le_mul h hi

Result:
no goals

Proof state:
case nil
p q : ℕ
h : p ≤ q
⊢ ofDigits p [] ≤ ofDigits q []

Tactic:
rfl

Result:
no goals
-- Mathlib/Data/Rat/Lemmas.lean
theorem mul_self_num (q : ℚ) : (q * q).num = q.num * q.num

Proof state:
q : ℚ
⊢ (q.num.natAbs * q.num.natAbs).Coprime (q.den * q.den)

Tactic:
exact (q.reduced.mul_right q.reduced).mul (q.reduced.mul_right q.reduced)

Result:
no goals

Proof state:
q : ℚ
⊢ (q * q).num = q.num * q.num

Tactic:
rw [mul_num, Int.natAbs_mul, Nat.Coprime.gcd_eq_one, Int.ofNat_one, Int.ediv_one]

Result:
q : ℚ
⊢ (q.num.natAbs * q.num.natAbs).Coprime (q.den * q.den)
-- Mathlib/MeasureTheory/MeasurableSpace/Basic.lean
lemma Measurable.exists [Countable ι] {p : ι → α → Prop} (hp : ∀ i, Measurable (p i)) :
    Measurable fun a ↦ ∃ i, p i a :=
  measurableSet_setOf.1 <| by rw [setOf_exists]; exact MeasurableSet.iUnion fun i ↦ (hp i).setOf

Proof state:
α : Type u_1
ι : Sort uι
inst✝¹ : MeasurableSpace α
inst✝ : Countable ι
p : ι → α → Prop
hp : ∀ (i : ι), Measurable (p i)
⊢ MeasurableSet (⋃ i, {x | p i x})

Tactic:
exact MeasurableSet.iUnion fun i ↦ (hp i).setOf

Result:
no goals

Proof state:
α : Type u_1
ι : Sort uι
inst✝¹ : MeasurableSpace α
inst✝ : Countable ι
p : ι → α → Prop
hp : ∀ (i : ι), Measurable (p i)
⊢ MeasurableSet {a | ∃ i, p i a}

Tactic:
rw [setOf_exists]

Result:
α : Type u_1
ι : Sort uι
inst✝¹ : MeasurableSpace α
inst✝ : Countable ι
p : ι → α → Prop
hp : ∀ (i : ι), Measurable (p i)
⊢ MeasurableSet (⋃ i, {x | p i x})
-- Mathlib/Topology/LocallyConstant/Basic.lean
theorem ofIsClopen_fiber_zero {X : Type*} [TopologicalSpace X] {U : Set X} [∀ x, Decidable (x ∈ U)]
    (hU : IsClopen U) : ofIsClopen hU ⁻¹' ({0} : Set (Fin 2)) = U

Proof state:
case h
X : Type u_5
inst✝¹ : TopologicalSpace X
U : Set X
inst✝ : (x : X) → Decidable (x ∈ U)
hU : IsClopen U
x✝ : X
⊢ x✝ ∈ ⇑(ofIsClopen hU) ⁻¹' {0} ↔ x✝ ∈ U

Tactic:
simp only [ofIsClopen, mem_singleton_iff, Fin.one_eq_zero_iff, coe_mk, mem_preimage,
  ite_eq_left_iff, Nat.succ_succ_ne_one]

Result:
case h
X : Type u_5
inst✝¹ : TopologicalSpace X
U : Set X
inst✝ : (x : X) → Decidable (x ∈ U)
hU : IsClopen U
x✝ : X
⊢ x✝ ∉ U → False ↔ x✝ ∈ U

Proof state:
X : Type u_5
inst✝¹ : TopologicalSpace X
U : Set X
inst✝ : (x : X) → Decidable (x ∈ U)
hU : IsClopen U
⊢ ⇑(ofIsClopen hU) ⁻¹' {0} = U

Tactic:
ext

Result:
case h
X : Type u_5
inst✝¹ : TopologicalSpace X
U : Set X
inst✝ : (x : X) → Decidable (x ∈ U)
hU : IsClopen U
x✝ : X
⊢ x✝ ∈ ⇑(ofIsClopen hU) ⁻¹' {0} ↔ x✝ ∈ U

Proof state:
case h
X : Type u_5
inst✝¹ : TopologicalSpace X
U : Set X
inst✝ : (x : X) → Decidable (x ∈ U)
hU : IsClopen U
x✝ : X
⊢ x✝ ∉ U → False ↔ x✝ ∈ U

Tactic:
tauto

Result:
no goals
-- Mathlib/.lake/packages/batteries/Batteries/Data/RBMap/WF.lean
theorem reverse_balLeft (l : RBNode α) (v : α) (r : RBNode α) :
    (balLeft l v r).reverse = balRight r.reverse v l.reverse

Proof state:
case h_2.h_3.x
α : Type u_1
l : RBNode α
v : α
r l✝ : RBNode α
x✝³ : ∀ (a : RBNode α) (x : α) (b : RBNode α), l = node red a x b → False
r✝ : RBNode α
x✝² : ∀ (a : RBNode α) (y : α) (b : RBNode α), r = node black a y b → False
x✝¹ : ∀ (a : RBNode α) (y : α) (b : RBNode α) (z : α) (c : RBNode α), r = node red (node black a y b) z c → False
a✝ : RBNode α
x✝ : α
b✝ : RBNode α
y✝ : α
c✝ : RBNode α
⊢ ¬r = node red (node black c✝.reverse y✝ b✝.reverse) x✝ a✝.reverse

Tactic:
solve_by_elim

Result:
no goals

Proof state:
α : Type u_1
l : RBNode α
v : α
r : RBNode α
⊢ (l.balLeft v r).reverse = r.reverse.balRight v l.reverse

Tactic:
unfold balLeft balRight

Result:
α : Type u_1
l : RBNode α
v : α
r : RBNode α
⊢ (match l with
      | node red a x b => node red (node black a x b) v r
      | l =>
        match r with
        | node black a y b => l.balance2 v (node red a y b)
        | node red (node black a y b) z c => node red (node black l v a) y (b.balance2 z c.setRed)
        | r => node red l v r).reverse =
    match l.reverse with
    | node red b y c => node red r.reverse v (node black b y c)
    | r_1 =>
      match r.reverse with
      | node black a x b => (node red a x b).balance1 v r_1
      | node red a x (node black b y c) => node red (a.setRed.balance1 x b) y (node black c v r_1)
      | l => node red l v r_1

Proof state:
case h_2.h_3.x
α : Type u_1
l : RBNode α
v : α
r l✝ : RBNode α
x✝² : ∀ (a : RBNode α) (x : α) (b : RBNode α), l = node red a x b → False
r✝ : RBNode α
x✝¹ : ∀ (a : RBNode α) (y : α) (b : RBNode α), r = node black a y b → False
x✝ : ∀ (a : RBNode α) (y : α) (b : RBNode α) (z : α) (c : RBNode α), r = node red (node black a y b) z c → False
⊢ ∀ (a : RBNode α) (x : α) (b : RBNode α) (y : α) (c : RBNode α),
    ¬r = node red (node black c.reverse y b.reverse) x a.reverse

Tactic:
intros

Result:
case h_2.h_3.x
α : Type u_1
l : RBNode α
v : α
r l✝ : RBNode α
x✝³ : ∀ (a : RBNode α) (x : α) (b : RBNode α), l = node red a x b → False
r✝ : RBNode α
x✝² : ∀ (a : RBNode α) (y : α) (b : RBNode α), r = node black a y b → False
x✝¹ : ∀ (a : RBNode α) (y : α) (b : RBNode α) (z : α) (c : RBNode α), r = node red (node black a y b) z c → False
a✝ : RBNode α
x✝ : α
b✝ : RBNode α
y✝ : α
c✝ : RBNode α
⊢ ¬r = node red (node black c✝.reverse y✝ b✝.reverse) x✝ a✝.reverse

Proof state:
α : Type u_1
l : RBNode α
v : α
r l✝ : RBNode α
x✝ : ∀ (a : RBNode α) (x : α) (b : RBNode α), l = node red a x b → False
⊢ ∀ (a : RBNode α) (x : α) (b : RBNode α), ¬l = node red b.reverse x a.reverse

Tactic:
intros

Result:
α : Type u_1
l : RBNode α
v : α
r l✝ : RBNode α
x✝¹ : ∀ (a : RBNode α) (x : α) (b : RBNode α), l = node red a x b → False
a✝ : RBNode α
x✝ : α
b✝ : RBNode α
⊢ ¬l = node red b✝.reverse x✝ a✝.reverse
-- Mathlib/Data/Multiset/Fintype.lean
theorem prod_eq_prod_toEnumFinset [CommMonoid α] (m : Multiset α) :
    m.prod = ∏ x ∈ m.toEnumFinset, x.1

Proof state:
case e_a
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : CommMonoid α
m : Multiset α
⊢ m = map (fun x => x.1) m.toEnumFinset.val

Tactic:
simp

Result:
no goals

Proof state:
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : CommMonoid α
m : Multiset α
⊢ m.prod = ∏ x ∈ m.toEnumFinset, x.1

Tactic:
congr

Result:
case e_a
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : CommMonoid α
m : Multiset α
⊢ m = map (fun x => x.1) m.toEnumFinset.val
-- Mathlib/Analysis/SpecialFunctions/Pow/Asymptotics.lean
theorem tendsto_rpow_neg_div : Tendsto (fun x => x ^ (-(1 : ℝ) / x)) atTop (𝓝 1)

Proof state:
⊢ Tendsto (fun x => x ^ (-1 / x)) atTop (𝓝 1)

Tactic:
convert tendsto_rpow_div_mul_add (-(1 : ℝ)) _ (0 : ℝ) zero_ne_one

Result:
case h.e'_3.h.h.e'_6.h.e'_6
x✝ : ℝ
⊢ x✝ = 1 * x✝ + 0

Proof state:
case h.e'_3.h.h.e'_6.h.e'_6
x✝ : ℝ
⊢ x✝ = 1 * x✝ + 0

Tactic:
ring

Result:
no goals
-- Mathlib/SetTheory/Ordinal/Arithmetic.lean
theorem has_succ_of_type_succ_lt {α} {r : α → α → Prop} [wo : IsWellOrder α r]
    (h : ∀ a < type r, succ a < type r) (x : α) : ∃ y, r x y

Proof state:
case h.e'_1
α : Type u_4
r : α → α → Prop
wo : IsWellOrder α r
h : ∀ a < type r, succ a < type r
x : α
⊢ x = (enum r) ?h.convert_4

Tactic:
rw [enum_typein]

Result:
no goals

Proof state:
case h
α : Type u_4
r : α → α → Prop
wo : IsWellOrder α r
h : ∀ a < type r, succ a < type r
x : α
⊢ r x ((enum r) ⟨succ ((typein r).toRelEmbedding x), ⋯⟩)

Tactic:
convert enum_lt_enum.mpr _

Result:
case h.e'_1
α : Type u_4
r : α → α → Prop
wo : IsWellOrder α r
h : ∀ a < type r, succ a < type r
x : α
⊢ x = (enum r) ?h.convert_4

case h.convert_4
α : Type u_4
r : α → α → Prop
wo : IsWellOrder α r
h : ∀ a < type r, succ a < type r
x : α
⊢ ↑(Iio (type r))

case h.convert_6
α : Type u_4
r : α → α → Prop
wo : IsWellOrder α r
h : ∀ a < type r, succ a < type r
x : α
⊢ ?h.convert_4 < ⟨succ ((typein r).toRelEmbedding x), ⋯⟩

Proof state:
α : Type u_4
r : α → α → Prop
wo : IsWellOrder α r
h : ∀ a < type r, succ a < type r
x : α
⊢ ∃ y, r x y

Tactic:
use enum r ⟨succ (typein r x), h _ (typein_lt_type r x)⟩

Result:
case h
α : Type u_4
r : α → α → Prop
wo : IsWellOrder α r
h : ∀ a < type r, succ a < type r
x : α
⊢ r x ((enum r) ⟨succ ((typein r).toRelEmbedding x), ⋯⟩)

Proof state:
case h.convert_6
α : Type u_4
r : α → α → Prop
wo : IsWellOrder α r
h : ∀ a < type r, succ a < type r
x : α
⊢ ⟨(typein r).toRelEmbedding x, ⋯⟩ < ⟨succ ((typein r).toRelEmbedding x), ⋯⟩

Tactic:
rw [Subtype.mk_lt_mk, lt_succ_iff]

Result:
no goals
-- Mathlib/LinearAlgebra/Projectivization/Cardinality.lean
lemma card_of_finrank [Finite k] {n : ℕ} (h : Module.finrank k V = n) :
    Nat.card (ℙ k V) = ∑ i ∈ Finset.range n, Nat.card k ^ i

Proof state:
k : Type u_1
V : Type u_2
inst✝³ : Field k
inst✝² : AddCommGroup V
inst✝¹ : Module k V
inst✝ : Finite k
n : ℕ
h : Module.finrank k V = n
this :
  ∀ (k : Type u_1) (V : Type u_2) [inst : Field k] [inst_1 : AddCommGroup V] [inst_2 : Module k V] [inst_3 : Finite k]
    {n : ℕ}, Module.finrank k V = n → Finite V → Nat.card (ℙ k V) = ∑ i ∈ Finset.range n, Nat.card k ^ i
hf : Infinite V
⊢ ¬Finite V

Tactic:
simpa

Result:
no goals

Proof state:
case inr
k : Type u_1
V : Type u_2
inst✝³ : Field k
inst✝² : AddCommGroup V
inst✝¹ : Module k V
inst✝ : Finite k
n : ℕ
h : Module.finrank k V = n
this✝¹ :
  ∀ (k : Type u_1) (V : Type u_2) [inst : Field k] [inst_1 : AddCommGroup V] [inst_2 : Module k V] [inst_3 : Finite k]
    {n : ℕ}, Module.finrank k V = n → Finite V → Nat.card (ℙ k V) = ∑ i ∈ Finset.range n, Nat.card k ^ i
hf : Infinite V
this✝ : Infinite (ℙ k V)
this : n = 0
⊢ Nat.card (ℙ k V) = ∑ i ∈ Finset.range n, Nat.card k ^ i

Tactic:
simp [this]

Result:
no goals

Proof state:
k✝ : Type u_1
V✝ : Type u_2
inst✝⁶ : Field k✝
inst✝⁵ : AddCommGroup V✝
inst✝⁴ : Module k✝ V✝
k : Type u_1
V : Type u_2
inst✝³ : Field k
inst✝² : AddCommGroup V
inst✝¹ : Module k V
inst✝ : Finite k
n : ℕ
h : Module.finrank k V = n
hf : Finite V
this : 1 < Nat.card k
e : V ≃ₗ[k] Fin n → k := LinearEquiv.ofFinrankEq V (Fin n → k) ⋯
⊢ Nat.card V = Nat.card k ^ n

Tactic:
simp [Nat.card_congr e.toEquiv, Nat.card_fun]

Result:
no goals

Proof state:
case inr
k : Type u_1
V : Type u_2
inst✝³ : Field k
inst✝² : AddCommGroup V
inst✝¹ : Module k V
inst✝ : Finite k
n : ℕ
h : Module.finrank k V = n
this :
  ∀ (k : Type u_1) (V : Type u_2) [inst : Field k] [inst_1 : AddCommGroup V] [inst_2 : Module k V] [inst_3 : Finite k]
    {n : ℕ}, Module.finrank k V = n → Finite V → Nat.card (ℙ k V) = ∑ i ∈ Finset.range n, Nat.card k ^ i
hf : Infinite V
⊢ Nat.card (ℙ k V) = ∑ i ∈ Finset.range n, Nat.card k ^ i

Tactic:
have : Infinite (ℙ k V) := by
  rw [← not_finite_iff_infinite, not_iff_not.mpr (finite_iff_of_finite k V)]
  simpa

Result:
case inr
k : Type u_1
V : Type u_2
inst✝³ : Field k
inst✝² : AddCommGroup V
inst✝¹ : Module k V
inst✝ : Finite k
n : ℕ
h : Module.finrank k V = n
this✝ :
  ∀ (k : Type u_1) (V : Type u_2) [inst : Field k] [inst_1 : AddCommGroup V] [inst_2 : Module k V] [inst_3 : Finite k]
    {n : ℕ}, Module.finrank k V = n → Finite V → Nat.card (ℙ k V) = ∑ i ∈ Finset.range n, Nat.card k ^ i
hf : Infinite V
this : Infinite (ℙ k V)
⊢ Nat.card (ℙ k V) = ∑ i ∈ Finset.range n, Nat.card k ^ i
-- Mathlib/Data/Nat/Bitwise.lean
theorem lt_xor_cases {a b c : ℕ} (h : a < b ^^^ c) : a ^^^ c < b ∨ a ^^^ b < c

Proof state:
a b c : ℕ
h : a < b ^^^ c
⊢ a ^^^ c < b ∨ a ^^^ b < c

Tactic:
obtain ha | hb | hc := xor_trichotomy <| Nat.xor_assoc _ _ _ ▸ xor_ne_zero.2 h.ne

Result:
case inl
a b c : ℕ
h : a < b ^^^ c
ha : b ^^^ c < a
⊢ a ^^^ c < b ∨ a ^^^ b < c

case inr.inl
a b c : ℕ
h : a < b ^^^ c
hb : c ^^^ a < b
⊢ a ^^^ c < b ∨ a ^^^ b < c

case inr.inr
a b c : ℕ
h : a < b ^^^ c
hc : a ^^^ b < c
⊢ a ^^^ c < b ∨ a ^^^ b < c

Proof state:
case inl
a b c : ℕ
h : a < b ^^^ c
ha : b ^^^ c < a
⊢ a ^^^ c < b ∨ a ^^^ b < c

case inr.inl
a b c : ℕ
h : a < b ^^^ c
hb : c ^^^ a < b
⊢ a ^^^ c < b ∨ a ^^^ b < c

case inr.inr
a b c : ℕ
h : a < b ^^^ c
hc : a ^^^ b < c
⊢ a ^^^ c < b ∨ a ^^^ b < c

Tactic:
exacts [(h.asymm ha).elim, Or.inl <| Nat.xor_comm _ _ ▸ hb, Or.inr hc]

Result:
no goals
-- Mathlib/NumberTheory/Padics/PadicNumbers.lean
theorem rat_dense (q : ℚ_[p]) {ε : ℝ} (hε : 0 < ε) : ∃ r : ℚ, ‖q - r‖ < ε :=
  let ⟨ε', hε'l, hε'r⟩ := exists_rat_btwn hε
  let ⟨r, hr⟩ := rat_dense' q (ε := ε') (by simpa using hε'l)
  ⟨r, lt_trans (by simpa [Norm.norm] using hr) hε'r⟩

Proof state:
p : ℕ
inst✝ : Fact (Nat.Prime p)
q : ℚ_[p]
ε : ℝ
hε : 0 < ε
ε' : ℚ
hε'l : 0 < ↑ε'
hε'r : ↑ε' < ε
⊢ 0 < ε'

Tactic:
simpa using hε'l

Result:
no goals

Proof state:
p : ℕ
inst✝ : Fact (Nat.Prime p)
q : ℚ_[p]
ε : ℝ
hε : 0 < ε
ε' : ℚ
hε'l : 0 < ↑ε'
hε'r : ↑ε' < ε
r : ℚ
hr : padicNormE (q - ↑r) < ε'
⊢ ‖q - ↑r‖ < ↑ε'

Tactic:
simpa [Norm.norm] using hr

Result:
no goals
-- Mathlib/Analysis/Convex/Exposed.lean
theorem mem_exposedPoints_iff_exposed_singleton : x ∈ A.exposedPoints 𝕜 ↔ IsExposed 𝕜 A {x}

Proof state:
case mpr
𝕜 : Type u_1
E : Type u_2
inst✝⁴ : TopologicalSpace 𝕜
inst✝³ : OrderedRing 𝕜
inst✝² : AddCommMonoid E
inst✝¹ : TopologicalSpace E
inst✝ : Module 𝕜 E
A : Set E
x : E
h : IsExposed 𝕜 A {x}
⊢ x ∈ exposedPoints 𝕜 A

Tactic:
obtain ⟨l, hl⟩ := h ⟨x, mem_singleton _⟩

Result:
case mpr.intro
𝕜 : Type u_1
E : Type u_2
inst✝⁴ : TopologicalSpace 𝕜
inst✝³ : OrderedRing 𝕜
inst✝² : AddCommMonoid E
inst✝¹ : TopologicalSpace E
inst✝ : Module 𝕜 E
A : Set E
x : E
h : IsExposed 𝕜 A {x}
l : E →L[𝕜] 𝕜
hl : {x} = {x | x ∈ A ∧ ∀ y ∈ A, l y ≤ l x}
⊢ x ∈ exposedPoints 𝕜 A

Proof state:
case mpr.intro
𝕜 : Type u_1
E : Type u_2
inst✝⁴ : TopologicalSpace 𝕜
inst✝³ : OrderedRing 𝕜
inst✝² : AddCommMonoid E
inst✝¹ : TopologicalSpace E
inst✝ : Module 𝕜 E
A : Set E
x : E
h : IsExposed 𝕜 A {x}
l : E →L[𝕜] 𝕜
hl : x ∈ {x | x ∈ A ∧ ∀ y ∈ A, l y ≤ l x} ∧ ∀ x_1 ∈ {x | x ∈ A ∧ ∀ y ∈ A, l y ≤ l x}, x_1 = x
⊢ x ∈ exposedPoints 𝕜 A

Tactic:
exact
  ⟨hl.1.1, l, fun y hy =>
    ⟨hl.1.2 y hy, fun hxy => hl.2 y ⟨hy, fun z hz => (hl.1.2 z hz).trans hxy⟩⟩⟩

Result:
no goals

Proof state:
case mpr.intro
𝕜 : Type u_1
E : Type u_2
inst✝⁴ : TopologicalSpace 𝕜
inst✝³ : OrderedRing 𝕜
inst✝² : AddCommMonoid E
inst✝¹ : TopologicalSpace E
inst✝ : Module 𝕜 E
A : Set E
x : E
h : IsExposed 𝕜 A {x}
l : E →L[𝕜] 𝕜
hl : {x} = {x | x ∈ A ∧ ∀ y ∈ A, l y ≤ l x}
⊢ x ∈ exposedPoints 𝕜 A

Tactic:
rw [eq_comm, eq_singleton_iff_unique_mem] at hl

Result:
case mpr.intro
𝕜 : Type u_1
E : Type u_2
inst✝⁴ : TopologicalSpace 𝕜
inst✝³ : OrderedRing 𝕜
inst✝² : AddCommMonoid E
inst✝¹ : TopologicalSpace E
inst✝ : Module 𝕜 E
A : Set E
x : E
h : IsExposed 𝕜 A {x}
l : E →L[𝕜] 𝕜
hl : x ∈ {x | x ∈ A ∧ ∀ y ∈ A, l y ≤ l x} ∧ ∀ x_1 ∈ {x | x ∈ A ∧ ∀ y ∈ A, l y ≤ l x}, x_1 = x
⊢ x ∈ exposedPoints 𝕜 A

Proof state:
𝕜 : Type u_1
E : Type u_2
inst✝⁴ : TopologicalSpace 𝕜
inst✝³ : OrderedRing 𝕜
inst✝² : AddCommMonoid E
inst✝¹ : TopologicalSpace E
inst✝ : Module 𝕜 E
A : Set E
x : E
⊢ x ∈ exposedPoints 𝕜 A ↔ IsExposed 𝕜 A {x}

Tactic:
use fun ⟨hxA, l, hl⟩ _ =>
  ⟨l,
    Eq.symm <|
      eq_singleton_iff_unique_mem.2
        ⟨⟨hxA, fun y hy => (hl y hy).1⟩, fun z hz => (hl z hz.1).2 (hz.2 x hxA)⟩⟩

Result:
case mpr
𝕜 : Type u_1
E : Type u_2
inst✝⁴ : TopologicalSpace 𝕜
inst✝³ : OrderedRing 𝕜
inst✝² : AddCommMonoid E
inst✝¹ : TopologicalSpace E
inst✝ : Module 𝕜 E
A : Set E
x : E
⊢ IsExposed 𝕜 A {x} → x ∈ exposedPoints 𝕜 A

Proof state:
case mpr
𝕜 : Type u_1
E : Type u_2
inst✝⁴ : TopologicalSpace 𝕜
inst✝³ : OrderedRing 𝕜
inst✝² : AddCommMonoid E
inst✝¹ : TopologicalSpace E
inst✝ : Module 𝕜 E
A : Set E
x : E
⊢ IsExposed 𝕜 A {x} → x ∈ exposedPoints 𝕜 A

Tactic:
rintro h

Result:
case mpr
𝕜 : Type u_1
E : Type u_2
inst✝⁴ : TopologicalSpace 𝕜
inst✝³ : OrderedRing 𝕜
inst✝² : AddCommMonoid E
inst✝¹ : TopologicalSpace E
inst✝ : Module 𝕜 E
A : Set E
x : E
h : IsExposed 𝕜 A {x}
⊢ x ∈ exposedPoints 𝕜 A
-- Mathlib/Topology/Constructions.lean
theorem mem_nhds_prod_iff' {x : X} {y : Y} {s : Set (X × Y)} :
    s ∈ 𝓝 (x, y) ↔ ∃ u v, IsOpen u ∧ x ∈ u ∧ IsOpen v ∧ y ∈ v ∧ u ×ˢ v ⊆ s :=
  ((nhds_basis_opens x).prod_nhds (nhds_basis_opens y)).mem_iff.trans <| by
    simp only [Prod.exists, and_comm, and_assoc, and_left_comm]

Proof state:
X : Type u
Y : Type v
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
x : X
y : Y
s : Set (X × Y)
⊢ (∃ i, ((x ∈ i.1 ∧ IsOpen i.1) ∧ y ∈ i.2 ∧ IsOpen i.2) ∧ i.1 ×ˢ i.2 ⊆ s) ↔
    ∃ u v, IsOpen u ∧ x ∈ u ∧ IsOpen v ∧ y ∈ v ∧ u ×ˢ v ⊆ s

Tactic:
simp only [Prod.exists, and_comm, and_assoc, and_left_comm]

Result:
no goals
-- Mathlib/MeasureTheory/Integral/BochnerL1.lean
theorem norm_integral_le_integral_norm (f : α →ₛ E) (hf : Integrable f μ) :
    ‖f.integral μ‖ ≤ (f.map norm).integral μ

Proof state:
α : Type u_1
E : Type u_2
inst✝¹ : NormedAddCommGroup E
m : MeasurableSpace α
μ : Measure α
inst✝ : NormedSpace ℝ E
f : α →ₛ E
hf : Integrable (⇑f) μ
s : Set α
x✝¹ : MeasurableSet s
x✝ : μ s < ⊤
⊢ ‖weightedSMul μ s‖ ≤ 1 * (μ s).toReal

Tactic:
exact (norm_weightedSMul_le s).trans (one_mul _).symm.le

Result:
no goals

Proof state:
α : Type u_1
E : Type u_2
inst✝¹ : NormedAddCommGroup E
m : MeasurableSpace α
μ : Measure α
inst✝ : NormedSpace ℝ E
f : α →ₛ E
hf : Integrable (⇑f) μ
⊢ ‖integral μ f‖ ≤ integral μ (map norm f)

Tactic:
refine (norm_setToSimpleFunc_le_integral_norm _ (fun s _ _ => ?_) hf).trans (one_mul _).le

Result:
α : Type u_1
E : Type u_2
inst✝¹ : NormedAddCommGroup E
m : MeasurableSpace α
μ : Measure α
inst✝ : NormedSpace ℝ E
f : α →ₛ E
hf : Integrable (⇑f) μ
s : Set α
x✝¹ : MeasurableSet s
x✝ : μ s < ⊤
⊢ ‖weightedSMul μ s‖ ≤ 1 * (μ s).toReal
-- Mathlib/MeasureTheory/Integral/IntervalIntegral.lean
theorem inv_smul_integral_comp_div (c) :
    (c⁻¹ • ∫ x in a..b, f (x / c)) = ∫ x in a / c..b / c, f x

Proof state:
E : Type u_3
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
a b : ℝ
f : ℝ → E
c : ℝ
⊢ c⁻¹ • ∫ (x : ℝ) in a..b, f (x / c) = ∫ (x : ℝ) in a / c..b / c, f x

Tactic:
by_cases hc : c = 0 <;> simp [hc, integral_comp_div]

Result:
no goals