harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/SetTheory/Game/Ordinal.lean
theorem toPGame_nmul (a b : Ordinal) : (a ⨳ b).toPGame ≈ a.toPGame * b.toPGame

Proof state:
case refine_2
a b : Ordinal.{u_1}
i : (a.toPGame * b.toPGame).LeftMoves
⊢ (a.toPGame * b.toPGame).moveLeft i ⧏ (a ⨳ b).toPGame

Tactic:
apply leftMoves_mul_cases i _ isEmptyElim

Result:
a b : Ordinal.{u_1}
i : (a.toPGame * b.toPGame).LeftMoves
⊢ ∀ (ix : a.toPGame.LeftMoves) (iy : b.toPGame.LeftMoves),
    (a.toPGame * b.toPGame).moveLeft (toLeftMovesMul (Sum.inl (ix, iy))) ⧏ (a ⨳ b).toPGame

Proof state:
a b : Ordinal.{u_1}
i✝ : (a.toPGame * b.toPGame).LeftMoves
i : a.toPGame.LeftMoves
j : b.toPGame.LeftMoves
⊢ ¬⟦(a ⨳ b).toPGame⟧ + ⟦(↑(toLeftMovesToPGame.symm i) ⨳ ↑(toLeftMovesToPGame.symm j)).toPGame⟧ ≤
      ⟦(↑(toLeftMovesToPGame.symm i) ⨳ b).toPGame⟧ + ⟦a.toPGame * (↑(toLeftMovesToPGame.symm j)).toPGame⟧

Tactic:
rw [← game_eq (toPGame_nmul _ _)]

Result:
a b : Ordinal.{u_1}
i✝ : (a.toPGame * b.toPGame).LeftMoves
i : a.toPGame.LeftMoves
j : b.toPGame.LeftMoves
⊢ ¬⟦(a ⨳ b).toPGame⟧ + ⟦(↑(toLeftMovesToPGame.symm i) ⨳ ↑(toLeftMovesToPGame.symm j)).toPGame⟧ ≤
      ⟦(↑(toLeftMovesToPGame.symm i) ⨳ b).toPGame⟧ + ⟦(a ⨳ ↑(toLeftMovesToPGame.symm j)).toPGame⟧

Proof state:
a b : Ordinal.{u_1}
i✝ : (a.toPGame * b.toPGame).LeftMoves
i : a.toPGame.LeftMoves
j : b.toPGame.LeftMoves
⊢ ¬toGame (a ⨳ b ♯ ↑(toLeftMovesToPGame.symm i) ⨳ ↑(toLeftMovesToPGame.symm j)) ≤
      toGame (↑(toLeftMovesToPGame.symm i) ⨳ b ♯ a ⨳ ↑(toLeftMovesToPGame.symm j))

Tactic:
apply toPGame_lf (nmul_nadd_lt _ _) <;>
exact toLeftMovesToPGame_symm_lt _

Result:
no goals

Proof state:
case refine_1
a b : Ordinal.{u_1}
i : (a ⨳ b).toPGame.LeftMoves
⊢ (↑(toLeftMovesToPGame.symm i)).toPGame ⧏ a.toPGame * b.toPGame

Tactic:
rcases lt_nmul_iff.1 (toLeftMovesToPGame_symm_lt i) with ⟨c, hc, d, hd, h⟩

Result:
case refine_1.intro.intro.intro.intro
a b : Ordinal.{u_1}
i : (a ⨳ b).toPGame.LeftMoves
c : Ordinal.{u_1}
hc : c < a
d : Ordinal.{u_1}
hd : d < b
h : ↑(toLeftMovesToPGame.symm i) ♯ c ⨳ d ≤ c ⨳ b ♯ a ⨳ d
⊢ (↑(toLeftMovesToPGame.symm i)).toPGame ⧏ a.toPGame * b.toPGame
-- Mathlib/Algebra/Homology/Homotopy.lean
theorem dNext_eq (f : ∀ i j, C.X i ⟶ D.X j) {i i' : ι} (w : c.Rel i i') :
    dNext i f = C.d i i' ≫ f i' i

Proof state:
ι : Type u_1
V : Type u
inst✝¹ : Category.{v, u} V
inst✝ : Preadditive V
c : ComplexShape ι
C D : HomologicalComplex V c
f : (i j : ι) → C.X i ⟶ D.X j
i : ι
w : c.Rel i (c.next i)
⊢ (dNext i) f = C.d i (c.next i) ≫ f (c.next i) i

Tactic:
rfl

Result:
no goals

Proof state:
ι : Type u_1
V : Type u
inst✝¹ : Category.{v, u} V
inst✝ : Preadditive V
c : ComplexShape ι
C D : HomologicalComplex V c
f : (i j : ι) → C.X i ⟶ D.X j
i i' : ι
w : c.Rel i i'
⊢ (dNext i) f = C.d i i' ≫ f i' i

Tactic:
obtain rfl := c.next_eq' w

