harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/AlgebraicGeometry/EllipticCurve/NormalForms.lean
theorem toCharTwoJEqZeroNF_spec (ha₁ : W.a₁ = 0) :
    (W.variableChange W.toCharTwoJEqZeroNF).IsCharTwoJEqZeroNF

Proof state:
R : Type u_1
inst✝¹ : CommRing R
W : WeierstrassCurve R
inst✝ : CharP R 2
ha₁ : W.a₁ = 0
⊢ (W.variableChange W.toCharTwoJEqZeroNF).IsCharTwoJEqZeroNF

Tactic:
constructor

Result:
case a₁
R : Type u_1
inst✝¹ : CommRing R
W : WeierstrassCurve R
inst✝ : CharP R 2
ha₁ : W.a₁ = 0
⊢ (W.variableChange W.toCharTwoJEqZeroNF).a₁ = 0

case a₂
R : Type u_1
inst✝¹ : CommRing R
W : WeierstrassCurve R
inst✝ : CharP R 2
ha₁ : W.a₁ = 0
⊢ (W.variableChange W.toCharTwoJEqZeroNF).a₂ = 0

Proof state:
case a₂
R : Type u_1
inst✝¹ : CommRing R
W : WeierstrassCurve R
inst✝ : CharP R 2
ha₁ : W.a₁ = 0
⊢ (W.variableChange W.toCharTwoJEqZeroNF).a₂ = 0

Tactic:
simp_rw [toCharTwoJEqZeroNF, variableChange_a₂, inv_one, Units.val_one]

Result:
case a₂
R : Type u_1
inst✝¹ : CommRing R
W : WeierstrassCurve R
inst✝ : CharP R 2
ha₁ : W.a₁ = 0
⊢ 1 ^ 2 * (W.a₂ - 0 * W.a₁ + 3 * W.a₂ - 0 ^ 2) = 0

Proof state:
case a₁
R : Type u_1
inst✝¹ : CommRing R
W : WeierstrassCurve R
inst✝ : CharP R 2
ha₁ : W.a₁ = 0
⊢ (W.variableChange W.toCharTwoJEqZeroNF).a₁ = 0

Tactic:
simp [toCharTwoJEqZeroNF, ha₁]

Result:
no goals

Proof state:
case a₂
R : Type u_1
inst✝¹ : CommRing R
W : WeierstrassCurve R
inst✝ : CharP R 2
ha₁ : W.a₁ = 0
⊢ 1 ^ 2 * (W.a₂ - 0 * W.a₁ + 3 * W.a₂ - 0 ^ 2) = 0

Tactic:
linear_combination 2 * W.a₂ * CharP.cast_eq_zero R 2

Result:
no goals
-- Mathlib/Topology/Homotopy/Product.lean
theorem proj_pi (i : ι) (paths : ∀ i, Path.Homotopic.Quotient (as i) (bs i)) :
    proj i (pi paths) = paths i

Proof state:
ι : Type u_1
X : ι → Type u_2
inst✝ : (i : ι) → TopologicalSpace (X i)
as bs : (i : ι) → X i
i : ι
paths : (i : ι) → Homotopic.Quotient (as i) (bs i)
⊢ proj i (pi paths) = paths i

Tactic:
induction paths using Quotient.induction_on_pi

Result:
case h
ι : Type u_1
X : ι → Type u_2
inst✝ : (i : ι) → TopologicalSpace (X i)
as bs : (i : ι) → X i
i : ι
a✝ : (i : ι) → Path (as i) (bs i)
⊢ proj i (pi fun i => ⟦a✝ i⟧) = (fun i => ⟦a✝ i⟧) i

Proof state:
case h
ι : Type u_1
X : ι → Type u_2
inst✝ : (i : ι) → TopologicalSpace (X i)
as bs : (i : ι) → X i
i : ι
a✝ : (i : ι) → Path (as i) (bs i)
⊢ ⟦(Path.pi a✝).map ⋯⟧ = (fun i => ⟦a✝ i⟧) i

Tactic:
congr

Result:
no goals

Proof state:
case h
ι : Type u_1
X : ι → Type u_2
inst✝ : (i : ι) → TopologicalSpace (X i)
as bs : (i : ι) → X i
i : ι
a✝ : (i : ι) → Path (as i) (bs i)
⊢ proj i (pi fun i => ⟦a✝ i⟧) = (fun i => ⟦a✝ i⟧) i

Tactic:
rw [proj, pi_lift, ← Path.Homotopic.map_lift]

