harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Vector/Lemmas.lean
theorem set_append {s : Vector α n} {t : Vector α m} {i : Nat} {x : α} (h : i < n + m) :
    (s ++ t).set i x =
      if h' : i < n then
        s.set i x ++ t
      else
        s ++ t.set (i - n) x

Proof state:
α : Type u_1
n m : Nat
s : Vector α n
t : Vector α m
i : Nat
x : α
h : i < n + m
⊢ (s ++ t).set i x h = if h' : i < n then s.set i x h' ++ t else s ++ t.set (i - n) x ⋯

Tactic:
rcases s with ⟨s, rfl⟩

Result:
case mk
α : Type u_1
m : Nat
t : Vector α m
i : Nat
x : α
s : Array α
h : i < s.size + m
⊢ ({ toArray := s, size_toArray := ⋯ } ++ t).set i x h =
    if h' : i < s.size then { toArray := s, size_toArray := ⋯ }.set i x h' ++ t
    else { toArray := s, size_toArray := ⋯ } ++ t.set (i - s.size) x ⋯

Proof state:
case mk
α : Type u_1
m : Nat
t : Vector α m
i : Nat
x : α
s : Array α
h : i < s.size + m
⊢ ({ toArray := s, size_toArray := ⋯ } ++ t).set i x h =
    if h' : i < s.size then { toArray := s, size_toArray := ⋯ }.set i x h' ++ t
    else { toArray := s, size_toArray := ⋯ } ++ t.set (i - s.size) x ⋯

Tactic:
rcases t with ⟨t, rfl⟩

Result:
case mk.mk
α : Type u_1
i : Nat
x : α
s t : Array α
h : i < s.size + t.size
⊢ ({ toArray := s, size_toArray := ⋯ } ++ { toArray := t, size_toArray := ⋯ }).set i x h =
    if h' : i < s.size then { toArray := s, size_toArray := ⋯ }.set i x h' ++ { toArray := t, size_toArray := ⋯ }
    else { toArray := s, size_toArray := ⋯ } ++ { toArray := t, size_toArray := ⋯ }.set (i - s.size) x ⋯

Proof state:
case mk.mk
α : Type u_1
i : Nat
x : α
s t : Array α
h : i < s.size + t.size
⊢ { toArray := if h' : i < s.size then s.set i x h' ++ t else s ++ t.set (i - s.size) x ⋯, size_toArray := ⋯ } =
    if h : i < s.size then { toArray := s.set i x ⋯ ++ t, size_toArray := ⋯ }
    else { toArray := s ++ t.set (i - s.size) x ⋯, size_toArray := ⋯ }

Tactic:
split <;> simp

Result:
no goals

Proof state:
case mk.mk
α : Type u_1
i : Nat
x : α
s t : Array α
h : i < s.size + t.size
⊢ ({ toArray := s, size_toArray := ⋯ } ++ { toArray := t, size_toArray := ⋯ }).set i x h =
    if h' : i < s.size then { toArray := s, size_toArray := ⋯ }.set i x h' ++ { toArray := t, size_toArray := ⋯ }
    else { toArray := s, size_toArray := ⋯ } ++ { toArray := t, size_toArray := ⋯ }.set (i - s.size) x ⋯

Tactic:
simp only [mk_append_mk, set_mk, Array.set_append]

Result:
case mk.mk
α : Type u_1
i : Nat
x : α
s t : Array α
h : i < s.size + t.size
⊢ { toArray := if h' : i < s.size then s.set i x h' ++ t else s ++ t.set (i - s.size) x ⋯, size_toArray := ⋯ } =
    if h : i < s.size then { toArray := s.set i x ⋯ ++ t, size_toArray := ⋯ }
    else { toArray := s ++ t.set (i - s.size) x ⋯, size_toArray := ⋯ }
-- Mathlib/LinearAlgebra/Matrix/Permanent.lean
theorem permanent_unique {n : Type*} [Unique n] [DecidableEq n] [Fintype n] (A : Matrix n n R) :
    permanent A = A default default

Proof state:
R : Type u_2
inst✝³ : CommSemiring R
n : Type u_3
inst✝² : Unique n
inst✝¹ : DecidableEq n
inst✝ : Fintype n
A : Matrix n n R
⊢ A.permanent = A default default

Tactic:
simp [permanent, univ_unique]

Result:
no goals
-- Mathlib/Analysis/Convex/Between.lean
theorem Collinear.wbtw_or_wbtw_or_wbtw {x y z : P} (h : Collinear R ({x, y, z} : Set P)) :
    Wbtw R x y z ∨ Wbtw R y z x ∨ Wbtw R z x y

