harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/Algebra/Homology/HomotopyCofiber.lean
lemma descSigma_ext_iff {φ : F ⟶ G} {K : HomologicalComplex C c}
    (x y : Σ (α : G ⟶ K), Homotopy (φ ≫ α) 0) :
    x = y ↔ x.1 = y.1 ∧ (∀ (i j : ι) (_ : c.Rel j i), x.2.hom i j = y.2.hom i j)

Proof state:
case mpr
C : Type u_1
inst✝² : Category.{u_3, u_1} C
inst✝¹ : Preadditive C
ι : Type u_2
c : ComplexShape ι
F G : HomologicalComplex C c
inst✝ : DecidableRel c.Rel
φ : F ⟶ G
K : HomologicalComplex C c
x y : (α : G ⟶ K) × Homotopy (φ ≫ α) 0
⊢ (x.fst = y.fst ∧ ∀ (i j : ι), c.Rel j i → x.snd.hom i j = y.snd.hom i j) → x = y

Tactic:
obtain ⟨x₁, x₂⟩ := x

Result:
case mpr.mk
C : Type u_1
inst✝² : Category.{u_3, u_1} C
inst✝¹ : Preadditive C
ι : Type u_2
c : ComplexShape ι
F G : HomologicalComplex C c
inst✝ : DecidableRel c.Rel
φ : F ⟶ G
K : HomologicalComplex C c
y : (α : G ⟶ K) × Homotopy (φ ≫ α) 0
x₁ : G ⟶ K
x₂ : Homotopy (φ ≫ x₁) 0
⊢ (⟨x₁, x₂⟩.fst = y.fst ∧ ∀ (i j : ι), c.Rel j i → ⟨x₁, x₂⟩.snd.hom i j = y.snd.hom i j) → ⟨x₁, x₂⟩ = y
-- Mathlib/Algebra/Polynomial/Monic.lean
theorem natDegree_mul' (hp : p.Monic) (hq : q ≠ 0) :
    (p * q).natDegree = p.natDegree + q.natDegree

Proof state:
R : Type u
inst✝ : Semiring R
p q : R[X]
hp : p.Monic
hq : q ≠ 0
⊢ (p * q).natDegree = p.natDegree + q.natDegree