Result:
case h
ι : Type u_1
X : ι → Type u_2
inst✝ : (i : ι) → TopologicalSpace (X i)
as bs : (i : ι) → X i
i : ι
a✝ : (i : ι) → Path (as i) (bs i)
⊢ ⟦(Path.pi a✝).map ⋯⟧ = (fun i => ⟦a✝ i⟧) i
-- Mathlib/Computability/RegularExpressions.lean
theorem char_rmatch_iff (a : α) (x : List α) : rmatch (char a) x ↔ x = [a]

Proof state:
case cons.nil
α : Type u_1
inst✝ : DecidableEq α
a head✝ : α
⊢ (char a).rmatch [head✝] = true ↔ [head✝] = [a]

Tactic:
rw [rmatch, deriv, List.singleton_inj]

Result:
case cons.nil
α : Type u_1
inst✝ : DecidableEq α
a head✝ : α
⊢ (if a = head✝ then 1 else 0).rmatch [] = true ↔ head✝ = a

Proof state:
case cons
α : Type u_1
inst✝ : DecidableEq α
a head✝ : α
x : List α
⊢ (char a).rmatch (head✝ :: x) = true ↔ head✝ :: x = [a]

Tactic:
rcases x with - | ⟨head, tail⟩

Result:
case cons.nil
α : Type u_1
inst✝ : DecidableEq α
a head✝ : α
⊢ (char a).rmatch [head✝] = true ↔ [head✝] = [a]

case cons.cons
α : Type u_1
inst✝ : DecidableEq α
a head✝ head : α
tail : List α
⊢ (char a).rmatch (head✝ :: head :: tail) = true ↔ head✝ :: head :: tail = [a]

Proof state:
case cons.cons
α : Type u_1
inst✝ : DecidableEq α
a head✝ head : α
tail : List α
⊢ (char a).rmatch (head✝ :: head :: tail) = true ↔ head✝ :: head :: tail = [a]

Tactic:
rw [rmatch, rmatch, deriv, cons.injEq]

Result:
case cons.cons
α : Type u_1
inst✝ : DecidableEq α
a head✝ head : α
tail : List α
⊢ ((if a = head✝ then 1 else 0).deriv head).rmatch tail = true ↔ head✝ = a ∧ head :: tail = []

Proof state:
case cons.cons
α : Type u_1
inst✝ : DecidableEq α
a head✝ head : α
tail : List α
⊢ ((if a = head✝ then 1 else 0).deriv head).rmatch tail = true ↔ head✝ = a ∧ head :: tail = []

Tactic:
split

Result:
case cons.cons.isTrue
α : Type u_1
inst✝ : DecidableEq α
a head✝ head : α
tail : List α
h✝ : a = head✝
⊢ (deriv 1 head).rmatch tail = true ↔ head✝ = a ∧ head :: tail = []

case cons.cons.isFalse
α : Type u_1
inst✝ : DecidableEq α
a head✝ head : α
tail : List α
h✝ : ¬a = head✝
⊢ (deriv 0 head).rmatch tail = true ↔ head✝ = a ∧ head :: tail = []

Proof state:
case cons.cons.isFalse
α : Type u_1
inst✝ : DecidableEq α
a head✝ head : α
tail : List α
h✝ : ¬a = head✝
⊢ (deriv 0 head).rmatch tail = true ↔ head✝ = a ∧ head :: tail = []

Tactic:
simp_rw [deriv_zero, zero_rmatch, reduceCtorEq, and_false]

Result:
no goals

Proof state:
case cons.nil
α : Type u_1
inst✝ : DecidableEq α
a head✝ : α
⊢ (if a = head✝ then 1 else 0).rmatch [] = true ↔ head✝ = a

Tactic:
split <;> tauto

Result:
no goals

Proof state:
case nil
α : Type u_1
inst✝ : DecidableEq α
a : α
⊢ (char a).rmatch [] = true ↔ [] = [a]

Tactic:
exact of_decide_eq_true rfl

Result:
no goals

Proof state:
case cons.cons.isTrue
α : Type u_1
inst✝ : DecidableEq α
a head✝ head : α
tail : List α
h✝ : a = head✝
⊢ (deriv 1 head).rmatch tail = true ↔ head✝ = a ∧ head :: tail = []

Tactic:
simp_rw [deriv_one, zero_rmatch, reduceCtorEq, and_false]

Result:
no goals

Proof state:
α : Type u_1
inst✝ : DecidableEq α
a : α
x : List α
⊢ (char a).rmatch x = true ↔ x = [a]

Tactic:
rcases x with - | ⟨_, x⟩

Result:
case nil
α : Type u_1
inst✝ : DecidableEq α
a : α
⊢ (char a).rmatch [] = true ↔ [] = [a]