Result:
ι : Type u_1
V : Type u
inst✝¹ : Category.{v, u} V
inst✝ : Preadditive V
c : ComplexShape ι
C D : HomologicalComplex V c
f : (i j : ι) → C.X i ⟶ D.X j
i : ι
w : c.Rel i (c.next i)
⊢ (dNext i) f = C.d i (c.next i) ≫ f (c.next i) i
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Bool.lean
theorem forall_bool' {p : Bool → Prop} (b : Bool) : (∀ x, p x) ↔ p b ∧ p !b :=
  ⟨fun h ↦ ⟨h _, h _⟩, fun ⟨h₁, h₂⟩ x ↦ by cases b <;> cases x <;> assumption⟩

Proof state:
p : Bool → Prop
b : Bool
x✝ : p b ∧ p !b
x : Bool
h₁ : p b
h₂ : p !b
⊢ p x

Tactic:
cases b <;> cases x <;> assumption

Result:
no goals
-- Mathlib/Geometry/Euclidean/Angle/Oriented/Affine.lean
theorem collinear_iff_of_two_zsmul_oangle_eq {p₁ p₂ p₃ p₄ p₅ p₆ : P}
    (h : (2 : ℤ) • ∡ p₁ p₂ p₃ = (2 : ℤ) • ∡ p₄ p₅ p₆) :
    Collinear ℝ ({p₁, p₂, p₃} : Set P) ↔ Collinear ℝ ({p₄, p₅, p₆} : Set P)

Proof state:
V : Type u_1
P : Type u_2
inst✝⁴ : NormedAddCommGroup V
inst✝³ : InnerProductSpace ℝ V
inst✝² : MetricSpace P
inst✝¹ : NormedAddTorsor V P
hd2 : Fact (finrank ℝ V = 2)
inst✝ : Oriented ℝ V (Fin 2)
p₁ p₂ p₃ p₄ p₅ p₆ : P
h : 2 • ∡ p₁ p₂ p₃ = 2 • ∡ p₄ p₅ p₆
⊢ Collinear ℝ {p₁, p₂, p₃} ↔ Collinear ℝ {p₄, p₅, p₆}

Tactic:
simp_rw [← oangle_eq_zero_or_eq_pi_iff_collinear, ← Real.Angle.two_zsmul_eq_zero_iff, h]