Tactic:
rw [natDegree_mul']

Result:
R : Type u
inst✝ : Semiring R
p q : R[X]
hp : p.Monic
hq : q ≠ 0
⊢ p.leadingCoeff * q.leadingCoeff ≠ 0

Proof state:
R : Type u
inst✝ : Semiring R
p q : R[X]
hp : p.Monic
hq : q ≠ 0
⊢ p.leadingCoeff * q.leadingCoeff ≠ 0

Tactic:
simpa [hp.leadingCoeff, leadingCoeff_ne_zero]

Result:
no goals
-- Mathlib/Data/Nat/Lattice.lean
theorem not_mem_of_lt_sInf {s : Set ℕ} {m : ℕ} (hm : m < sInf s) : m ∉ s

Proof state:
case inr
s : Set ℕ
m : ℕ
hm : m < sInf s
h : s.Nonempty
⊢ m ∉ s

Tactic:
rw [Nat.sInf_def h] at hm

Result:
case inr
s : Set ℕ
m : ℕ
h : s.Nonempty
hm : m < Nat.find h
⊢ m ∉ s

Proof state:
s : Set ℕ
m : ℕ
hm : m < sInf s
⊢ m ∉ s

Tactic:
classical
cases eq_empty_or_nonempty s with
| inl h => subst h; apply not_mem_empty
| inr h => rw [Nat.sInf_def h] at hm; exact Nat.find_min h hm

Result:
no goals

Proof state:
case inl
m : ℕ
hm : m < sInf ∅
⊢ m ∉ ∅

Tactic:
apply not_mem_empty

Result:
no goals

Proof state:
case inl
s : Set ℕ
m : ℕ
hm : m < sInf s
h : s = ∅
⊢ m ∉ s

Tactic:
subst h

Result:
case inl
m : ℕ
hm : m < sInf ∅
⊢ m ∉ ∅

Proof state:
s : Set ℕ
m : ℕ
hm : m < sInf s
⊢ m ∉ s

Tactic:
cases eq_empty_or_nonempty s with
| inl h => subst h; apply not_mem_empty
| inr h => rw [Nat.sInf_def h] at hm; exact Nat.find_min h hm

Result:
no goals

Proof state:
case inr
s : Set ℕ
m : ℕ
h : s.Nonempty
hm : m < Nat.find h
⊢ m ∉ s

Tactic:
exact Nat.find_min h hm

Result:
no goals
-- Mathlib/Geometry/Euclidean/Angle/Unoriented/RightAngle.lean
theorem angle_sub_eq_arcsin_of_inner_eq_zero {x y : V} (h : ⟪x, y⟫ = 0) (h0 : x ≠ 0 ∨ y ≠ 0) :
    angle x (x - y) = Real.arcsin (‖y‖ / ‖x - y‖)

Proof state:
V : Type u_1
inst✝¹ : NormedAddCommGroup V
inst✝ : InnerProductSpace ℝ V
x y : V
h : inner x y = 0
h0 : x ≠ 0 ∨ y ≠ 0
⊢ angle x (x - y) = Real.arcsin (‖y‖ / ‖x - y‖)

Tactic:
rw [← neg_eq_zero, ← inner_neg_right] at h

Result:
V : Type u_1
inst✝¹ : NormedAddCommGroup V
inst✝ : InnerProductSpace ℝ V
x y : V
h : inner x (-y) = 0
h0 : x ≠ 0 ∨ y ≠ 0
⊢ angle x (x - y) = Real.arcsin (‖y‖ / ‖x - y‖)

Proof state:
V : Type u_1
inst✝¹ : NormedAddCommGroup V
inst✝ : InnerProductSpace ℝ V
x y : V
h : inner x (-y) = 0
h0 : x ≠ 0 ∨ -y ≠ 0
⊢ angle x (x - y) = Real.arcsin (‖y‖ / ‖x - y‖)

Tactic:
rw [sub_eq_add_neg, angle_add_eq_arcsin_of_inner_eq_zero h h0, norm_neg]

Result:
no goals

Proof state:
V : Type u_1
inst✝¹ : NormedAddCommGroup V
inst✝ : InnerProductSpace ℝ V
x y : V
h : inner x (-y) = 0
h0 : x ≠ 0 ∨ y ≠ 0
⊢ angle x (x - y) = Real.arcsin (‖y‖ / ‖x - y‖)

Tactic:
rw [or_comm, ← neg_ne_zero, or_comm] at h0

Result:
V : Type u_1
inst✝¹ : NormedAddCommGroup V
inst✝ : InnerProductSpace ℝ V
x y : V
h : inner x (-y) = 0
h0 : x ≠ 0 ∨ -y ≠ 0
⊢ angle x (x - y) = Real.arcsin (‖y‖ / ‖x - y‖)
-- Mathlib/Data/Multiset/Powerset.lean
theorem mem_powersetCardAux {n} {l : List α} {s} : s ∈ powersetCardAux n l ↔ s ≤ ↑l ∧ card s = n :=
  Quotient.inductionOn s <| by
    simp only [quot_mk_to_coe, powersetCardAux_eq_map_coe, List.mem_map, mem_sublistsLen,
      coe_eq_coe, coe_le, Subperm, exists_prop, coe_card]
    exact fun l₁ =>
      ⟨fun ⟨l₂, ⟨s, e⟩, p⟩ => ⟨⟨_, p, s⟩, p.symm.length_eq.trans e⟩,
       fun ⟨⟨l₂, p, s⟩, e⟩ => ⟨_, ⟨s, p.length_eq.trans e⟩, p⟩⟩

Proof state:
α : Type u_1
n : ℕ
l : List α
s : Multiset α
⊢ ∀ (a : List α), ⟦a⟧ ∈ powersetCardAux n l ↔ ⟦a⟧ ≤ ↑l ∧ card ⟦a⟧ = n

Tactic:
simp only [quot_mk_to_coe, powersetCardAux_eq_map_coe, List.mem_map, mem_sublistsLen,
  coe_eq_coe, coe_le, Subperm, exists_prop, coe_card]

Result:
α : Type u_1
n : ℕ
l : List α
s : Multiset α
⊢ ∀ (a : List α), (∃ a_1, (a_1 <+ l ∧ a_1.length = n) ∧ a_1 ~ a) ↔ (∃ l_1, l_1 ~ a ∧ l_1 <+ l) ∧ a.length = n

Proof state:
α : Type u_1
n : ℕ
l : List α
s : Multiset α
⊢ ∀ (a : List α), (∃ a_1, (a_1 <+ l ∧ a_1.length = n) ∧ a_1 ~ a) ↔ (∃ l_1, l_1 ~ a ∧ l_1 <+ l) ∧ a.length = n

Tactic:
exact fun l₁ =>
  ⟨fun ⟨l₂, ⟨s, e⟩, p⟩ => ⟨⟨_, p, s⟩, p.symm.length_eq.trans e⟩,
   fun ⟨⟨l₂, p, s⟩, e⟩ => ⟨_, ⟨s, p.length_eq.trans e⟩, p⟩⟩

Result:
no goals
-- Mathlib/Data/Nat/Init.lean
lemma div_eq_sub_mod_div : m / n = (m - m % n) / n

Proof state:
case inr
m n : ℕ
hn : n > 0
this : m - m % n = n * (m / n)
⊢ m / n = (m - m % n) / n

Tactic:
rw [this, mul_div_right _ hn]

Result:
no goals

Proof state:
case inr
m n : ℕ
hn : n > 0
⊢ m / n = (m - m % n) / n

Tactic:
have : m - m % n = n * (m / n) := by
  rw [Nat.sub_eq_iff_eq_add (Nat.mod_le _ _), Nat.add_comm, mod_add_div]

Result:
case inr
m n : ℕ
hn : n > 0
this : m - m % n = n * (m / n)
⊢ m / n = (m - m % n) / n

Proof state:
case inl
m : ℕ
⊢ m / 0 = (m - m % 0) / 0

Tactic:
rw [Nat.div_zero, Nat.div_zero]

Result:
no goals

Proof state:
m n : ℕ
hn : n > 0
⊢ m - m % n = n * (m / n)

Tactic:
rw [Nat.sub_eq_iff_eq_add (Nat.mod_le _ _), Nat.add_comm, mod_add_div]

Result:
no goals

Proof state:
m n : ℕ
⊢ m / n = (m - m % n) / n

Tactic:
obtain rfl | hn := n.eq_zero_or_pos

Result:
case inl
m : ℕ
⊢ m / 0 = (m - m % 0) / 0

case inr
m n : ℕ
hn : n > 0
⊢ m / n = (m - m % n) / n
-- Mathlib/Data/PFunctor/Univariate/M.lean
theorem iselect_eq_default [DecidableEq F.A] [Inhabited (M F)] (ps : Path F) (x : M F)
    (h : ¬IsPath ps x) : iselect ps x = head default

Proof state:
case pos.h.a
F : PFunctor.{u}
inst✝¹ : DecidableEq F.A
inst✝ : Inhabited F.M
ps_tail : List F.Idx
ps_ih : ∀ (x : F.M), ¬IsPath ps_tail x → (isubtree ps_tail x).head = default.head
a : F.A
i : F.B a
x_f : F.B a → F.M
h : ¬IsPath (⟨a, i⟩ :: ps_tail) (M.mk ⟨a, x_f⟩)
h' : IsPath ps_tail (x_f (cast ⋯ i))
⊢ IsPath ps_tail (x_f i)

Tactic:
apply h'

Result:
no goals

Proof state:
case pos
F : PFunctor.{u}
inst✝¹ : DecidableEq F.A
inst✝ : Inhabited F.M
ps_tail : List F.Idx
ps_ih : ∀ (x : F.M), ¬IsPath ps_tail x → (isubtree ps_tail x).head = default.head
a : F.A
i : F.B a
x_f : F.B a → F.M
h : ¬IsPath (⟨a, i⟩ :: ps_tail) (M.mk ⟨a, x_f⟩)
⊢ ((M.mk ⟨a, x_f⟩).casesOn' fun a' f => if h : a = a' then isubtree ps_tail (f (cast ⋯ i)) else default).head =
    default.head

Tactic:
simp only [dif_pos, eq_self_iff_true, casesOn_mk']

Result:
case pos
F : PFunctor.{u}
inst✝¹ : DecidableEq F.A
inst✝ : Inhabited F.M
ps_tail : List F.Idx
ps_ih : ∀ (x : F.M), ¬IsPath ps_tail x → (isubtree ps_tail x).head = default.head
a : F.A
i : F.B a
x_f : F.B a → F.M
h : ¬IsPath (⟨a, i⟩ :: ps_tail) (M.mk ⟨a, x_f⟩)
⊢ (isubtree ps_tail (x_f (cast ⋯ i))).head = default.head

Proof state:
case cons.mk
F : PFunctor.{u}
inst✝¹ : DecidableEq F.A
inst✝ : Inhabited F.M
ps_tail : List F.Idx
ps_ih : ∀ (x : F.M), ¬IsPath ps_tail x → iselect ps_tail x = default.head
x : F.M
a : F.A
i : F.B a
h : ¬IsPath (⟨a, i⟩ :: ps_tail) x
⊢ iselect (⟨a, i⟩ :: ps_tail) x = default.head

Tactic:
induction' x using PFunctor.M.casesOn' with x_a x_f

Result:
case cons.mk.f
F : PFunctor.{u}
inst✝¹ : DecidableEq F.A
inst✝ : Inhabited F.M
ps_tail : List F.Idx
ps_ih : ∀ (x : F.M), ¬IsPath ps_tail x → iselect ps_tail x = default.head
a : F.A
i : F.B a
x_a : F.A
x_f : F.B x_a → F.M
h : ¬IsPath (⟨a, i⟩ :: ps_tail) (M.mk ⟨x_a, x_f⟩)
⊢ iselect (⟨a, i⟩ :: ps_tail) (M.mk ⟨x_a, x_f⟩) = default.head

Proof state:
case nil
F : PFunctor.{u}
inst✝¹ : DecidableEq F.A
inst✝ : Inhabited F.M
x : F.M
h : ¬IsPath [] x
⊢ iselect [] x = default.head

Tactic:
exfalso

Result:
case nil
F : PFunctor.{u}
inst✝¹ : DecidableEq F.A
inst✝ : Inhabited F.M
x : F.M
h : ¬IsPath [] x
⊢ False

Proof state:
case pos.h
F : PFunctor.{u}
inst✝¹ : DecidableEq F.A
inst✝ : Inhabited F.M
ps_tail : List F.Idx
ps_ih : ∀ (x : F.M), ¬IsPath ps_tail x → (isubtree ps_tail x).head = default.head
a : F.A
i : F.B a
x_f : F.B a → F.M
h : ¬IsPath (⟨a, i⟩ :: ps_tail) (M.mk ⟨a, x_f⟩)
⊢ ¬IsPath ps_tail (x_f (cast ⋯ i))

Tactic:
intro h'

Result:
case pos.h
F : PFunctor.{u}
inst✝¹ : DecidableEq F.A
inst✝ : Inhabited F.M
ps_tail : List F.Idx
ps_ih : ∀ (x : F.M), ¬IsPath ps_tail x → (isubtree ps_tail x).head = default.head
a : F.A
i : F.B a
x_f : F.B a → F.M
h : ¬IsPath (⟨a, i⟩ :: ps_tail) (M.mk ⟨a, x_f⟩)
h' : IsPath ps_tail (x_f (cast ⋯ i))
⊢ False
-- Mathlib/Probability/BorelCantelli.lean
theorem measure_limsup_eq_one {s : ℕ → Set Ω} (hsm : ∀ n, MeasurableSet (s n)) (hs : iIndepSet s μ)
    (hs' : (∑' n, μ (s n)) = ∞) : μ (limsup s atTop) = 1

Proof state:
Ω : Type u_1
m0 : MeasurableSpace Ω
μ : Measure Ω
s : ℕ → Set Ω
hsm : ∀ (n : ℕ), MeasurableSet (s n)
hs : iIndepSet s μ
hs' : ∑' (n : ℕ), μ (s n) = ⊤
this : IsProbabilityMeasure μ
⊢ μ {ω | Tendsto (fun n => ∑ k ∈ Finset.range n, (μ[(s (k + 1)).indicator 1|↑(filtrationOfSet hsm) k]) ω) atTop atTop} =
    1

Tactic:
suffices {ω | Tendsto (fun n => ∑ k ∈ Finset.range n,
    (μ[(s (k + 1)).indicator (1 : Ω → ℝ)|filtrationOfSet hsm k]) ω) atTop atTop} =ᵐ[μ] Set.univ by
  rw [measure_congr this, measure_univ]

Result:
Ω : Type u_1
m0 : MeasurableSpace Ω
μ : Measure Ω
s : ℕ → Set Ω
hsm : ∀ (n : ℕ), MeasurableSet (s n)
hs : iIndepSet s μ
hs' : ∑' (n : ℕ), μ (s n) = ⊤
this : IsProbabilityMeasure μ
⊢ {ω |
      Tendsto (fun n => ∑ k ∈ Finset.range n, (μ[(s (k + 1)).indicator 1|↑(filtrationOfSet hsm) k]) ω) atTop
        atTop} =ᶠ[ae μ]
    Set.univ
-- Mathlib/Data/Real/Archimedean.lean
theorem exists_isGLB (hne : s.Nonempty) (hbdd : BddBelow s) : ∃ x, IsGLB s x

Proof state:
s : Set ℝ
hne : s.Nonempty
hbdd : BddBelow s
hne' : (-s).Nonempty
hbdd' : BddAbove (-s)
⊢ ∃ x, IsGLB s x

Tactic:
use -Classical.choose (Real.exists_isLUB hne' hbdd')

Result:
case h
s : Set ℝ
hne : s.Nonempty
hbdd : BddBelow s
hne' : (-s).Nonempty
hbdd' : BddAbove (-s)
⊢ IsGLB s (-Classical.choose ⋯)

Proof state:
s : Set ℝ
hne : s.Nonempty
hbdd : BddBelow s
⊢ ∃ x, IsGLB s x

Tactic:
have hne' : (-s).Nonempty := Set.nonempty_neg.mpr hne

Result:
s : Set ℝ
hne : s.Nonempty
hbdd : BddBelow s
hne' : (-s).Nonempty
⊢ ∃ x, IsGLB s x

Proof state:
case h
s : Set ℝ
hne : s.Nonempty
hbdd : BddBelow s
hne' : (-s).Nonempty
hbdd' : BddAbove (-s)
⊢ IsGLB s (-Classical.choose ⋯)

Tactic:
rw [← isLUB_neg]

Result:
case h
s : Set ℝ
hne : s.Nonempty
hbdd : BddBelow s
hne' : (-s).Nonempty
hbdd' : BddAbove (-s)
⊢ IsLUB (-s) (Classical.choose ⋯)

Proof state:
case h
s : Set ℝ
hne : s.Nonempty
hbdd : BddBelow s
hne' : (-s).Nonempty
hbdd' : BddAbove (-s)
⊢ IsLUB (-s) (Classical.choose ⋯)

Tactic:
exact Classical.choose_spec (Real.exists_isLUB hne' hbdd')

Result:
no goals

Proof state:
s : Set ℝ
hne : s.Nonempty
hbdd : BddBelow s
hne' : (-s).Nonempty
⊢ ∃ x, IsGLB s x

Tactic:
have hbdd' : BddAbove (-s) := bddAbove_neg.mpr hbdd

Result:
s : Set ℝ
hne : s.Nonempty
hbdd : BddBelow s
hne' : (-s).Nonempty
hbdd' : BddAbove (-s)
⊢ ∃ x, IsGLB s x
-- Mathlib/LinearAlgebra/Matrix/Determinant/Basic.lean
theorem det_updateCol_eq_zero (h : i ≠ j) :
    (M.updateCol j (fun k ↦ M k i)).det = 0 := det_zero_of_column_eq h (by simp [h])

Proof state:
n : Type u_2
inst✝² : DecidableEq n
inst✝¹ : Fintype n
R : Type v
inst✝ : CommRing R
M : Matrix n n R
i j : n
h : i ≠ j
⊢ ∀ (k : n), M.updateCol j (fun k => M k i) k i = M.updateCol j (fun k => M k i) k j

Tactic:
simp [h]

Result:
no goals
-- Mathlib/Geometry/RingedSpace/Basic.lean
theorem isUnit_res_basicOpen {U : Opens X} (f : X.presheaf.obj (op U)) :
    IsUnit (X.presheaf.map (@homOfLE (Opens X) _ _ _ (X.basicOpen_le f)).op f)

Proof state:
case h
X : RingedSpace
U : Opens ↑↑X.toPresheafedSpace
f : ↑(X.presheaf.obj (op U))
⊢ ∀ (x : ↑↑X.toPresheafedSpace) (hx : x ∈ X.basicOpen f),
    IsUnit
      ((ConcreteCategory.hom (X.presheaf.germ (X.basicOpen f) x hx))
        ((ConcreteCategory.hom (X.presheaf.map (homOfLE ⋯).op)) f))

Tactic:
rintro x ⟨hxU, hx⟩

Result:
case h.intro
X : RingedSpace
U : Opens ↑↑X.toPresheafedSpace
f : ↑(X.presheaf.obj (op U))
x : ↑↑X.toPresheafedSpace
hxU : x ∈ U
hx : IsUnit ((ConcreteCategory.hom (X.presheaf.germ U x hxU)) f)
⊢ IsUnit
    ((ConcreteCategory.hom (X.presheaf.germ (X.basicOpen f) x ⋯))
      ((ConcreteCategory.hom (X.presheaf.map (homOfLE ⋯).op)) f))

Proof state:
case h.e'_3
X : RingedSpace
U : Opens ↑↑X.toPresheafedSpace
f : ↑(X.presheaf.obj (op U))
x : ↑↑X.toPresheafedSpace
hxU : x ∈ U
hx : IsUnit ((ConcreteCategory.hom (X.presheaf.germ U x hxU)) f)
⊢ (ConcreteCategory.hom (X.presheaf.germ (X.basicOpen f) x ⋯))
      ((ConcreteCategory.hom (X.presheaf.map (homOfLE ⋯).op)) f) =
    (ConcreteCategory.hom (X.presheaf.germ U x hxU)) f

Tactic:
exact X.presheaf.germ_res_apply _ _ _ _

Result:
no goals

Proof state:
X : RingedSpace
U : Opens ↑↑X.toPresheafedSpace
f : ↑(X.presheaf.obj (op U))
⊢ IsUnit ((ConcreteCategory.hom (X.presheaf.map (homOfLE ⋯).op)) f)

Tactic:
apply isUnit_of_isUnit_germ

Result:
case h
X : RingedSpace
U : Opens ↑↑X.toPresheafedSpace
f : ↑(X.presheaf.obj (op U))
⊢ ∀ (x : ↑↑X.toPresheafedSpace) (hx : x ∈ X.basicOpen f),
    IsUnit
      ((ConcreteCategory.hom (X.presheaf.germ (X.basicOpen f) x hx))
        ((ConcreteCategory.hom (X.presheaf.map (homOfLE ⋯).op)) f))

Proof state:
case h.intro
X : RingedSpace
U : Opens ↑↑X.toPresheafedSpace
f : ↑(X.presheaf.obj (op U))
x : ↑↑X.toPresheafedSpace
hxU : x ∈ U
hx : IsUnit ((ConcreteCategory.hom (X.presheaf.germ U x hxU)) f)
⊢ IsUnit
    ((ConcreteCategory.hom (X.presheaf.germ (X.basicOpen f) x ⋯))
      ((ConcreteCategory.hom (X.presheaf.map (homOfLE ⋯).op)) f))

Tactic:
convert hx

Result:
case h.e'_3
X : RingedSpace
U : Opens ↑↑X.toPresheafedSpace
f : ↑(X.presheaf.obj (op U))
x : ↑↑X.toPresheafedSpace
hxU : x ∈ U
hx : IsUnit ((ConcreteCategory.hom (X.presheaf.germ U x hxU)) f)
⊢ (ConcreteCategory.hom (X.presheaf.germ (X.basicOpen f) x ⋯))
      ((ConcreteCategory.hom (X.presheaf.map (homOfLE ⋯).op)) f) =
    (ConcreteCategory.hom (X.presheaf.germ U x hxU)) f
-- Mathlib/Data/Finset/Basic.lean
@[simp]
lemma toFinset_replicate (n : ℕ) (a : α) :
    (replicate n a).toFinset = if n = 0 then ∅ else {a}

Proof state:
case h
α : Type u_1
inst✝ : DecidableEq α
n : ℕ
a x : α
⊢ x ∈ (replicate n a).toFinset ↔ x ∈ if n = 0 then ∅ else {a}

Tactic:
simp only [mem_toFinset, Finset.mem_singleton, mem_replicate]

Result:
case h
α : Type u_1
inst✝ : DecidableEq α
n : ℕ
a x : α
⊢ n ≠ 0 ∧ x = a ↔ x ∈ if n = 0 then ∅ else {a}

Proof state:
case h
α : Type u_1
inst✝ : DecidableEq α
n : ℕ
a x : α
⊢ n ≠ 0 ∧ x = a ↔ x ∈ if n = 0 then ∅ else {a}

Tactic:
split_ifs with hn <;> simp [hn]

Result:
no goals

Proof state:
α : Type u_1
inst✝ : DecidableEq α
n : ℕ
a : α
⊢ (replicate n a).toFinset = if n = 0 then ∅ else {a}

Tactic:
ext x

Result:
case h
α : Type u_1
inst✝ : DecidableEq α
n : ℕ
a x : α
⊢ x ∈ (replicate n a).toFinset ↔ x ∈ if n = 0 then ∅ else {a}
-- Mathlib/Geometry/Euclidean/Angle/Unoriented/RightAngle.lean
theorem sin_angle_add_of_inner_eq_zero {x y : V} (h : ⟪x, y⟫ = 0) (h0 : x ≠ 0 ∨ y ≠ 0) :
    Real.sin (angle x (x + y)) = ‖y‖ / ‖x + y‖

Proof state:
V : Type u_1
inst✝¹ : NormedAddCommGroup V
inst✝ : InnerProductSpace ℝ V
x y : V
h : inner x y = 0
h0 : x ≠ 0 ∨ y ≠ 0
⊢ -1 ≤ 0

Tactic:
norm_num

Result:
no goals

Proof state:
V : Type u_1
inst✝¹ : NormedAddCommGroup V
inst✝ : InnerProductSpace ℝ V
x y : V
h : inner x y = 0
h0 : x ≠ 0 ∨ y ≠ 0
⊢ ‖y‖ ≤ ‖x + y‖

Tactic:
rw [mul_self_le_mul_self_iff (norm_nonneg _) (norm_nonneg _),
  norm_add_sq_eq_norm_sq_add_norm_sq_real h]

Result:
V : Type u_1
inst✝¹ : NormedAddCommGroup V
inst✝ : InnerProductSpace ℝ V
x y : V
h : inner x y = 0
h0 : x ≠ 0 ∨ y ≠ 0
⊢ ‖y‖ * ‖y‖ ≤ ‖x‖ * ‖x‖ + ‖y‖ * ‖y‖

Proof state:
V : Type u_1
inst✝¹ : NormedAddCommGroup V
inst✝ : InnerProductSpace ℝ V
x y : V
h : inner x y = 0
h0 : x ≠ 0 ∨ y ≠ 0
⊢ ‖y‖ * ‖y‖ ≤ ‖x‖ * ‖x‖ + ‖y‖ * ‖y‖

Tactic:
exact le_add_of_nonneg_left (mul_self_nonneg _)

Result:
no goals

Proof state:
V : Type u_1
inst✝¹ : NormedAddCommGroup V
inst✝ : InnerProductSpace ℝ V
x y : V
h : inner x y = 0
h0 : x ≠ 0 ∨ y ≠ 0
⊢ Real.sin (angle x (x + y)) = ‖y‖ / ‖x + y‖

Tactic:
rw [angle_add_eq_arcsin_of_inner_eq_zero h h0,
  Real.sin_arcsin (le_trans (by norm_num) (div_nonneg (norm_nonneg _) (norm_nonneg _)))
    (div_le_one_of_le₀ _ (norm_nonneg _))]

Result:
V : Type u_1
inst✝¹ : NormedAddCommGroup V
inst✝ : InnerProductSpace ℝ V
x y : V
h : inner x y = 0
h0 : x ≠ 0 ∨ y ≠ 0
⊢ ‖y‖ ≤ ‖x + y‖
-- Mathlib/MeasureTheory/Integral/SetToL1.lean
theorem setToSimpleFunc_add (T : Set α → E →L[ℝ] F) (h_add : FinMeasAdditive μ T) {f g : α →ₛ E}
    (hf : Integrable f μ) (hg : Integrable g μ) :
    setToSimpleFunc T (f + g) = setToSimpleFunc T f + setToSimpleFunc T g :=
  have hp_pair : Integrable (f.pair g) μ := integrable_pair hf hg
  calc
    setToSimpleFunc T (f + g) = ∑ x ∈ (pair f g).range, T (pair f g ⁻¹' {x}) (x.fst + x.snd)

Proof state:
α : Type u_1
E : Type u_2
F : Type u_3
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
m : MeasurableSpace α
μ : Measure α
T : Set α → E →L[ℝ] F
h_add : FinMeasAdditive μ T
f g : α →ₛ E
hf : Integrable (⇑f) μ
hg : Integrable (⇑g) μ
hp_pair : Integrable (⇑(f.pair g)) μ
⊢ 0.1 + 0.2 = 0

Tactic:
simp

Result:
no goals

Proof state:
α : Type u_1
E : Type u_2
F : Type u_3
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
m : MeasurableSpace α
μ : Measure α
T : Set α → E →L[ℝ] F
h_add : FinMeasAdditive μ T
f g : α →ₛ E
hf : Integrable (⇑f) μ
hg : Integrable (⇑g) μ
hp_pair : Integrable (⇑(f.pair g)) μ
⊢ setToSimpleFunc T (f + g) = ∑ x ∈ (f.pair g).range, (T (⇑(f.pair g) ⁻¹' {x})) (x.1 + x.2)

Tactic:
rw [add_eq_map₂, map_setToSimpleFunc T h_add hp_pair]

Result:
α : Type u_1
E : Type u_2
F : Type u_3
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
m : MeasurableSpace α
μ : Measure α
T : Set α → E →L[ℝ] F
h_add : FinMeasAdditive μ T
f g : α →ₛ E
hf : Integrable (⇑f) μ
hg : Integrable (⇑g) μ
hp_pair : Integrable (⇑(f.pair g)) μ
⊢ 0.1 + 0.2 = 0

Proof state:
α : Type u_1
E : Type u_2
F : Type u_3
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
m : MeasurableSpace α
μ : Measure α
T : Set α → E →L[ℝ] F
h_add : FinMeasAdditive μ T
f g : α →ₛ E
hf : Integrable (⇑f) μ
hg : Integrable (⇑g) μ
hp_pair : Integrable (⇑(f.pair g)) μ
⊢ ∑ x ∈ (f.pair g).range, ((T (⇑(f.pair g) ⁻¹' {x})) x.1 + (T (⇑(f.pair g) ⁻¹' {x})) x.2) =
    ∑ x ∈ (f.pair g).range, (T (⇑(f.pair g) ⁻¹' {x})) x.1 + ∑ x ∈ (f.pair g).range, (T (⇑(f.pair g) ⁻¹' {x})) x.2

Tactic:
rw [Finset.sum_add_distrib]

Result:
no goals

Proof state:
α : Type u_1
E : Type u_2
F : Type u_3
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
m : MeasurableSpace α
μ : Measure α
T : Set α → E →L[ℝ] F
h_add : FinMeasAdditive μ T
f g : α →ₛ E
hf : Integrable (⇑f) μ
hg : Integrable (⇑g) μ
hp_pair : Integrable (⇑(f.pair g)) μ
⊢ ∑ x ∈ (f.pair g).range, (T (⇑(f.pair g) ⁻¹' {x})) x.1 + ∑ x ∈ (f.pair g).range, (T (⇑(f.pair g) ⁻¹' {x})) x.2 =
    setToSimpleFunc T (map Prod.fst (f.pair g)) + setToSimpleFunc T (map Prod.snd (f.pair g))

Tactic:
rw [map_setToSimpleFunc T h_add hp_pair Prod.snd_zero,
  map_setToSimpleFunc T h_add hp_pair Prod.fst_zero]

Result:
no goals
-- Mathlib/Order/Interval/Finset/Fin.lean
@[simp]
lemma card_Ioc : #(Ioc a b) = b - a

Proof state:
n : ℕ
a b : Fin n
⊢ #(Ioc a b) = ↑b - ↑a

Tactic:
rw [← Nat.card_Ioc, ← map_valEmbedding_Ioc, card_map]

Result:
no goals
-- Mathlib/RingTheory/Polynomial/Basic.lean
theorem mem_map_C_iff {I : Ideal R} {f : R[X]} :
    f ∈ (Ideal.map (C : R →+* R[X]) I : Ideal R[X]) ↔ ∀ n : ℕ, f.coeff n ∈ I

Proof state:
case mp.refine_1.intro
R : Type u
inst✝ : CommSemiring R
I : Ideal R
f✝ : R[X]
hf✝ : f✝ ∈ map C I
f : R[X]
hf : f ∈ ⇑C '' ↑I
n : ℕ
x : R
hx : x ∈ ↑I ∧ C x = f
⊢ (if n = 0 then x else 0) ∈ I

Tactic:
by_cases h : n = 0

Result:
case pos
R : Type u
inst✝ : CommSemiring R
I : Ideal R
f✝ : R[X]
hf✝ : f✝ ∈ map C I
f : R[X]
hf : f ∈ ⇑C '' ↑I
n : ℕ
x : R
hx : x ∈ ↑I ∧ C x = f
h : n = 0
⊢ (if n = 0 then x else 0) ∈ I

case neg
R : Type u
inst✝ : CommSemiring R
I : Ideal R
f✝ : R[X]
hf✝ : f✝ ∈ map C I
f : R[X]
hf : f ∈ ⇑C '' ↑I
n : ℕ
x : R
hx : x ∈ ↑I ∧ C x = f
h : ¬n = 0
⊢ (if n = 0 then x else 0) ∈ I
-- Mathlib/LinearAlgebra/Basis/Cardinality.lean
/--
Over any nontrivial ring, the existence of a finite spanning set implies that any basis is finite.
-/
lemma basis_finite_of_finite_spans (w : Set M) (hw : w.Finite) (s : span R w = ⊤) {ι : Type w}
    (b : Basis ι R M) : Finite ι

Proof state:
R : Type u
M : Type v
inst✝³ : Semiring R
inst✝² : AddCommMonoid M
inst✝¹ : Nontrivial R
inst✝ : Module R M
w : Set M
hw : w.Finite
s : span R w = ⊤
ι : Type w
b : Basis ι R M
this : Finite ↑w
val✝ : Fintype ↑w
i : Infinite ι
S : Finset ι := Finset.univ.sup fun x => (b.repr ↑x).support
bS : Set M := ⇑b '' ↑S
h : ∀ x ∈ w, x ∈ span R bS
k : span R bS = ⊤
x : ι
nm : x ∉ S
⊢ b x ∈ span R bS

Tactic:
rw [k]

Result:
R : Type u
M : Type v
inst✝³ : Semiring R
inst✝² : AddCommMonoid M
inst✝¹ : Nontrivial R
inst✝ : Module R M
w : Set M
hw : w.Finite
s : span R w = ⊤
ι : Type w
b : Basis ι R M
this : Finite ↑w
val✝ : Fintype ↑w
i : Infinite ι
S : Finset ι := Finset.univ.sup fun x => (b.repr ↑x).support
bS : Set M := ⇑b '' ↑S
h : ∀ x ∈ w, x ∈ span R bS
k : span R bS = ⊤
x : ι
nm : x ∉ S
⊢ b x ∈ ⊤