Proof state:
case intro.intro.intro.inr.inr.inl
R : Type u_1
V : Type u_2
P : Type u_4
inst✝³ : LinearOrderedField R
inst✝² : AddCommGroup V
inst✝¹ : Module R V
inst✝ : AddTorsor V P
x : P
v : V
ty tz : R
h : ∀ (p : P), p = x ∨ p = ty • v +ᵥ x ∨ p = tz • v +ᵥ x → ∃ r, p = r • v +ᵥ x
hy0 : 0 < ty
hz0 : tz < 0
⊢ Wbtw R x (ty • v +ᵥ x) (tz • v +ᵥ x) ∨ Wbtw R (ty • v +ᵥ x) (tz • v +ᵥ x) x ∨ Wbtw R (tz • v +ᵥ x) x (ty • v +ᵥ x)

Tactic:
refine Or.inr (Or.inr (wbtw_smul_vadd_smul_vadd_of_nonpos_of_nonneg _ _ hz0.le hy0.le))

Result:
no goals

Proof state:
case intro.intro.intro.inl.inl
R : Type u_1
V : Type u_2
P : Type u_4
inst✝³ : LinearOrderedField R
inst✝² : AddCommGroup V
inst✝¹ : Module R V
inst✝ : AddTorsor V P
x : P
v : V
ty tz : R
h : ∀ (p : P), p = x ∨ p = ty • v +ᵥ x ∨ p = tz • v +ᵥ x → ∃ r, p = r • v +ᵥ x
hy0 : ty < 0
hz0 : tz < 0
⊢ (Wbtw R x (ty • v +ᵥ x) (tz • v +ᵥ x) ∨ Wbtw R x (tz • v +ᵥ x) (ty • v +ᵥ x)) ∨ Wbtw R (tz • v +ᵥ x) x (ty • v +ᵥ x)