case cons
α : Type u_1
inst✝ : DecidableEq α
a head✝ : α
x : List α
⊢ (char a).rmatch (head✝ :: x) = true ↔ head✝ :: x = [a]
-- Mathlib/CategoryTheory/Preadditive/Biproducts.lean
theorem HasBiproduct.of_hasCoproduct (f : J → C) [HasCoproduct f] : HasBiproduct f

Proof state:
case intro
C : Type u
inst✝³ : Category.{v, u} C
inst✝² : Preadditive C
J : Type
inst✝¹ : Finite J
f : J → C
inst✝ : HasCoproduct f
val✝ : Fintype J
⊢ HasBiproduct f

Tactic:
exact HasBiproduct.mk
  { bicone := _
    isBilimit := biconeIsBilimitOfColimitCoconeOfIsColimit (colimit.isColimit _) }

Result:
no goals

Proof state:
C : Type u
inst✝³ : Category.{v, u} C
inst✝² : Preadditive C
J : Type
inst✝¹ : Finite J
f : J → C
inst✝ : HasCoproduct f
⊢ HasBiproduct f

Tactic:
cases nonempty_fintype J

Result:
case intro
C : Type u
inst✝³ : Category.{v, u} C
inst✝² : Preadditive C
J : Type
inst✝¹ : Finite J
f : J → C
inst✝ : HasCoproduct f
val✝ : Fintype J
⊢ HasBiproduct f
-- Mathlib/Analysis/Convex/Topology.lean
theorem Convex.openSegment_closure_interior_subset_interior {s : Set E} (hs : Convex 𝕜 s) {x y : E}
    (hx : x ∈ closure s) (hy : y ∈ interior s) : openSegment 𝕜 x y ⊆ interior s

Proof state:
case intro.intro.intro.intro.intro
𝕜 : Type u_2
E : Type u_3
inst✝⁵ : LinearOrderedField 𝕜
inst✝⁴ : AddCommGroup E
inst✝³ : Module 𝕜 E
inst✝² : TopologicalSpace E
inst✝¹ : IsTopologicalAddGroup E
inst✝ : ContinuousConstSMul 𝕜 E
s : Set E
hs : Convex 𝕜 s
x y : E
hx : x ∈ closure s
hy : y ∈ interior s
a b : 𝕜
ha : 0 < a
hb : 0 < b
hab : a + b = 1
⊢ a • x + b • y ∈ interior s

Tactic:
exact hs.combo_closure_interior_mem_interior hx hy ha.le hb hab

Result:
no goals

Proof state:
𝕜 : Type u_2
E : Type u_3
inst✝⁵ : LinearOrderedField 𝕜
inst✝⁴ : AddCommGroup E
inst✝³ : Module 𝕜 E
inst✝² : TopologicalSpace E
inst✝¹ : IsTopologicalAddGroup E
inst✝ : ContinuousConstSMul 𝕜 E
s : Set E
hs : Convex 𝕜 s
x y : E
hx : x ∈ closure s
hy : y ∈ interior s
⊢ openSegment 𝕜 x y ⊆ interior s

Tactic:
rintro _ ⟨a, b, ha, hb, hab, rfl⟩