Result:
no goals
-- Mathlib/Data/Sym/Sym2.lean
lemma lift_smul_lift {α R N} [SMul R N] (f : { f : α → α → R // ∀ a₁ a₂, f a₁ a₂ = f a₂ a₁ })
    (g : { g : α → α → N // ∀ a₁ a₂, g a₁ a₂ = g a₂ a₁ }) :
    lift f • lift g = lift ⟨f.val • g.val, fun _ _ => by
      rw [Pi.smul_apply', Pi.smul_apply', Pi.smul_apply', Pi.smul_apply', f.prop, g.prop]⟩

Proof state:
α : Type u_4
R : Type u_5
N : Type u_6
inst✝ : SMul R N
f : { f // ∀ (a₁ a₂ : α), f a₁ a₂ = f a₂ a₁ }
g : { g // ∀ (a₁ a₂ : α), g a₁ a₂ = g a₂ a₁ }
⊢ lift f • lift g = lift ⟨↑f • ↑g, ⋯⟩

Tactic:
ext ⟨i,j⟩

Result:
case h.mk.mk
α : Type u_4
R : Type u_5
N : Type u_6
inst✝ : SMul R N
f : { f // ∀ (a₁ a₂ : α), f a₁ a₂ = f a₂ a₁ }
g : { g // ∀ (a₁ a₂ : α), g a₁ a₂ = g a₂ a₁ }
x✝ : Sym2 α
i j : α
⊢ (lift f • lift g) (Quot.mk (Rel α) (i, j)) = lift ⟨↑f • ↑g, ⋯⟩ (Quot.mk (Rel α) (i, j))

Proof state:
α✝ : Type u_1
β : Type u_2
γ : Type u_3
e : Sym2 α✝
f✝ : α✝ → β
α : Type ?u.75759
R : Type ?u.75697
N : Type ?u.75696
inst✝ : SMul R N
f : { f // ∀ (a₁ a₂ : α), f a₁ a₂ = f a₂ a₁ }
g : { g // ∀ (a₁ a₂ : α), g a₁ a₂ = g a₂ a₁ }
x✝¹ x✝ : α
⊢ (↑f • ↑g) x✝¹ x✝ = (↑f • ↑g) x✝ x✝¹

Tactic:
rw [Pi.smul_apply', Pi.smul_apply', Pi.smul_apply', Pi.smul_apply', f.prop, g.prop]

Result:
no goals

Proof state:
case h.mk.mk
α : Type u_4
R : Type u_5
N : Type u_6
inst✝ : SMul R N
f : { f // ∀ (a₁ a₂ : α), f a₁ a₂ = f a₂ a₁ }
g : { g // ∀ (a₁ a₂ : α), g a₁ a₂ = g a₂ a₁ }
x✝ : Sym2 α
i j : α
⊢ (lift f • lift g) (Quot.mk (Rel α) (i, j)) = lift ⟨↑f • ↑g, ⋯⟩ (Quot.mk (Rel α) (i, j))

Tactic:
simp_all only [Pi.smul_apply', lift_mk]

Result:
no goals
-- Mathlib/Data/Set/Card.lean
theorem exists_ne_of_one_lt_ncard (hs : 1 < s.ncard) (a : α) : ∃ b, b ∈ s ∧ b ≠ a

Proof state:
α : Type u_1
s : Set α
a : α
hsf : s.Finite
hs : 1 < hsf.toFinset.card
⊢ ∃ b ∈ s, b ≠ a

Tactic:
simpa only [Finite.mem_toFinset] using Finset.exists_ne_of_one_lt_card hs a

Result:
no goals

Proof state:
α : Type u_1
s : Set α
hs : 1 < s.ncard
a : α
⊢ ∃ b ∈ s, b ≠ a

Tactic:
have hsf := finite_of_ncard_ne_zero (zero_lt_one.trans hs).ne.symm

Result:
α : Type u_1
s : Set α
hs : 1 < s.ncard
a : α
hsf : s.Finite
⊢ ∃ b ∈ s, b ≠ a

Proof state:
α : Type u_1
s : Set α
hs : 1 < s.ncard
a : α
hsf : s.Finite
⊢ ∃ b ∈ s, b ≠ a

Tactic:
rw [ncard_eq_toFinset_card _ hsf] at hs

Result:
α : Type u_1
s : Set α
a : α
hsf : s.Finite
hs : 1 < hsf.toFinset.card
⊢ ∃ b ∈ s, b ≠ a
-- Mathlib/Algebra/SMulWithZero.lean
theorem smul_inv₀ [SMulCommClass α β β] [IsScalarTower α β β] (c : α) (x : β) :
    (c • x)⁻¹ = c⁻¹ • x⁻¹

Proof state:
case inr.inr
α : Type u_5
β : Type u_6
inst✝⁴ : GroupWithZero α
inst✝³ : GroupWithZero β
inst✝² : MulActionWithZero α β
inst✝¹ : SMulCommClass α β β
inst✝ : IsScalarTower α β β
c : α
x : β
hc : c ≠ 0
hx : x ≠ 0
⊢ (c • x)⁻¹ = c⁻¹ • x⁻¹

Tactic:
refine inv_eq_of_mul_eq_one_left ?_

Result:
case inr.inr
α : Type u_5
β : Type u_6
inst✝⁴ : GroupWithZero α
inst✝³ : GroupWithZero β
inst✝² : MulActionWithZero α β
inst✝¹ : SMulCommClass α β β
inst✝ : IsScalarTower α β β
c : α
x : β
hc : c ≠ 0
hx : x ≠ 0
⊢ c⁻¹ • x⁻¹ * c • x = 1

Proof state:
case inl
α : Type u_5
β : Type u_6
inst✝⁴ : GroupWithZero α
inst✝³ : GroupWithZero β
inst✝² : MulActionWithZero α β
inst✝¹ : SMulCommClass α β β
inst✝ : IsScalarTower α β β
x : β
⊢ (0 • x)⁻¹ = 0⁻¹ • x⁻¹

Tactic:
simp only [inv_zero, zero_smul]

Result:
no goals

Proof state:
α : Type u_5
β : Type u_6
inst✝⁴ : GroupWithZero α
inst✝³ : GroupWithZero β
inst✝² : MulActionWithZero α β
inst✝¹ : SMulCommClass α β β
inst✝ : IsScalarTower α β β
c : α
x : β
⊢ (c • x)⁻¹ = c⁻¹ • x⁻¹

Tactic:
obtain rfl | hc := eq_or_ne c 0

Result:
case inl
α : Type u_5
β : Type u_6
inst✝⁴ : GroupWithZero α
inst✝³ : GroupWithZero β
inst✝² : MulActionWithZero α β
inst✝¹ : SMulCommClass α β β
inst✝ : IsScalarTower α β β
x : β
⊢ (0 • x)⁻¹ = 0⁻¹ • x⁻¹

case inr
α : Type u_5
β : Type u_6
inst✝⁴ : GroupWithZero α
inst✝³ : GroupWithZero β
inst✝² : MulActionWithZero α β
inst✝¹ : SMulCommClass α β β
inst✝ : IsScalarTower α β β
c : α
x : β
hc : c ≠ 0
⊢ (c • x)⁻¹ = c⁻¹ • x⁻¹

Proof state:
case inr.inr
α : Type u_5
β : Type u_6
inst✝⁴ : GroupWithZero α
inst✝³ : GroupWithZero β
inst✝² : MulActionWithZero α β
inst✝¹ : SMulCommClass α β β
inst✝ : IsScalarTower α β β
c : α
x : β
hc : c ≠ 0
hx : x ≠ 0
⊢ c⁻¹ • x⁻¹ * c • x = 1

Tactic:
rw [smul_mul_smul_comm, inv_mul_cancel₀ hc, inv_mul_cancel₀ hx, one_smul]

Result:
no goals

Proof state:
case inr.inl
α : Type u_5
β : Type u_6
inst✝⁴ : GroupWithZero α
inst✝³ : GroupWithZero β
inst✝² : MulActionWithZero α β
inst✝¹ : SMulCommClass α β β
inst✝ : IsScalarTower α β β
c : α
hc : c ≠ 0
⊢ (c • 0)⁻¹ = c⁻¹ • 0⁻¹

Tactic:
simp only [inv_zero, smul_zero]

Result:
no goals

Proof state:
case inr
α : Type u_5
β : Type u_6
inst✝⁴ : GroupWithZero α
inst✝³ : GroupWithZero β
inst✝² : MulActionWithZero α β
inst✝¹ : SMulCommClass α β β
inst✝ : IsScalarTower α β β
c : α
x : β
hc : c ≠ 0
⊢ (c • x)⁻¹ = c⁻¹ • x⁻¹

Tactic:
obtain rfl | hx := eq_or_ne x 0

Result:
case inr.inl
α : Type u_5
β : Type u_6
inst✝⁴ : GroupWithZero α
inst✝³ : GroupWithZero β
inst✝² : MulActionWithZero α β
inst✝¹ : SMulCommClass α β β
inst✝ : IsScalarTower α β β
c : α
hc : c ≠ 0
⊢ (c • 0)⁻¹ = c⁻¹ • 0⁻¹

case inr.inr
α : Type u_5
β : Type u_6
inst✝⁴ : GroupWithZero α
inst✝³ : GroupWithZero β
inst✝² : MulActionWithZero α β
inst✝¹ : SMulCommClass α β β
inst✝ : IsScalarTower α β β
c : α
x : β
hc : c ≠ 0
hx : x ≠ 0
⊢ (c • x)⁻¹ = c⁻¹ • x⁻¹
-- Mathlib/RingTheory/Polynomial/Cyclotomic/Basic.lean
theorem cyclotomic_dvd_geom_sum_of_dvd (R) [Ring R] {d n : ℕ} (hdn : d ∣ n) (hd : d ≠ 1) :
    cyclotomic d R ∣ ∑ i ∈ Finset.range n, X ^ i

Proof state:
case inr
R : Type u_1
inst✝ : Ring R
d n : ℕ
hdn : d ∣ n
hd : d ≠ 1
hn : n > 0
⊢ cyclotomic d ℤ ∣ ∑ i ∈ range n, X ^ i

Tactic:
rw [← prod_cyclotomic_eq_geom_sum hn]

Result:
case inr
R : Type u_1
inst✝ : Ring R
d n : ℕ
hdn : d ∣ n
hd : d ≠ 1
hn : n > 0
⊢ cyclotomic d ℤ ∣ ∏ i ∈ n.divisors.erase 1, cyclotomic i ℤ

Proof state:
R : Type u_1
inst✝ : Ring R
d n : ℕ
hdn : d ∣ n
hd : d ≠ 1
⊢ cyclotomic d ℤ ∣ ∑ i ∈ range n, X ^ i

Tactic:
rcases n.eq_zero_or_pos with (rfl | hn)

Result:
case inl
R : Type u_1
inst✝ : Ring R
d : ℕ
hd : d ≠ 1
hdn : d ∣ 0
⊢ cyclotomic d ℤ ∣ ∑ i ∈ range 0, X ^ i

case inr
R : Type u_1
inst✝ : Ring R
d n : ℕ
hdn : d ∣ n
hd : d ≠ 1
hn : n > 0
⊢ cyclotomic d ℤ ∣ ∑ i ∈ range n, X ^ i

Proof state:
R : Type u_1
inst✝ : Ring R
d n : ℕ
hdn : d ∣ n
hd : d ≠ 1
⊢ cyclotomic d R ∣ ∑ i ∈ range n, X ^ i

Tactic:
suffices cyclotomic d ℤ ∣ ∑ i ∈ Finset.range n, X ^ i by
  simpa only [map_cyclotomic_int, Polynomial.map_sum, Polynomial.map_pow, Polynomial.map_X] using
    map_dvd (Int.castRingHom R) this

Result:
R : Type u_1
inst✝ : Ring R
d n : ℕ
hdn : d ∣ n
hd : d ≠ 1
⊢ cyclotomic d ℤ ∣ ∑ i ∈ range n, X ^ i

Proof state:
R : Type u_1
inst✝ : Ring R
d n : ℕ
hdn : d ∣ n
hd : d ≠ 1
this : cyclotomic d ℤ ∣ ∑ i ∈ range n, X ^ i
⊢ cyclotomic d R ∣ ∑ i ∈ range n, X ^ i

Tactic:
simpa only [map_cyclotomic_int, Polynomial.map_sum, Polynomial.map_pow, Polynomial.map_X] using
  map_dvd (Int.castRingHom R) this

Result:
no goals

Proof state:
case inl
R : Type u_1
inst✝ : Ring R
d : ℕ
hd : d ≠ 1
hdn : d ∣ 0
⊢ cyclotomic d ℤ ∣ ∑ i ∈ range 0, X ^ i

Tactic:
simp

Result:
no goals

Proof state:
case inr.ha
R : Type u_1
inst✝ : Ring R
d n : ℕ
hdn : d ∣ n
hd : d ≠ 1
hn : n > 0
⊢ d ∈ n.divisors.erase 1

Tactic:
simp [hd, hdn, hn.ne']

Result:
no goals

Proof state:
case inr
R : Type u_1
inst✝ : Ring R
d n : ℕ
hdn : d ∣ n
hd : d ≠ 1
hn : n > 0
⊢ cyclotomic d ℤ ∣ ∏ i ∈ n.divisors.erase 1, cyclotomic i ℤ

Tactic:
apply Finset.dvd_prod_of_mem

Result:
case inr.ha
R : Type u_1
inst✝ : Ring R
d n : ℕ
hdn : d ∣ n
hd : d ≠ 1
hn : n > 0
⊢ d ∈ n.divisors.erase 1
-- Mathlib/FieldTheory/PurelyInseparable/Basic.lean
theorem eq_separableClosure_iff [Algebra.IsAlgebraic F E] (L : IntermediateField F E) :
    L = separableClosure F E ↔ Algebra.IsSeparable F L ∧ IsPurelyInseparable L E :=
  ⟨by rintro rfl; exact ⟨isSeparable F E, isPurelyInseparable F E⟩,
   fun ⟨_, _⟩ ↦ eq_separableClosure F E L⟩

Proof state:
F : Type u
E : Type v
inst✝³ : Field F
inst✝² : Field E
inst✝¹ : Algebra F E
inst✝ : Algebra.IsAlgebraic F E
⊢ Algebra.IsSeparable F ↥(separableClosure F E) ∧ IsPurelyInseparable (↥(separableClosure F E)) E

Tactic:
exact ⟨isSeparable F E, isPurelyInseparable F E⟩

Result:
no goals

Proof state:
F : Type u
E : Type v
inst✝³ : Field F
inst✝² : Field E
inst✝¹ : Algebra F E
inst✝ : Algebra.IsAlgebraic F E
L : IntermediateField F E
⊢ L = separableClosure F E → Algebra.IsSeparable F ↥L ∧ IsPurelyInseparable (↥L) E

Tactic:
rintro rfl

Result:
F : Type u
E : Type v
inst✝³ : Field F
inst✝² : Field E
inst✝¹ : Algebra F E
inst✝ : Algebra.IsAlgebraic F E
⊢ Algebra.IsSeparable F ↥(separableClosure F E) ∧ IsPurelyInseparable (↥(separableClosure F E)) E
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/BitVec/Lemmas.lean
theorem getLsbD_shiftLeftZeroExtend (x : BitVec m) (n : Nat) :
    getLsbD (shiftLeftZeroExtend x n) i = ((! decide (i < n)) && getLsbD x (i - n))

Proof state:
case false.true.false.ge
m i : Nat
x : BitVec m
n : Nat
h₁ : n ≤ i
h₂ : i - n < m + n
h₃ : m + n ≤ i
⊢ m ≤ i - n

Tactic:
omega

Result:
no goals

Proof state:
m i : Nat
x : BitVec m
n : Nat
⊢ (decide (i < m + n) && !decide (i < n) && (decide (i - n < m + n) && x.getLsbD (i - n))) =
    (!decide (i < n) && x.getLsbD (i - n))

Tactic:
cases h₁ : decide (i < n) <;> cases h₂ : decide (i - n < m + n) <;> cases h₃ : decide (i < m + n)
  <;> simp_all
  <;> (rw [getLsbD_ge]; omega)

Result:
no goals

Proof state:
m i : Nat
x : BitVec m
n : Nat
⊢ (setWidth (m + n) x <<< n).getLsbD i = (!decide (i < n) && x.getLsbD (i - n))

Tactic:
simp only [getLsbD_shiftLeft, getLsbD_setWidth]

Result:
m i : Nat
x : BitVec m
n : Nat
⊢ (decide (i < m + n) && !decide (i < n) && (decide (i - n < m + n) && x.getLsbD (i - n))) =
    (!decide (i < n) && x.getLsbD (i - n))

Proof state:
case false.true.false
m i : Nat
x : BitVec m
n : Nat
h₁ : n ≤ i
h₂ : i - n < m + n
h₃ : m + n ≤ i
⊢ x.getLsbD (i - n) = false

Tactic:
rw [getLsbD_ge]

Result:
case false.true.false.ge
m i : Nat
x : BitVec m
n : Nat
h₁ : n ≤ i
h₂ : i - n < m + n
h₃ : m + n ≤ i
⊢ m ≤ i - n

Proof state:
m i : Nat
x : BitVec m
n : Nat
⊢ (x.shiftLeftZeroExtend n).getLsbD i = (!decide (i < n) && x.getLsbD (i - n))

Tactic:
rw [shiftLeftZeroExtend_eq]

Result:
m i : Nat
x : BitVec m
n : Nat
⊢ (setWidth (m + n) x <<< n).getLsbD i = (!decide (i < n) && x.getLsbD (i - n))
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Array/Lemmas.lean
theorem any_eq_false' {p : α → Bool} {as : Array α} :
    as.any p = false ↔ ∀ x, x ∈ as → ¬p x

Proof state:
α : Type u_1
p : α → Bool
as : Array α
⊢ as.any p = false ↔ ∀ (x : α), x ∈ as → ¬p x = true

Tactic:
rw [Bool.eq_false_iff, Ne, any_eq_true']

Result:
α : Type u_1
p : α → Bool
as : Array α
⊢ (¬∃ x, x ∈ as ∧ p x = true) ↔ ∀ (x : α), x ∈ as → ¬p x = true

Proof state:
α : Type u_1
p : α → Bool
as : Array α
⊢ (¬∃ x, x ∈ as ∧ p x = true) ↔ ∀ (x : α), x ∈ as → ¬p x = true

Tactic:
simp

Result:
no goals
-- Mathlib/Computability/PartrecCode.lean
theorem hG : Primrec G

Proof state:
case hpr
a : Primrec fun a => ofNat (ℕ × Code) a.length
k✝ : Primrec fun a => (ofNat (ℕ × Code) a.1.length).1
n✝ : Primrec Prod.snd
k : Primrec fun a => (ofNat (ℕ × Code) a.1.1.length).1
n : Primrec fun a => a.1.2
k' : Primrec Prod.snd
c : Primrec fun a => (ofNat (ℕ × Code) a.1.1.length).2
⊢ Primrec fun a => do
    let x ← Nat.Partrec.Code.lup a.1.1.1 ((ofNat (ℕ × Code) a.1.1.1.length).1, a.2.1) a.1.1.2
    let y ← Nat.Partrec.Code.lup a.1.1.1 ((ofNat (ℕ × Code) a.1.1.1.length).1, a.2.2.1) a.1.1.2
    some (Nat.pair x y)

Tactic:
have L := (Primrec.fst.comp Primrec.fst).comp
  (Primrec.fst (α := (List (List (Option ℕ)) × ℕ) × ℕ)
    (β := Code × Code × Option ℕ × Option ℕ))

Result:
case hpr
a : Primrec fun a => ofNat (ℕ × Code) a.length
k✝ : Primrec fun a => (ofNat (ℕ × Code) a.1.length).1
n✝ : Primrec Prod.snd
k : Primrec fun a => (ofNat (ℕ × Code) a.1.1.length).1
n : Primrec fun a => a.1.2
k' : Primrec Prod.snd
c : Primrec fun a => (ofNat (ℕ × Code) a.1.1.length).2
L : Primrec fun a => a.1.1.1
⊢ Primrec fun a => do
    let x ← Nat.Partrec.Code.lup a.1.1.1 ((ofNat (ℕ × Code) a.1.1.1.length).1, a.2.1) a.1.1.2
    let y ← Nat.Partrec.Code.lup a.1.1.1 ((ofNat (ℕ × Code) a.1.1.1.length).1, a.2.2.1) a.1.1.2
    some (Nat.pair x y)
-- Mathlib/Topology/Instances/EReal/Lemmas.lean
lemma nhdsWithin_bot : 𝓝[≠] (⊥ : EReal) = (atBot).map Real.toEReal

Proof state:
case h

⊢ ∀ (i : EReal), ⊥ < i → ∃ i', True ∧ Real.toEReal '' Iic i' ⊆ Iic i ∩ {⊥}ᶜ

Tactic:
simp only [EReal.image_coe_Iic, Set.subset_compl_singleton_iff, Set.mem_Ioc, lt_self_iff_false,
  bot_le, and_true, not_false_eq_true, true_and]

Result:
case h

⊢ ∀ (i : EReal), ⊥ < i → ∃ i', Ioc ⊥ ↑i' ⊆ Iic i ∩ {⊥}ᶜ

Proof state:
case h

⊢ ∀ (i : EReal), ⊥ < i → ∃ i', Ioc ⊥ ↑i' ⊆ Iic i ∩ {⊥}ᶜ

Tactic:
intro x hx

Result:
case h
x : EReal
hx : ⊥ < x
⊢ ∃ i', Ioc ⊥ ↑i' ⊆ Iic x ∩ {⊥}ᶜ

Proof state:
case pos
x : EReal
hx : ⊥ < x
hx_top : x = ⊤
⊢ ∃ i', Ioc ⊥ ↑i' ⊆ Iic x ∩ {⊥}ᶜ

Tactic:
simp [hx_top]

Result:
no goals

Proof state:
case h'

⊢ ∀ (i' : ℝ), ∃ i, ⊥ < i ∧ Iic i ∩ {⊥}ᶜ ⊆ Ioc ⊥ ↑i'

Tactic:
refine fun x ↦ ⟨x, ⟨EReal.bot_lt_coe x, fun x ⟨(h1 : x ≤ _), h2⟩ ↦ ?_⟩⟩

Result:
case h'
x✝¹ : ℝ
x : EReal
x✝ : x ∈ Iic ↑x✝¹ ∩ {⊥}ᶜ
h1 : x ≤ ↑x✝¹
h2 : x ∈ {⊥}ᶜ
⊢ x ∈ Ioc ⊥ ↑x✝¹

Proof state:
case h
x : EReal
hx : ⊥ < x
⊢ ∃ i', Ioc ⊥ ↑i' ⊆ Iic x ∩ {⊥}ᶜ

Tactic:
by_cases hx_top : x = ⊤

Result:
case pos
x : EReal
hx : ⊥ < x
hx_top : x = ⊤
⊢ ∃ i', Ioc ⊥ ↑i' ⊆ Iic x ∩ {⊥}ᶜ

case neg
x : EReal
hx : ⊥ < x
hx_top : ¬x = ⊤
⊢ ∃ i', Ioc ⊥ ↑i' ⊆ Iic x ∩ {⊥}ᶜ

Proof state:
case h'

⊢ ∀ (i' : ℝ), True → ∃ i, ⊥ < i ∧ Iic i ∩ {⊥}ᶜ ⊆ Real.toEReal '' Iic i'

Tactic:
simp only [EReal.image_coe_Iic, true_implies]

Result:
case h'

⊢ ∀ (i' : ℝ), ∃ i, ⊥ < i ∧ Iic i ∩ {⊥}ᶜ ⊆ Ioc ⊥ ↑i'

Proof state:
case neg
x : EReal
hx : ⊥ < x
hx_top : ¬x = ⊤
⊢ ∃ i', Ioc ⊥ ↑i' ⊆ Iic x ∩ {⊥}ᶜ

Tactic:
lift x to ℝ using ⟨hx_top, hx.ne_bot⟩

Result:
case neg.intro
x : ℝ
hx : ⊥ < ↑x
hx_top : ¬↑x = ⊤
⊢ ∃ i', Ioc ⊥ ↑i' ⊆ Iic ↑x ∩ {⊥}ᶜ

Proof state:
case neg.intro
x✝¹ : ℝ
hx : ⊥ < ↑x✝¹
hx_top : ¬↑x✝¹ = ⊤
x : EReal
x✝ : x ∈ Ioc ⊥ ↑x✝¹
h1 : ⊥ < x
h2 : x ≤ ↑x✝¹
⊢ x ∈ Iic ↑x✝¹ ∩ {⊥}ᶜ

Tactic:
simp [h2, h1.ne_bot]

Result:
no goals

Proof state:
⊢ 𝓝[≠] ⊥ = map Real.toEReal atBot

Tactic:
apply (nhdsWithin_hasBasis nhds_bot_basis_Iic _).ext (atBot_basis.map Real.toEReal)

Result:
case h

⊢ ∀ (i : EReal), ⊥ < i → ∃ i', True ∧ Real.toEReal '' Iic i' ⊆ Iic i ∩ {⊥}ᶜ

case h'

⊢ ∀ (i' : ℝ), True → ∃ i, ⊥ < i ∧ Iic i ∩ {⊥}ᶜ ⊆ Real.toEReal '' Iic i'

Proof state:
case h'
x✝¹ : ℝ
x : EReal
x✝ : x ∈ Iic ↑x✝¹ ∩ {⊥}ᶜ
h1 : x ≤ ↑x✝¹
h2 : x ∈ {⊥}ᶜ
⊢ x ∈ Ioc ⊥ ↑x✝¹

Tactic:
simp [h1, Ne.bot_lt' fun a ↦ h2 a.symm]

Result:
no goals

Proof state:
case neg.intro
x : ℝ
hx : ⊥ < ↑x
hx_top : ¬↑x = ⊤
⊢ ∃ i', Ioc ⊥ ↑i' ⊆ Iic ↑x ∩ {⊥}ᶜ

Tactic:
refine ⟨x, fun x ⟨h1, h2⟩ ↦ ?_⟩

Result:
case neg.intro
x✝¹ : ℝ
hx : ⊥ < ↑x✝¹
hx_top : ¬↑x✝¹ = ⊤
x : EReal
x✝ : x ∈ Ioc ⊥ ↑x✝¹
h1 : ⊥ < x
h2 : x ≤ ↑x✝¹
⊢ x ∈ Iic ↑x✝¹ ∩ {⊥}ᶜ
-- Mathlib/Geometry/Euclidean/Basic.lean
theorem eq_of_dist_eq_of_dist_eq_of_mem_of_finrank_eq_two {s : AffineSubspace ℝ P}
    [FiniteDimensional ℝ s.direction] (hd : finrank ℝ s.direction = 2) {c₁ c₂ p₁ p₂ p : P}
    (hc₁s : c₁ ∈ s) (hc₂s : c₂ ∈ s) (hp₁s : p₁ ∈ s) (hp₂s : p₂ ∈ s) (hps : p ∈ s) {r₁ r₂ : ℝ}
    (hc : c₁ ≠ c₂) (hp : p₁ ≠ p₂) (hp₁c₁ : dist p₁ c₁ = r₁) (hp₂c₁ : dist p₂ c₁ = r₁)
    (hpc₁ : dist p c₁ = r₁) (hp₁c₂ : dist p₁ c₂ = r₂) (hp₂c₂ : dist p₂ c₂ = r₂)
    (hpc₂ : dist p c₂ = r₂) : p = p₁ ∨ p = p₂

Proof state:
case refine_2.«1».«0»
V : Type u_1
P : Type u_2
inst✝⁴ : NormedAddCommGroup V
inst✝³ : InnerProductSpace ℝ V
inst✝² : MetricSpace P
inst✝¹ : NormedAddTorsor V P
s : AffineSubspace ℝ P
inst✝ : FiniteDimensional ℝ ↥s.direction
hd : finrank ℝ ↥s.direction = 2
c₁ c₂ p₁ p₂ p : P
hc₁s : c₁ ∈ s
hc₂s : c₂ ∈ s
hp₁s : p₁ ∈ s
hp₂s : p₂ ∈ s
hps : p ∈ s
r₁ r₂ : ℝ
hc : c₁ ≠ c₂
hp : p₁ ≠ p₂
hp₁c₁ : dist p₁ c₁ = r₁
hp₂c₁ : dist p₂ c₁ = r₁
hpc₁ : dist p c₁ = r₁
hp₁c₂ : dist p₁ c₂ = r₂
hp₂c₂ : dist p₂ c₂ = r₂
hpc₂ : dist p c₂ = r₂
ho : inner (c₂ -ᵥ c₁) (p₂ -ᵥ p₁) = 0
hop : inner (c₂ -ᵥ c₁) (p -ᵥ p₁) = 0
b : Fin 2 → V := ![c₂ -ᵥ c₁, p₂ -ᵥ p₁]
hij : (fun i => i) ⟨1, ⋯⟩ ≠ (fun i => i) ⟨0, ⋯⟩
⊢ inner (b ((fun i => i) ⟨1, ⋯⟩)) (b ((fun i => i) ⟨0, ⋯⟩)) = 0

Tactic:
rw [real_inner_comm]

Result:
case refine_2.«1».«0»
V : Type u_1
P : Type u_2
inst✝⁴ : NormedAddCommGroup V
inst✝³ : InnerProductSpace ℝ V
inst✝² : MetricSpace P
inst✝¹ : NormedAddTorsor V P
s : AffineSubspace ℝ P
inst✝ : FiniteDimensional ℝ ↥s.direction
hd : finrank ℝ ↥s.direction = 2
c₁ c₂ p₁ p₂ p : P
hc₁s : c₁ ∈ s
hc₂s : c₂ ∈ s
hp₁s : p₁ ∈ s
hp₂s : p₂ ∈ s
hps : p ∈ s
r₁ r₂ : ℝ
hc : c₁ ≠ c₂
hp : p₁ ≠ p₂
hp₁c₁ : dist p₁ c₁ = r₁
hp₂c₁ : dist p₂ c₁ = r₁
hpc₁ : dist p c₁ = r₁
hp₁c₂ : dist p₁ c₂ = r₂
hp₂c₂ : dist p₂ c₂ = r₂
hpc₂ : dist p c₂ = r₂
ho : inner (c₂ -ᵥ c₁) (p₂ -ᵥ p₁) = 0
hop : inner (c₂ -ᵥ c₁) (p -ᵥ p₁) = 0
b : Fin 2 → V := ![c₂ -ᵥ c₁, p₂ -ᵥ p₁]
hij : (fun i => i) ⟨1, ⋯⟩ ≠ (fun i => i) ⟨0, ⋯⟩
⊢ inner (b ((fun i => i) ⟨0, ⋯⟩)) (b ((fun i => i) ⟨1, ⋯⟩)) = 0

Proof state:
V : Type u_1
P : Type u_2
inst✝⁴ : NormedAddCommGroup V
inst✝³ : InnerProductSpace ℝ V
inst✝² : MetricSpace P
inst✝¹ : NormedAddTorsor V P
s : AffineSubspace ℝ P
inst✝ : FiniteDimensional ℝ ↥s.direction
hd : finrank ℝ ↥s.direction = 2
c₁ c₂ p₁ p₂ p : P
hc₁s : c₁ ∈ s
hc₂s : c₂ ∈ s
hp₁s : p₁ ∈ s
hp₂s : p₂ ∈ s
hps : p ∈ s
r₁ r₂ : ℝ
hc : c₁ ≠ c₂
hp : p₁ ≠ p₂
hp₁c₁ : dist p₁ c₁ = r₁
hp₂c₁ : dist p₂ c₁ = r₁
hpc₁ : dist p c₁ = r₁
hp₁c₂ : dist p₁ c₂ = r₂
hp₂c₂ : dist p₂ c₂ = r₂
hpc₂ : dist p c₂ = r₂
ho : inner (c₂ -ᵥ c₁) (p₂ -ᵥ p₁) = 0
hop : inner (c₂ -ᵥ c₁) (p -ᵥ p₁) = 0
b : Fin 2 → V := ![c₂ -ᵥ c₁, p₂ -ᵥ p₁]
hb : LinearIndependent ℝ b
hbs : Submodule.span ℝ (Set.range b) = s.direction
v : V
hv : v ∈ s.direction
hu : Finset.univ = {0, 1}
⊢ Set.range b = {c₂ -ᵥ c₁, p₂ -ᵥ p₁}

Tactic:
classical
rw [← Fintype.coe_image_univ, hu]
simp [b]

Result:
no goals