Tactic:
exact Or.inl (wbtw_or_wbtw_smul_vadd_of_nonpos _ _ hy0.le hz0.le)

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/List/Attach.lean
theorem filterMap_subtype {p : α → Prop} {l : List { x // p x }}
    {f : { x // p x } → Option β} {g : α → Option β} (hf : ∀ x h, f ⟨x, h⟩ = g x) :
    l.filterMap f = l.unattach.filterMap g

Proof state:
case nil
α : Type u_1
β : Type u_2
p : α → Prop
f : { x // p x } → Option β
g : α → Option β
hf : ∀ (x : α) (h : p x), f ⟨x, h⟩ = g x
⊢ filterMap f [] = filterMap g (map (fun x => x.val) [])

Tactic:
simp

Result:
no goals

Proof state:
α : Type u_1
β : Type u_2
p : α → Prop
l : List { x // p x }
f : { x // p x } → Option β
g : α → Option β
hf : ∀ (x : α) (h : p x), f ⟨x, h⟩ = g x
⊢ filterMap f l = filterMap g (map (fun x => x.val) l)

Tactic:
induction l with
| nil => simp
| cons a l ih => simp [ih, hf, filterMap_cons]

Result:
no goals

Proof state:
case cons
α : Type u_1
β : Type u_2
p : α → Prop
f : { x // p x } → Option β
g : α → Option β
hf : ∀ (x : α) (h : p x), f ⟨x, h⟩ = g x
a : { x // p x }
l : List { x // p x }
ih : filterMap f l = filterMap g (map (fun x => x.val) l)
⊢ filterMap f (a :: l) = filterMap g (map (fun x => x.val) (a :: l))

Tactic:
simp [ih, hf, filterMap_cons]

Result:
no goals

Proof state:
α : Type u_1
β : Type u_2
p : α → Prop
l : List { x // p x }
f : { x // p x } → Option β
g : α → Option β
hf : ∀ (x : α) (h : p x), f ⟨x, h⟩ = g x
⊢ filterMap f l = filterMap g l.unattach

Tactic:
unfold unattach

Result:
α : Type u_1
β : Type u_2
p : α → Prop
l : List { x // p x }
f : { x // p x } → Option β
g : α → Option β
hf : ∀ (x : α) (h : p x), f ⟨x, h⟩ = g x
⊢ filterMap f l = filterMap g (map (fun x => x.val) l)
-- Mathlib/Algebra/ModEq.lean
theorem zsmul : a ≡ b [PMOD p] → z • a ≡ z • b [PMOD z • p] :=
  Exists.imp fun m hm => by rw [← smul_sub, hm, smul_comm]

Proof state:
α : Type u_1
inst✝ : AddCommGroup α
p a b : α
z m : ℤ
hm : b - a = m • p
⊢ z • b - z • a = m • z • p

Tactic:
rw [← smul_sub, hm, smul_comm]

Result:
no goals
-- Mathlib/Algebra/ContinuedFractions/Translations.lean
theorem zeroth_conv_eq_h : g.convs 0 = g.h

Proof state:
K : Type u_1
g : GenContFract K
inst✝ : DivisionRing K
⊢ g.convs 0 = g.h

Tactic:
simp [conv_eq_num_div_den, num_eq_conts_a, den_eq_conts_b, div_one]

Result:
no goals
-- Mathlib/Algebra/ModEq.lean
@[simp, norm_cast]
lemma intCast_modEq_intCast' {a b : ℤ} {n : ℕ} : a ≡ b [PMOD (n : α)] ↔ a ≡ b [PMOD (n : ℤ)]

Proof state:
α : Type u_1
inst✝¹ : AddCommGroupWithOne α
inst✝ : CharZero α
a b : ℤ
n : ℕ
⊢ ↑a ≡ ↑b [PMOD ↑n] ↔ a ≡ b [PMOD ↑n]

Tactic:
simpa using intCast_modEq_intCast (α := α) (z := n)

Result:
no goals
-- Mathlib/MeasureTheory/Function/LpSpace/Basic.lean
theorem indicatorConstLp_disjoint_union {s t : Set α} (hs : MeasurableSet s) (ht : MeasurableSet t)
    (hμs : μ s ≠ ∞) (hμt : μ t ≠ ∞) (hst : Disjoint s t) (c : E) :
    indicatorConstLp p (hs.union ht) (measure_union_ne_top hμs hμt) c =
      indicatorConstLp p hs hμs c + indicatorConstLp p ht hμt c

Proof state:
α : Type u_1
E : Type u_4
m0 : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
inst✝ : NormedAddCommGroup E
s t : Set α
hs : MeasurableSet s
ht : MeasurableSet t
hμs : μ s ≠ ⊤
hμt : μ t ≠ ⊤
hst : Disjoint s t
c : E
⊢ indicatorConstLp p ⋯ ⋯ c = indicatorConstLp p hs hμs c + indicatorConstLp p ht hμt c

Tactic:
ext1

Result:
case h
α : Type u_1
E : Type u_4
m0 : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
inst✝ : NormedAddCommGroup E
s t : Set α
hs : MeasurableSet s
ht : MeasurableSet t
hμs : μ s ≠ ⊤
hμt : μ t ≠ ⊤
hst : Disjoint s t
c : E
⊢ ↑↑(indicatorConstLp p ⋯ ⋯ c) =ᶠ[ae μ] ↑↑(indicatorConstLp p hs hμs c + indicatorConstLp p ht hμt c)

Proof state:
case h
α : Type u_1
E : Type u_4
m0 : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
inst✝ : NormedAddCommGroup E
s t : Set α
hs : MeasurableSet s
ht : MeasurableSet t
hμs : μ s ≠ ⊤
hμt : μ t ≠ ⊤
hst : Disjoint s t
c : E
⊢ ((s ∪ t).indicator fun x => c) =ᶠ[ae μ] fun x => s.indicator (fun x => c) x + t.indicator (fun x => c) x

Tactic:
rw [Set.indicator_union_of_disjoint hst]

Result:
no goals

Proof state:
case h
α : Type u_1
E : Type u_4
m0 : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
inst✝ : NormedAddCommGroup E
s t : Set α
hs : MeasurableSet s
ht : MeasurableSet t
hμs : μ s ≠ ⊤
hμt : μ t ≠ ⊤
hst : Disjoint s t
c : E
⊢ ((s ∪ t).indicator fun x => c) =ᶠ[ae μ] ↑↑(indicatorConstLp p hs hμs c) + ↑↑(indicatorConstLp p ht hμt c)

Tactic:
refine
  EventuallyEq.trans ?_
    (EventuallyEq.add indicatorConstLp_coeFn.symm indicatorConstLp_coeFn.symm)

Result:
case h
α : Type u_1
E : Type u_4
m0 : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
inst✝ : NormedAddCommGroup E
s t : Set α
hs : MeasurableSet s
ht : MeasurableSet t
hμs : μ s ≠ ⊤
hμt : μ t ≠ ⊤
hst : Disjoint s t
c : E
⊢ ((s ∪ t).indicator fun x => c) =ᶠ[ae μ] fun x => s.indicator (fun x => c) x + t.indicator (fun x => c) x

Proof state:
case h
α : Type u_1
E : Type u_4
m0 : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
inst✝ : NormedAddCommGroup E
s t : Set α
hs : MeasurableSet s
ht : MeasurableSet t
hμs : μ s ≠ ⊤
hμt : μ t ≠ ⊤
hst : Disjoint s t
c : E
⊢ ↑↑(indicatorConstLp p ⋯ ⋯ c) =ᶠ[ae μ] ↑↑(indicatorConstLp p hs hμs c + indicatorConstLp p ht hμt c)

Tactic:
refine indicatorConstLp_coeFn.trans (EventuallyEq.trans ?_ (Lp.coeFn_add _ _).symm)

Result:
case h
α : Type u_1
E : Type u_4
m0 : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
inst✝ : NormedAddCommGroup E
s t : Set α
hs : MeasurableSet s
ht : MeasurableSet t
hμs : μ s ≠ ⊤
hμt : μ t ≠ ⊤
hst : Disjoint s t
c : E
⊢ ((s ∪ t).indicator fun x => c) =ᶠ[ae μ] ↑↑(indicatorConstLp p hs hμs c) + ↑↑(indicatorConstLp p ht hμt c)
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/BitVec/Bitblast.lean
theorem getMsbD_sub {i : Nat} {i_lt : i < w} {x y : BitVec w} :
    (x - y).getMsbD i =
      (x.getMsbD i ^^ ((~~~y + 1).getMsbD i ^^ carry (w - 1 - i) x (~~~y + 1) false))

Proof state:
w i : Nat
i_lt : i < w
x y : BitVec w
⊢ (x.getMsbD i ^^ ((~~~y + 1#w).getMsbD i ^^ carry (w - 1 - i) x (~~~y + 1#w) false)) =
    (x.getMsbD i ^^ ((~~~y + 1).getMsbD i ^^ carry (w - 1 - i) x (~~~y + 1) false))

Tactic:
rfl

Result:
no goals

Proof state:
w i : Nat
i_lt : i < w
x y : BitVec w
⊢ (x - y).getMsbD i = (x.getMsbD i ^^ ((~~~y + 1).getMsbD i ^^ carry (w - 1 - i) x (~~~y + 1) false))

Tactic:
rw [sub_toAdd, neg_eq_not_add, getMsbD_add]

Result:
w i : Nat
i_lt : i < w
x y : BitVec w
⊢ (x.getMsbD i ^^ ((~~~y + 1#w).getMsbD i ^^ carry (w - 1 - i) x (~~~y + 1#w) false)) =
    (x.getMsbD i ^^ ((~~~y + 1).getMsbD i ^^ carry (w - 1 - i) x (~~~y + 1) false))

w i : Nat
i_lt : i < w
x y : BitVec w
⊢ i < w

Proof state:
w i : Nat
i_lt : i < w
x y : BitVec w
⊢ i < w

Tactic:
omega

Result:
no goals
-- Mathlib/NumberTheory/LegendreSymbol/GaussEisensteinLemmas.lean
theorem div_eq_filter_card {a b c : ℕ} (hb0 : 0 < b) (hc : a / b ≤ c) :
    a / b = #{x ∈ Ico 1 c.succ | x * b ≤ a} :=
  calc
    a / b = #(Ico 1 (a / b).succ)

Proof state:
a b c : ℕ
hb0 : 0 < b
hc : a / b ≤ c
⊢ a / b = #(Ico 1 (a / b).succ)

Tactic:
simp

Result:
no goals

Proof state:
a b c : ℕ
hb0 : 0 < b
hc : a / b ≤ c
x : ℕ
this : x * b ≤ a → x ≤ c
⊢ x * b ≤ a → 1 ≤ x → x ≤ c

Tactic:
tauto

Result:
no goals

Proof state:
a b c : ℕ
hb0 : 0 < b
hc : a / b ≤ c
x : ℕ
this : x * b ≤ a → x ≤ c
⊢ x ∈ Ico 1 (a / b).succ ↔ x ∈ filter (fun x => x * b ≤ a) (Ico 1 c.succ)

Tactic:
simp [Nat.lt_succ_iff, le_div_iff_mul_le hb0]

Result:
a b c : ℕ
hb0 : 0 < b
hc : a / b ≤ c
x : ℕ
this : x * b ≤ a → x ≤ c
⊢ x * b ≤ a → 1 ≤ x → x ≤ c

Proof state:
a b c : ℕ
hb0 : 0 < b
hc : a / b ≤ c
x : ℕ
h : x * b ≤ a
⊢ x ≤ a / b

Tactic:
rwa [le_div_iff_mul_le hb0]

Result:
no goals

Proof state:
a b c : ℕ
hb0 : 0 < b
hc : a / b ≤ c
x : ℕ
⊢ x ∈ Ico 1 (a / b).succ ↔ x ∈ filter (fun x => x * b ≤ a) (Ico 1 c.succ)

Tactic:
have : x * b ≤ a → x ≤ c := fun h => le_trans (by rwa [le_div_iff_mul_le hb0]) hc

Result:
a b c : ℕ
hb0 : 0 < b
hc : a / b ≤ c
x : ℕ
this : x * b ≤ a → x ≤ c
⊢ x ∈ Ico 1 (a / b).succ ↔ x ∈ filter (fun x => x * b ≤ a) (Ico 1 c.succ)
-- Mathlib/Topology/Connected/PathConnected.lean
theorem isPathConnected_iff_eq : IsPathConnected F ↔ ∃ x ∈ F, pathComponentIn x F = F

Proof state:
case right.h
X : Type u_1
inst✝ : TopologicalSpace X
F : Set X
x : X
x_in : x ∈ F
h : ∀ {y : X}, y ∈ F → JoinedIn F x y
y : X
⊢ y ∈ pathComponentIn x F ↔ y ∈ F

Tactic:
exact ⟨fun hy => hy.mem.2, h⟩

Result:
no goals

Proof state:
case right
X : Type u_1
inst✝ : TopologicalSpace X
F : Set X
x : X
x_in : x ∈ F
h : ∀ {y : X}, y ∈ F → JoinedIn F x y
⊢ pathComponentIn x F = F

Tactic:
ext y

Result:
case right.h
X : Type u_1
inst✝ : TopologicalSpace X
F : Set X
x : X
x_in : x ∈ F
h : ∀ {y : X}, y ∈ F → JoinedIn F x y
y : X
⊢ y ∈ pathComponentIn x F ↔ y ∈ F

Proof state:
X : Type u_1
inst✝ : TopologicalSpace X
F : Set X
⊢ IsPathConnected F ↔ ∃ x ∈ F, pathComponentIn x F = F

Tactic:
constructor <;> rintro ⟨x, x_in, h⟩ <;> use x, x_in

Result:
case right
X : Type u_1
inst✝ : TopologicalSpace X
F : Set X
x : X
x_in : x ∈ F
h : ∀ {y : X}, y ∈ F → JoinedIn F x y
⊢ pathComponentIn x F = F

case right
X : Type u_1
inst✝ : TopologicalSpace X
F : Set X
x : X
x_in : x ∈ F
h : pathComponentIn x F = F
⊢ ∀ {y : X}, y ∈ F → JoinedIn F x y

Proof state:
case right
X : Type u_1
inst✝ : TopologicalSpace X
F : Set X
x : X
x_in : x ∈ F
h : pathComponentIn x F = F
⊢ ∀ {y : X}, y ∈ F → JoinedIn F x y

Tactic:
intro y y_in

Result:
case right
X : Type u_1
inst✝ : TopologicalSpace X
F : Set X
x : X
x_in : x ∈ F
h : pathComponentIn x F = F
y : X
y_in : y ∈ F
⊢ JoinedIn F x y

Proof state:
case right
X : Type u_1
inst✝ : TopologicalSpace X
F : Set X
x : X
x_in : x ∈ F
h : pathComponentIn x F = F
y : X
y_in : y ∈ F
⊢ JoinedIn F x y

Tactic:
rwa [← h] at y_in

Result:
no goals
-- Mathlib/Order/Atoms.lean
theorem atom_le_iSup [Order.Frame α] {a : α} (ha : IsAtom a) {f : ι → α} :
    a ≤ iSup f ↔ ∃ i, a ≤ f i

Proof state:
ι : Sort u_1
α : Type u_2
inst✝ : Order.Frame α
f : ι → α
i : ι
x : α
hxf : x ≤ f i
hx : ¬x = ⊥
ha : IsAtom x
h : x ≤ ⨆ i, f i
ha' : ∀ (i : ι), ¬x ≤ f i
hxa : x ≤ x
⊢ False

Tactic:
exact ha' _ hxf

Result:
no goals

Proof state:
ι : Sort u_1
α : Type u_2
inst✝ : Order.Frame α
a : α
ha : IsAtom a
f : ι → α
⊢ a ≤ ⨆ i, f i → ∃ i, a ≤ f i

Tactic:
refine fun h => of_not_not fun ha' => ?_

Result:
ι : Sort u_1
α : Type u_2
inst✝ : Order.Frame α
a : α
ha : IsAtom a
f : ι → α
h : a ≤ ⨆ i, f i
ha' : ¬∃ i, a ≤ f i
⊢ False

Proof state:
ι : Sort u_1
α : Type u_2
inst✝ : Order.Frame α
a : α
ha : IsAtom a
f : ι → α
h : a ≤ ⨆ i, f i
ha' : ∀ (i : ι), ¬a ≤ f i
ha'' : Disjoint a (⨆ i, f i)
⊢ False

Tactic:
obtain rfl := le_bot_iff.1 (ha'' le_rfl h)

Result:
ι : Sort u_1
α : Type u_2
inst✝ : Order.Frame α
f : ι → α
ha : IsAtom ⊥
h : ⊥ ≤ ⨆ i, f i
ha' : ∀ (i : ι), ¬⊥ ≤ f i
ha'' : Disjoint ⊥ (⨆ i, f i)
⊢ False

Proof state:
ι : Sort u_1
α : Type u_2
inst✝ : Order.Frame α
a : α
ha : IsAtom a
f : ι → α
h : a ≤ ⨆ i, f i
ha' : ¬∃ i, a ≤ f i
⊢ False

Tactic:
push_neg at ha'

Result:
ι : Sort u_1
α : Type u_2
inst✝ : Order.Frame α
a : α
ha : IsAtom a
f : ι → α
h : a ≤ ⨆ i, f i
ha' : ∀ (i : ι), ¬a ≤ f i
⊢ False

Proof state:
ι : Sort u_1
α : Type u_2
inst✝ : Order.Frame α
a : α
ha : IsAtom a
f : ι → α
⊢ a ≤ iSup f → ∃ i, a ≤ f i

Tactic:
show (a ≤ ⨆ i, f i) → _

Result:
ι : Sort u_1
α : Type u_2
inst✝ : Order.Frame α
a : α
ha : IsAtom a
f : ι → α
⊢ a ≤ ⨆ i, f i → ∃ i, a ≤ f i

Proof state:
ι : Sort u_1
α : Type u_2
inst✝ : Order.Frame α
f : ι → α
ha : IsAtom ⊥
h : ⊥ ≤ ⨆ i, f i
ha' : ∀ (i : ι), ¬⊥ ≤ f i
ha'' : Disjoint ⊥ (⨆ i, f i)
⊢ False

Tactic:
exact ha.1 rfl

Result:
no goals

Proof state:
ι : Sort u_1
α : Type u_2
inst✝ : Order.Frame α
a : α
ha : IsAtom a
f : ι → α
⊢ a ≤ iSup f ↔ ∃ i, a ≤ f i

Tactic:
refine ⟨?_, fun ⟨i, hi⟩ => le_trans hi (le_iSup _ _)⟩

Result:
ι : Sort u_1
α : Type u_2
inst✝ : Order.Frame α
a : α
ha : IsAtom a
f : ι → α
⊢ a ≤ iSup f → ∃ i, a ≤ f i

Proof state:
ι : Sort u_1
α : Type u_2
inst✝ : Order.Frame α
a : α
ha : IsAtom a
f : ι → α
h : a ≤ ⨆ i, f i
ha' : ∀ (i : ι), ¬a ≤ f i
i : ι
x : α
hxa : x ≤ a
hxf : x ≤ f i
hx : ¬x = ⊥
⊢ ¬x = a

Tactic:
rintro rfl

Result:
ι : Sort u_1
α : Type u_2
inst✝ : Order.Frame α
f : ι → α
i : ι
x : α
hxf : x ≤ f i
hx : ¬x = ⊥
ha : IsAtom x
h : x ≤ ⨆ i, f i
ha' : ∀ (i : ι), ¬x ≤ f i
hxa : x ≤ x
⊢ False

Proof state:
ι : Sort u_1
α : Type u_2
inst✝ : Order.Frame α
a : α
ha : IsAtom a
f : ι → α
h : a ≤ ⨆ i, f i
ha' : ∀ (i : ι), ¬a ≤ f i
⊢ False

Tactic:
have ha'' : Disjoint a (⨆ i, f i) :=
  disjoint_iSup_iff.2 fun i => fun x hxa hxf => le_bot_iff.2 <| of_not_not fun hx =>
    have hxa : x < a := (le_iff_eq_or_lt.1 hxa).resolve_left (by rintro rfl; exact ha' _ hxf)
    hx (ha.2 _ hxa)

Result:
ι : Sort u_1
α : Type u_2
inst✝ : Order.Frame α
a : α
ha : IsAtom a
f : ι → α
h : a ≤ ⨆ i, f i
ha' : ∀ (i : ι), ¬a ≤ f i
ha'' : Disjoint a (⨆ i, f i)
⊢ False
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/List/BasicAux.lean
theorem append_cancel_left_eq (as bs cs : List α) : (as ++ bs = as ++ cs) = (bs = cs)

Proof state:
α : Type u_1
as bs cs : List α
⊢ (as ++ bs = as ++ cs) = (bs = cs)

Tactic:
apply propext

Result:
case a
α : Type u_1
as bs cs : List α
⊢ as ++ bs = as ++ cs ↔ bs = cs

Proof state:
case a.mp
α : Type u_1
as bs cs : List α
⊢ as ++ bs = as ++ cs → bs = cs

case a.mpr
α : Type u_1
as bs cs : List α
⊢ bs = cs → as ++ bs = as ++ cs

Tactic:
next => apply append_cancel_left

Result:
case a.mpr
α : Type u_1
as bs cs : List α
⊢ bs = cs → as ++ bs = as ++ cs

Proof state:
case a
α : Type u_1
as bs cs : List α
⊢ as ++ bs = as ++ cs ↔ bs = cs

Tactic:
apply Iff.intro

Result:
case a.mp
α : Type u_1
as bs cs : List α
⊢ as ++ bs = as ++ cs → bs = cs

case a.mpr
α : Type u_1
as bs cs : List α
⊢ bs = cs → as ++ bs = as ++ cs

Proof state:
case a.mpr
α : Type u_1
as bs cs : List α
⊢ bs = cs → as ++ bs = as ++ cs

Tactic:
next => intro h; simp [h]

Result:
no goals

Proof state:
α : Type u_1
as bs cs : List α
⊢ as ++ bs = as ++ cs → bs = cs

Tactic:
apply append_cancel_left

Result:
no goals

Proof state:
α : Type u_1
as bs cs : List α
⊢ bs = cs → as ++ bs = as ++ cs

Tactic:
intro h

Result:
α : Type u_1
as bs cs : List α
h : bs = cs
⊢ as ++ bs = as ++ cs

Proof state:
α : Type u_1
as bs cs : List α
h : bs = cs
⊢ as ++ bs = as ++ cs

Tactic:
simp [h]

Result:
no goals
-- Mathlib/Data/Int/ModEq.lean
theorem add_left_cancel (h₁ : a ≡ b [ZMOD n]) (h₂ : a + c ≡ b + d [ZMOD n]) :
    c ≡ d [ZMOD n] :=
  have : d - c = b + d - (a + c) - (b - a)

Proof state:
n a b c d : ℤ
h₁ : a ≡ b [ZMOD n]
h₂ : a + c ≡ b + d [ZMOD n]
this : d - c = b + d - (a + c) - (b - a)
⊢ n ∣ b + d - (a + c) - (b - a)

Tactic:
exact Int.dvd_sub h₂.dvd h₁.dvd

Result:
no goals

Proof state:
n a b c d : ℤ
h₁ : a ≡ b [ZMOD n]
h₂ : a + c ≡ b + d [ZMOD n]
this : d - c = b + d - (a + c) - (b - a)
⊢ n ∣ d - c

Tactic:
rw [this]

Result:
n a b c d : ℤ
h₁ : a ≡ b [ZMOD n]
h₂ : a + c ≡ b + d [ZMOD n]
this : d - c = b + d - (a + c) - (b - a)
⊢ n ∣ b + d - (a + c) - (b - a)

Proof state:
n a b c d : ℤ
h₁ : a ≡ b [ZMOD n]
h₂ : a + c ≡ b + d [ZMOD n]
⊢ d - c = b + d - (a + c) - (b - a)

Tactic:
omega

Result:
no goals
-- Mathlib/Algebra/Polynomial/Splits.lean
theorem splits_iff_card_roots {p : K[X]} :
    Splits (RingHom.id K) p ↔ Multiset.card p.roots = p.natDegree

Proof state:
case mp
K : Type v
inst✝ : Field K
p : K[X]
H : Splits (RingHom.id K) p
⊢ p.roots.card = p.natDegree

Tactic:
rw [natDegree_eq_card_roots H, map_id]

Result:
no goals

Proof state:
case h
K : Type v
inst✝ : Field K
p : K[X]
hroots : p.roots.card = p.natDegree
⊢ map (RingHom.id K) p = C ((RingHom.id K) p.leadingCoeff) * (Multiset.map (fun a => X - C a) p.roots).prod

Tactic:
simp only [RingHom.id_apply, map_id]

Result:
case h
K : Type v
inst✝ : Field K
p : K[X]
hroots : p.roots.card = p.natDegree
⊢ p = C p.leadingCoeff * (Multiset.map (fun a => X - C a) p.roots).prod

Proof state:
case mp
K : Type v
inst✝ : Field K
p : K[X]
⊢ Splits (RingHom.id K) p → p.roots.card = p.natDegree

Tactic:
intro H

Result:
case mp
K : Type v
inst✝ : Field K
p : K[X]
H : Splits (RingHom.id K) p
⊢ p.roots.card = p.natDegree

Proof state:
case mpr
K : Type v
inst✝ : Field K
p : K[X]
hroots : p.roots.card = p.natDegree
⊢ ∃ s, map (RingHom.id K) p = C ((RingHom.id K) p.leadingCoeff) * (Multiset.map (fun a => X - C a) s).prod

Tactic:
use p.roots

Result:
case h
K : Type v
inst✝ : Field K
p : K[X]
hroots : p.roots.card = p.natDegree
⊢ map (RingHom.id K) p = C ((RingHom.id K) p.leadingCoeff) * (Multiset.map (fun a => X - C a) p.roots).prod

Proof state:
case h
K : Type v
inst✝ : Field K
p : K[X]
hroots : p.roots.card = p.natDegree
⊢ p = C p.leadingCoeff * (Multiset.map (fun a => X - C a) p.roots).prod

Tactic:
exact (C_leadingCoeff_mul_prod_multiset_X_sub_C hroots).symm

Result:
no goals

Proof state:
case mpr
K : Type v
inst✝ : Field K
p : K[X]
⊢ p.roots.card = p.natDegree → Splits (RingHom.id K) p

Tactic:
intro hroots

Result:
case mpr
K : Type v
inst✝ : Field K
p : K[X]
hroots : p.roots.card = p.natDegree
⊢ Splits (RingHom.id K) p

Proof state:
case mpr
K : Type v
inst✝ : Field K
p : K[X]
hroots : p.roots.card = p.natDegree
⊢ Splits (RingHom.id K) p

Tactic:
rw [splits_iff_exists_multiset (RingHom.id K)]

Result:
case mpr
K : Type v
inst✝ : Field K
p : K[X]
hroots : p.roots.card = p.natDegree
⊢ ∃ s, map (RingHom.id K) p = C ((RingHom.id K) p.leadingCoeff) * (Multiset.map (fun a => X - C a) s).prod

Proof state:
K : Type v
inst✝ : Field K
p : K[X]
⊢ Splits (RingHom.id K) p ↔ p.roots.card = p.natDegree

Tactic:
constructor

Result:
case mp
K : Type v
inst✝ : Field K
p : K[X]
⊢ Splits (RingHom.id K) p → p.roots.card = p.natDegree

case mpr
K : Type v
inst✝ : Field K
p : K[X]
⊢ p.roots.card = p.natDegree → Splits (RingHom.id K) p
-- Mathlib/Logic/Relation.lean
theorem trans_induction_on {P : ∀ {a b : α}, ReflTransGen r a b → Prop} {a b : α}
    (h : ReflTransGen r a b) (ih₁ : ∀ a, @P a a refl) (ih₂ : ∀ {a b} (h : r a b), P (single h))
    (ih₃ : ∀ {a b c} (h₁ : ReflTransGen r a b) (h₂ : ReflTransGen r b c), P h₁ → P h₂ →
     P (h₁.trans h₂)) : P h

Proof state:
case refl
α : Type u_1
r : α → α → Prop
P : {a b : α} → ReflTransGen r a b → Prop
a b : α
ih₁ : ∀ (a : α), P ⋯
ih₂ : ∀ {a b : α} (h : r a b), P ⋯
ih₃ : ∀ {a b c : α} (h₁ : ReflTransGen r a b) (h₂ : ReflTransGen r b c), P h₁ → P h₂ → P ⋯
⊢ P ⋯

Tactic:
exact ih₁ a

Result:
no goals

Proof state:
case tail
α : Type u_1
r : α → α → Prop
P : {a b : α} → ReflTransGen r a b → Prop
a b : α
ih₁ : ∀ (a : α), P ⋯
ih₂ : ∀ {a b : α} (h : r a b), P ⋯
ih₃ : ∀ {a b c : α} (h₁ : ReflTransGen r a b) (h₂ : ReflTransGen r b c), P h₁ → P h₂ → P ⋯
b✝ c✝ : α
hab : ReflTransGen r a b✝
hbc : r b✝ c✝
ih : P hab
⊢ P ⋯

Tactic:
exact ih₃ hab (single hbc) ih (ih₂ hbc)

Result:
no goals

Proof state:
α : Type u_1
r : α → α → Prop
P : {a b : α} → ReflTransGen r a b → Prop
a b : α
h : ReflTransGen r a b
ih₁ : ∀ (a : α), P ⋯
ih₂ : ∀ {a b : α} (h : r a b), P ⋯
ih₃ : ∀ {a b c : α} (h₁ : ReflTransGen r a b) (h₂ : ReflTransGen r b c), P h₁ → P h₂ → P ⋯
⊢ P h

Tactic:
induction h with
| refl => exact ih₁ a
| tail hab hbc ih => exact ih₃ hab (single hbc) ih (ih₂ hbc)

Result:
no goals
-- Mathlib/Algebra/ContinuedFractions/Translations.lean
theorem partDen_eq_s_b {gp : Pair α} (s_nth_eq : g.s.get? n = some gp) :
    g.partDens.get? n = some gp.b

Proof state:
α : Type u_1
g : GenContFract α
n : ℕ
gp : Pair α
s_nth_eq : g.s.get? n = some gp
⊢ g.partDens.get? n = some gp.b

Tactic:
simp [partDens, s_nth_eq]

Result:
no goals