Result:
case intro.intro.intro.intro.intro
𝕜 : Type u_2
E : Type u_3
inst✝⁵ : LinearOrderedField 𝕜
inst✝⁴ : AddCommGroup E
inst✝³ : Module 𝕜 E
inst✝² : TopologicalSpace E
inst✝¹ : IsTopologicalAddGroup E
inst✝ : ContinuousConstSMul 𝕜 E
s : Set E
hs : Convex 𝕜 s
x y : E
hx : x ∈ closure s
hy : y ∈ interior s
a b : 𝕜
ha : 0 < a
hb : 0 < b
hab : a + b = 1
⊢ a • x + b • y ∈ interior s
-- Mathlib/LinearAlgebra/Dimension/Basic.lean
theorem lift_rank_le_of_injective_injective [AddCommGroup M'] [Module R' M']
    (i : R' → R) (j : M →+ M') (hi : ∀ r, i r = 0 → r = 0) (hj : Injective j)
    (hc : ∀ (r : R') (m : M), j (i r • m) = r • j m) :
    lift.{v'} (Module.rank R M) ≤ lift.{v} (Module.rank R' M')

Proof state:
R : Type u
R' : Type u'
M : Type v
M' : Type v'
inst✝⁵ : Ring R
inst✝⁴ : AddCommGroup M
inst✝³ : Module R M
inst✝² : Ring R'
inst✝¹ : AddCommGroup M'
inst✝ : Module R' M'
i : R' → R
j : M →+ M'
hi : ∀ (r : R'), i r = 0 → r = 0
hj : Injective ⇑j
hc : ∀ (r : R') (m : M), j (i r • m) = r • j m
⊢ lift.{v', v} (Module.rank R M) ≤ lift.{v, v'} (Module.rank R' M')

Tactic:
simp_rw [Module.rank, lift_iSup (bddAbove_range _)]

Result:
R : Type u
R' : Type u'
M : Type v
M' : Type v'
inst✝⁵ : Ring R
inst✝⁴ : AddCommGroup M
inst✝³ : Module R M
inst✝² : Ring R'
inst✝¹ : AddCommGroup M'
inst✝ : Module R' M'
i : R' → R
j : M →+ M'
hi : ∀ (r : R'), i r = 0 → r = 0
hj : Injective ⇑j
hc : ∀ (r : R') (m : M), j (i r • m) = r • j m
⊢ ⨆ i, lift.{v', v} #↑↑i ≤ ⨆ i, lift.{v, v'} #↑↑i

Proof state:
R : Type u
R' : Type u'
M : Type v
M' : Type v'
inst✝⁵ : Ring R
inst✝⁴ : AddCommGroup M
inst✝³ : Module R M
inst✝² : Ring R'
inst✝¹ : AddCommGroup M'
inst✝ : Module R' M'
i : R' → R
j : M →+ M'
hi : ∀ (r : R'), i r = 0 → r = 0
hj : Injective ⇑j
hc : ∀ (r : R') (m : M), j (i r • m) = r • j m
x✝² : { s // LinearIndepOn R id s }
s : Set M
h : LinearIndepOn R id s
x✝¹ : M
x✝ : j x✝¹ = 0
⊢ j x✝¹ = j 0

Tactic:
rwa [j.map_zero]

Result:
no goals

Proof state:
R : Type u
R' : Type u'
M : Type v
M' : Type v'
inst✝⁵ : Ring R
inst✝⁴ : AddCommGroup M
inst✝³ : Module R M
inst✝² : Ring R'
inst✝¹ : AddCommGroup M'
inst✝ : Module R' M'
i : R' → R
j : M →+ M'
hi : ∀ (r : R'), i r = 0 → r = 0
hj : Injective ⇑j
hc : ∀ (r : R') (m : M), j (i r • m) = r • j m
⊢ ⨆ i, lift.{v', v} #↑↑i ≤ ⨆ i, lift.{v, v'} #↑↑i

Tactic:
exact ciSup_mono' (bddAbove_range _) fun ⟨s, h⟩ ↦
  ⟨⟨j '' s, LinearIndepOn.id_image <| h.linearIndependent.map_of_injective_injective i j hi
    (fun _ _ ↦ hj <| by rwa [j.map_zero]) hc⟩,
  lift_mk_le'.mpr ⟨(Equiv.Set.image j s hj).toEmbedding⟩⟩

Result:
no goals
-- Mathlib/Computability/Tape.lean
theorem Tape.map_move {Γ Γ'} [Inhabited Γ] [Inhabited Γ'] (f : PointedMap Γ Γ') (T : Tape Γ) (d) :
    (T.move d).map f = (T.map f).move d

Proof state:
case mk
Γ : Type u_1
Γ' : Type u_2
inst✝¹ : Inhabited Γ
inst✝ : Inhabited Γ'
f : PointedMap Γ Γ'
d : Dir
head✝ : Γ
left✝ right✝ : ListBlank Γ
⊢ map f (move d { head := head✝, left := left✝, right := right✝ }) =
    move d (map f { head := head✝, left := left✝, right := right✝ })

Tactic:
cases d <;> simp only [Tape.move, Tape.map, ListBlank.head_map, eq_self_iff_true,
  ListBlank.map_cons, and_self_iff, ListBlank.tail_map]

Result:
no goals

Proof state:
Γ : Type u_1
Γ' : Type u_2
inst✝¹ : Inhabited Γ
inst✝ : Inhabited Γ'
f : PointedMap Γ Γ'
T : Tape Γ
d : Dir
⊢ map f (move d T) = move d (map f T)

Tactic:
cases T

Result:
case mk
Γ : Type u_1
Γ' : Type u_2
inst✝¹ : Inhabited Γ
inst✝ : Inhabited Γ'
f : PointedMap Γ Γ'
d : Dir
head✝ : Γ
left✝ right✝ : ListBlank Γ
⊢ map f (move d { head := head✝, left := left✝, right := right✝ }) =
    move d (map f { head := head✝, left := left✝, right := right✝ })
-- Mathlib/Analysis/SpecificLimits/Normed.lean
theorem isLittleO_pow_pow_of_abs_lt_left {r₁ r₂ : ℝ} (h : |r₁| < |r₂|) :
    (fun n : ℕ ↦ r₁ ^ n) =o[atTop] fun n ↦ r₂ ^ n

Proof state:
r₁ r₂ : ℝ
h : |r₁| < |r₂|
⊢ (fun n => r₁ ^ n) =o[atTop] fun n => r₂ ^ n

Tactic:
refine (IsLittleO.of_norm_left ?_).of_norm_right

Result:
r₁ r₂ : ℝ
h : |r₁| < |r₂|
⊢ (fun x => ‖r₁ ^ x‖) =o[atTop] fun x => ‖r₂ ^ x‖

Proof state:
r₁ r₂ : ℝ
h : |r₁| < |r₂|
⊢ (fun x => ‖r₁ ^ x‖) =o[atTop] fun x => ‖r₂ ^ x‖

Tactic:
exact (isLittleO_pow_pow_of_lt_left (abs_nonneg r₁) h).congr (pow_abs r₁) (pow_abs r₂)

Result:
no goals
-- Mathlib/Probability/Process/Stopping.lean
theorem measurableSet_lt' [TopologicalSpace ι] [OrderTopology ι]
    [FirstCountableTopology ι] (hτ : IsStoppingTime f τ) (i : ι) :
    MeasurableSet[hτ.measurableSpace] {ω | τ ω < i}

Proof state:
Ω : Type u_1
ι : Type u_3
m : MeasurableSpace Ω
inst✝³ : LinearOrder ι
f : Filtration ι m
τ : Ω → ι
inst✝² : TopologicalSpace ι
inst✝¹ : OrderTopology ι
inst✝ : FirstCountableTopology ι
hτ : IsStoppingTime f τ
i : ι
⊢ {ω | τ ω < i} = {ω | τ ω ≤ i} \ {ω | τ ω = i}

Tactic:
ext1 ω

Result:
case h
Ω : Type u_1
ι : Type u_3
m : MeasurableSpace Ω
inst✝³ : LinearOrder ι
f : Filtration ι m
τ : Ω → ι
inst✝² : TopologicalSpace ι
inst✝¹ : OrderTopology ι
inst✝ : FirstCountableTopology ι
hτ : IsStoppingTime f τ
i : ι
ω : Ω
⊢ ω ∈ {ω | τ ω < i} ↔ ω ∈ {ω | τ ω ≤ i} \ {ω | τ ω = i}

Proof state:
Ω : Type u_1
ι : Type u_3
m : MeasurableSpace Ω
inst✝³ : LinearOrder ι
f : Filtration ι m
τ : Ω → ι
inst✝² : TopologicalSpace ι
inst✝¹ : OrderTopology ι
inst✝ : FirstCountableTopology ι
hτ : IsStoppingTime f τ
i : ι
⊢ MeasurableSet {ω | τ ω < i}

Tactic:
have : {ω | τ ω < i} = {ω | τ ω ≤ i} \ {ω | τ ω = i} := by
  ext1 ω
  simp only [lt_iff_le_and_ne, Set.mem_setOf_eq, Set.mem_diff]

Result:
Ω : Type u_1
ι : Type u_3
m : MeasurableSpace Ω
inst✝³ : LinearOrder ι
f : Filtration ι m
τ : Ω → ι
inst✝² : TopologicalSpace ι
inst✝¹ : OrderTopology ι
inst✝ : FirstCountableTopology ι
hτ : IsStoppingTime f τ
i : ι
this : {ω | τ ω < i} = {ω | τ ω ≤ i} \ {ω | τ ω = i}
⊢ MeasurableSet {ω | τ ω < i}

Proof state:
Ω : Type u_1
ι : Type u_3
m : MeasurableSpace Ω
inst✝³ : LinearOrder ι
f : Filtration ι m
τ : Ω → ι
inst✝² : TopologicalSpace ι
inst✝¹ : OrderTopology ι
inst✝ : FirstCountableTopology ι
hτ : IsStoppingTime f τ
i : ι
this : {ω | τ ω < i} = {ω | τ ω ≤ i} \ {ω | τ ω = i}
⊢ MeasurableSet ({ω | τ ω ≤ i} \ {ω | τ ω = i})

Tactic:
exact (hτ.measurableSet_le' i).diff (hτ.measurableSet_eq' i)

Result:
no goals

Proof state:
case h
Ω : Type u_1
ι : Type u_3
m : MeasurableSpace Ω
inst✝³ : LinearOrder ι
f : Filtration ι m
τ : Ω → ι
inst✝² : TopologicalSpace ι
inst✝¹ : OrderTopology ι
inst✝ : FirstCountableTopology ι
hτ : IsStoppingTime f τ
i : ι
ω : Ω
⊢ ω ∈ {ω | τ ω < i} ↔ ω ∈ {ω | τ ω ≤ i} \ {ω | τ ω = i}

Tactic:
simp only [lt_iff_le_and_ne, Set.mem_setOf_eq, Set.mem_diff]

Result:
no goals

Proof state:
Ω : Type u_1
ι : Type u_3
m : MeasurableSpace Ω
inst✝³ : LinearOrder ι
f : Filtration ι m
τ : Ω → ι
inst✝² : TopologicalSpace ι
inst✝¹ : OrderTopology ι
inst✝ : FirstCountableTopology ι
hτ : IsStoppingTime f τ
i : ι
this : {ω | τ ω < i} = {ω | τ ω ≤ i} \ {ω | τ ω = i}
⊢ MeasurableSet {ω | τ ω < i}

Tactic:
rw [this]

Result:
Ω : Type u_1
ι : Type u_3
m : MeasurableSpace Ω
inst✝³ : LinearOrder ι
f : Filtration ι m
τ : Ω → ι
inst✝² : TopologicalSpace ι
inst✝¹ : OrderTopology ι
inst✝ : FirstCountableTopology ι
hτ : IsStoppingTime f τ
i : ι
this : {ω | τ ω < i} = {ω | τ ω ≤ i} \ {ω | τ ω = i}
⊢ MeasurableSet ({ω | τ ω ≤ i} \ {ω | τ ω = i})
-- Mathlib/Data/W/Constructions.lean
theorem leftInverse_list : Function.LeftInverse (ofList γ) (toList _)
  | WType.mk Listα.nil f => by
    simp only [toList, ofList, mk.injEq, heq_eq_eq, true_and]
    ext x
    cases x
  | WType.mk (Listα.cons x) f => by
    simp only [toList, ofList, leftInverse_list (f PUnit.unit), mk.injEq, heq_eq_eq, true_and]
    rfl

Proof state:
case h
γ : Type u
f : Listβ γ Listα.nil → WType (Listβ γ)
x : PEmpty.{u + 1}
⊢ x.elim = f x

Tactic:
cases x

Result:
no goals

Proof state:
γ : Type u
f : Listβ γ Listα.nil → WType (Listβ γ)
⊢ ofList γ (toList γ (mk Listα.nil f)) = mk Listα.nil f

Tactic:
simp only [toList, ofList, mk.injEq, heq_eq_eq, true_and]

Result:
γ : Type u
f : Listβ γ Listα.nil → WType (Listβ γ)
⊢ PEmpty.elim = f

Proof state:
γ : Type u
x : γ
f : Listβ γ (Listα.cons x) → WType (Listβ γ)
⊢ (fun x => f PUnit.unit) = f

Tactic:
rfl

Result:
no goals

Proof state:
γ : Type u
f : Listβ γ Listα.nil → WType (Listβ γ)
⊢ PEmpty.elim = f

Tactic:
ext x

Result:
case h
γ : Type u
f : Listβ γ Listα.nil → WType (Listβ γ)
x : PEmpty.{u + 1}
⊢ x.elim = f x

Proof state:
γ : Type u
x : γ
f : Listβ γ (Listα.cons x) → WType (Listβ γ)
⊢ ofList γ (toList γ (mk (Listα.cons x) f)) = mk (Listα.cons x) f

Tactic:
simp only [toList, ofList, leftInverse_list (f PUnit.unit), mk.injEq, heq_eq_eq, true_and]

Result:
γ : Type u
x : γ
f : Listβ γ (Listα.cons x) → WType (Listβ γ)
⊢ (fun x => f PUnit.unit) = f
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/List/Find.lean
theorem findIdx_eq_getD_findIdx? {xs : List α} {p : α → Bool} :
    xs.findIdx p = (xs.findIdx? p).getD xs.length

Proof state:
case nil
α : Type u_1
p : α → Bool
⊢ findIdx p [] = (findIdx? p []).getD [].length

Tactic:
simp

Result:
no goals

Proof state:
case cons
α : Type u_1
p : α → Bool
x : α
xs : List α
ih : findIdx p xs = (findIdx? p xs).getD xs.length
⊢ findIdx p (x :: xs) = (findIdx? p (x :: xs)).getD (x :: xs).length

Tactic:
simp only [findIdx_cons, findIdx?_cons]

Result:
case cons
α : Type u_1
p : α → Bool
x : α
xs : List α
ih : findIdx p xs = (findIdx? p xs).getD xs.length
⊢ (bif p x then 0 else findIdx p xs + 1) =
    (if p x = true then some 0 else Option.map (fun i => i + 1) (findIdx? p xs)).getD (x :: xs).length

Proof state:
α : Type u_1
xs : List α
p : α → Bool
⊢ findIdx p xs = (findIdx? p xs).getD xs.length

Tactic:
induction xs with
| nil => simp
| cons x xs ih =>
  simp only [findIdx_cons, findIdx?_cons]
  split <;> simp_all [ih]

Result:
no goals

Proof state:
case cons
α : Type u_1
p : α → Bool
x : α
xs : List α
ih : findIdx p xs = (findIdx? p xs).getD xs.length
⊢ (bif p x then 0 else findIdx p xs + 1) =
    (if p x = true then some 0 else Option.map (fun i => i + 1) (findIdx? p xs)).getD (x :: xs).length

Tactic:
split <;> simp_all [ih]

Result:
no goals
-- Mathlib/Data/Int/Log.lean
theorem clog_one_right (b : ℕ) : clog b (1 : R) = 0

Proof state:
R : Type u_1
inst✝¹ : LinearOrderedSemifield R
inst✝ : FloorSemiring R
b : ℕ
⊢ clog b 1 = 0

Tactic:
rw [clog_of_one_le_right _ le_rfl, Nat.ceil_one, Nat.clog_one_right, Int.ofNat_zero]

Result:
no goals
-- Mathlib/Data/ENNReal/Inv.lean
theorem coe_inv (hr : r ≠ 0) : (↑r⁻¹ : ℝ≥0∞) = (↑r)⁻¹ :=
  coe_inv_le.antisymm <| sInf_le <| mem_setOf.2 <| by rw [← coe_mul, mul_inv_cancel₀ hr, coe_one]

Proof state:
r : ℝ≥0
hr : r ≠ 0
⊢ 1 ≤ ↑r * ↑r⁻¹

Tactic:
rw [← coe_mul, mul_inv_cancel₀ hr, coe_one]

Result:
no goals
-- Mathlib/NumberTheory/LegendreSymbol/QuadraticChar/Basic.lean
theorem quadraticChar_eq_neg_one_iff_not_one {a : F} (ha : a ≠ 0) :
    quadraticChar F a = -1 ↔ ¬quadraticChar F a = 1 :=
  ⟨fun h ↦ by rw [h]; omega, fun h₂ ↦ (or_iff_right h₂).mp (quadraticChar_dichotomy ha)⟩

Proof state:
F : Type u_1
inst✝² : Field F
inst✝¹ : Fintype F
inst✝ : DecidableEq F
a : F
ha : a ≠ 0
h : (quadraticChar F) a = -1
⊢ ¬-1 = 1

Tactic:
omega

Result:
no goals

Proof state:
F : Type u_1
inst✝² : Field F
inst✝¹ : Fintype F
inst✝ : DecidableEq F
a : F
ha : a ≠ 0
h : (quadraticChar F) a = -1
⊢ ¬(quadraticChar F) a = 1

Tactic:
rw [h]

Result:
F : Type u_1
inst✝² : Field F
inst✝¹ : Fintype F
inst✝ : DecidableEq F
a : F
ha : a ≠ 0
h : (quadraticChar F) a = -1
⊢ ¬-1 = 1
-- Mathlib/AlgebraicGeometry/EllipticCurve/Jacobian.lean
@[simp]
protected lemma map_add {K : Type v} [Field K] (f : F →+* K) {P Q : Fin 3 → F}
    (hP : W.Nonsingular P) (hQ : W.Nonsingular Q) :
    (W.map f).toJacobian.add (f ∘ P) (f ∘ Q) = f ∘ W.add P Q

Proof state:
case neg
F : Type u
inst✝¹ : Field F
W : Jacobian F
K : Type v
inst✝ : Field K
f : F →+* K
P Q : Fin 3 → F
hP : W.Nonsingular P
hQ : W.Nonsingular Q
h : ¬P ≈ Q
⊢ (map W f).toJacobian.add (⇑f ∘ P) (⇑f ∘ Q) = ⇑f ∘ W.add P Q

Tactic:
rw [add_of_not_equiv <| h.comp (comp_equiv_comp f hP hQ).mp, add_of_not_equiv h, map_addXYZ]

Result:
no goals

Proof state:
case pos
F : Type u
inst✝¹ : Field F
W : Jacobian F
K : Type v
inst✝ : Field K
f : F →+* K
P Q : Fin 3 → F
hP : W.Nonsingular P
hQ : W.Nonsingular Q
h : P ≈ Q
⊢ (map W f).toJacobian.add (⇑f ∘ P) (⇑f ∘ Q) = ⇑f ∘ W.add P Q

Tactic:
rw [add_of_equiv <| (comp_equiv_comp f hP hQ).mpr h, add_of_equiv h, map_dblXYZ]

Result:
no goals

Proof state:
F : Type u
inst✝¹ : Field F
W : Jacobian F
K : Type v
inst✝ : Field K
f : F →+* K
P Q : Fin 3 → F
hP : W.Nonsingular P
hQ : W.Nonsingular Q
⊢ (map W f).toJacobian.add (⇑f ∘ P) (⇑f ∘ Q) = ⇑f ∘ W.add P Q

Tactic:
by_cases h : P ≈ Q

Result:
case pos
F : Type u
inst✝¹ : Field F
W : Jacobian F
K : Type v
inst✝ : Field K
f : F →+* K
P Q : Fin 3 → F
hP : W.Nonsingular P
hQ : W.Nonsingular Q
h : P ≈ Q
⊢ (map W f).toJacobian.add (⇑f ∘ P) (⇑f ∘ Q) = ⇑f ∘ W.add P Q

case neg
F : Type u
inst✝¹ : Field F
W : Jacobian F
K : Type v
inst✝ : Field K
f : F →+* K
P Q : Fin 3 → F
hP : W.Nonsingular P
hQ : W.Nonsingular Q
h : ¬P ≈ Q
⊢ (map W f).toJacobian.add (⇑f ∘ P) (⇑f ∘ Q) = ⇑f ∘ W.add P Q
-- Mathlib/Order/Cover.lean
theorem wcovBy_iff_Ioo_eq : a ⩿ b ↔ a ≤ b ∧ Ioo a b = ∅ :=
  and_congr_right' <| by simp [eq_empty_iff_forall_not_mem]

Proof state:
α : Type u_1
inst✝ : Preorder α
a b : α
⊢ (∀ ⦃c : α⦄, a < c → ¬c < b) ↔ Ioo a b = ∅

Tactic:
simp [eq_empty_iff_forall_not_mem]

Result:
no goals
-- Mathlib/Algebra/Field/Subfield/Basic.lean
theorem mem_iInf {ι : Sort*} {S : ι → Subfield K} {x : K} : (x ∈ ⨅ i, S i) ↔ ∀ i, x ∈ S i

Proof state:
K : Type u
inst✝ : DivisionRing K
ι : Sort u_1
S : ι → Subfield K
x : K
⊢ x ∈ ⨅ i, S i ↔ ∀ (i : ι), x ∈ S i

Tactic:
simp only [iInf, mem_sInf, Set.forall_mem_range]

Result:
no goals
-- Mathlib/MeasureTheory/Measure/Typeclasses.lean
theorem finiteAtBot {m0 : MeasurableSpace α} (μ : Measure α) : μ.FiniteAtFilter ⊥ :=
  ⟨∅, mem_bot, by simp only [measure_empty, zero_lt_top]⟩

Proof state:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
⊢ μ ∅ < ⊤

Tactic:
simp only [measure_empty, zero_lt_top]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Int/Order.lean
theorem lt_iff_le_not_le {a b : Int} : a < b ↔ a ≤ b ∧ ¬b ≤ a

Proof state:
a b : Int
⊢ a < b ↔ a ≤ b ∧ ¬b ≤ a

Tactic:
rw [Int.lt_iff_le_and_ne]

Result:
a b : Int
⊢ a ≤ b ∧ a ≠ b ↔ a ≤ b ∧ ¬b ≤ a

Proof state:
case mpr
a b : Int
x✝ : a ≤ b ∧ ¬b ≤ a
h : a ≤ b
h'✝ : ¬b ≤ a
h' : a = b
⊢ b ≤ a

Tactic:
subst h'

Result:
case mpr
a : Int
x✝ : a ≤ a ∧ ¬a ≤ a
h : a ≤ a
h' : ¬a ≤ a
⊢ a ≤ a

Proof state:
case mp
a b : Int
x✝ : a ≤ b ∧ a ≠ b
h : a ≤ b
h'✝ : a ≠ b
h' : b ≤ a
⊢ a = b

Tactic:
exact Int.le_antisymm h h'

Result:
no goals

Proof state:
a b : Int
⊢ a ≤ b ∧ a ≠ b ↔ a ≤ b ∧ ¬b ≤ a

Tactic:
constructor <;> refine fun ⟨h, h'⟩ => ⟨h, h'.imp fun h' => ?_⟩

Result:
case mp
a b : Int
x✝ : a ≤ b ∧ a ≠ b
h : a ≤ b
h'✝ : a ≠ b
h' : b ≤ a
⊢ a = b

case mpr
a b : Int
x✝ : a ≤ b ∧ ¬b ≤ a
h : a ≤ b
h'✝ : ¬b ≤ a
h' : a = b
⊢ b ≤ a

Proof state:
case mpr
a : Int
x✝ : a ≤ a ∧ ¬a ≤ a
h : a ≤ a
h' : ¬a ≤ a
⊢ a ≤ a

Tactic:
apply Int.le_refl

Result:
no goals