harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/Topology/MetricSpace/Completion.lean
theorem dist_triangle (x y z : Completion α) : dist x z ≤ dist x y + dist y z

Proof state:
α : Type u
inst✝ : PseudoMetricSpace α
x y z : Completion α
⊢ dist x z ≤ dist x y + dist y z

Tactic:
refine induction_on₃ x y z ?_ ?_

Result:
case refine_1
α : Type u
inst✝ : PseudoMetricSpace α
x y z : Completion α
⊢ IsClosed {x | dist x.1 x.2.2 ≤ dist x.1 x.2.1 + dist x.2.1 x.2.2}

case refine_2
α : Type u
inst✝ : PseudoMetricSpace α
x y z : Completion α
⊢ ∀ (a b c : α), dist ↑a ↑c ≤ dist ↑a ↑b + dist ↑b ↑c

Proof state:
case refine_2
α : Type u
inst✝ : PseudoMetricSpace α
x y z : Completion α
⊢ ∀ (a b c : α), dist ↑a ↑c ≤ dist ↑a ↑b + dist ↑b ↑c

Tactic:
intro a b c

Result:
case refine_2
α : Type u
inst✝ : PseudoMetricSpace α
x y z : Completion α
a b c : α
⊢ dist ↑a ↑c ≤ dist ↑a ↑b + dist ↑b ↑c

Proof state:
case refine_1
α : Type u
inst✝ : PseudoMetricSpace α
x y z : Completion α
⊢ IsClosed {x | dist x.1 x.2.2 ≤ dist x.1 x.2.1 + dist x.2.1 x.2.2}

Tactic:
refine isClosed_le ?_ (Continuous.add ?_ ?_) <;>
  apply_rules [Completion.continuous_dist, Continuous.fst, Continuous.snd, continuous_id]

Result:
no goals

Proof state:
case refine_2
α : Type u
inst✝ : PseudoMetricSpace α
x y z : Completion α
a b c : α
⊢ dist a c ≤ dist a b + dist b c

Tactic:
exact dist_triangle a b c

Result:
no goals

Proof state:
case refine_2
α : Type u
inst✝ : PseudoMetricSpace α
x y z : Completion α
a b c : α
⊢ dist ↑a ↑c ≤ dist ↑a ↑b + dist ↑b ↑c

Tactic:
rw [Completion.dist_eq, Completion.dist_eq, Completion.dist_eq]

Result:
case refine_2
α : Type u
inst✝ : PseudoMetricSpace α
x y z : Completion α
a b c : α
⊢ dist a c ≤ dist a b + dist b c
-- Mathlib/Data/Stream/Init.lean
theorem get_inits : ∀ (n : ℕ) (s : Stream' α), get (inits s) n = take (succ n) s

Proof state:
case zero
α : Type u
⊢ ∀ (s : Stream' α), s.inits.get 0 = take (succ 0) s

Tactic:
intros

Result:
case zero
α : Type u
s✝ : Stream' α
⊢ s✝.inits.get 0 = take (succ 0) s✝

Proof state:
case zero
α : Type u
s✝ : Stream' α
⊢ s✝.inits.get 0 = take (succ 0) s✝

Tactic:
rfl

Result:
no goals

Proof state:
case succ
α : Type u
n' : ℕ
ih : ∀ (s : Stream' α), s.inits.get n' = take n'.succ s
⊢ ∀ (s : Stream' α), s.inits.get (n' + 1) = take (n' + 1).succ s

Tactic:
intros

Result:
case succ
α : Type u
n' : ℕ
ih : ∀ (s : Stream' α), s.inits.get n' = take n'.succ s
s✝ : Stream' α
⊢ s✝.inits.get (n' + 1) = take (n' + 1).succ s✝

Proof state:
α : Type u
n : ℕ
⊢ ∀ (s : Stream' α), s.inits.get n = take n.succ s

Tactic:
induction' n with n' ih

Result:
case zero
α : Type u
⊢ ∀ (s : Stream' α), s.inits.get 0 = take (succ 0) s

case succ
α : Type u
n' : ℕ
ih : ∀ (s : Stream' α), s.inits.get n' = take n'.succ s
⊢ ∀ (s : Stream' α), s.inits.get (n' + 1) = take (n' + 1).succ s

Proof state:
α : Type u
⊢ ∀ (n : ℕ) (s : Stream' α), s.inits.get n = take n.succ s

Tactic:
intro n

Result:
α : Type u
n : ℕ
⊢ ∀ (s : Stream' α), s.inits.get n = take n.succ s

Proof state:
case succ
α : Type u
n' : ℕ
ih : ∀ (s : Stream' α), s.inits.get n' = take n'.succ s
s✝ : Stream' α
⊢ s✝.inits.get (n' + 1) = take (n' + 1).succ s✝

Tactic:
rw [get_succ, take_succ, ← ih, tail_inits, inits_tail, cons_get_inits_core]

Result:
no goals
-- Mathlib/MeasureTheory/Order/Lattice.lean
theorem Finset.measurable_range_sup'' {f : ℕ → δ → α} {n : ℕ} (hf : ∀ k ≤ n, Measurable (f k)) :
    Measurable fun x => (range (n + 1)).sup' nonempty_range_succ fun k => f k x

Proof state:
case h.e'_5.h
α : Type u_2
m : MeasurableSpace α
δ : Type u_3
inst✝² : MeasurableSpace δ
inst✝¹ : SemilatticeSup α
inst✝ : MeasurableSup₂ α
f : ℕ → δ → α
n : ℕ
hf : ∀ k ≤ n, Measurable (f k)
x : δ
⊢ ((range (n + 1)).sup' ⋯ fun k => f k x) = (range (n + 1)).sup' ⋯ f x

Tactic:
simp

Result:
no goals

Proof state:
α : Type u_2
m : MeasurableSpace α
δ : Type u_3
inst✝² : MeasurableSpace δ
inst✝¹ : SemilatticeSup α
inst✝ : MeasurableSup₂ α
f : ℕ → δ → α
n : ℕ
hf : ∀ k ≤ n, Measurable (f k)
⊢ Measurable fun x => (range (n + 1)).sup' ⋯ fun k => f k x

Tactic:
convert Finset.measurable_range_sup' hf using 1

Result:
case h.e'_5
α : Type u_2
m : MeasurableSpace α
δ : Type u_3
inst✝² : MeasurableSpace δ
inst✝¹ : SemilatticeSup α
inst✝ : MeasurableSup₂ α
f : ℕ → δ → α
n : ℕ
hf : ∀ k ≤ n, Measurable (f k)
⊢ (fun x => (range (n + 1)).sup' ⋯ fun k => f k x) = (range (n + 1)).sup' ⋯ f

Proof state:
case h.e'_5
α : Type u_2
m : MeasurableSpace α
δ : Type u_3
inst✝² : MeasurableSpace δ
inst✝¹ : SemilatticeSup α
inst✝ : MeasurableSup₂ α
f : ℕ → δ → α
n : ℕ
hf : ∀ k ≤ n, Measurable (f k)
⊢ (fun x => (range (n + 1)).sup' ⋯ fun k => f k x) = (range (n + 1)).sup' ⋯ f

Tactic:
ext x

Result:
case h.e'_5.h
α : Type u_2
m : MeasurableSpace α
δ : Type u_3
inst✝² : MeasurableSpace δ
inst✝¹ : SemilatticeSup α
inst✝ : MeasurableSup₂ α
f : ℕ → δ → α
n : ℕ
hf : ∀ k ≤ n, Measurable (f k)
x : δ
⊢ ((range (n + 1)).sup' ⋯ fun k => f k x) = (range (n + 1)).sup' ⋯ f x
-- Mathlib/Algebra/Homology/TotalComplex.lean
lemma d₁_eq {i₁ i₁' : I₁} (h : c₁.Rel i₁ i₁') (i₂ : I₂) (i₁₂ : I₁₂)
    (h' : ComplexShape.π c₁ c₂ c₁₂ ⟨i₁', i₂⟩ = i₁₂) :
    K.d₁ c₁₂ i₁ i₂ i₁₂ = ComplexShape.ε₁ c₁ c₂ c₁₂ ⟨i₁, i₂⟩ • ((K.d i₁ i₁').f i₂ ≫
      K.toGradedObject.ιMapObj (ComplexShape.π c₁ c₂ c₁₂) ⟨i₁', i₂⟩ i₁₂ h')

Proof state:
C : Type u_1
inst✝⁴ : Category.{u_5, u_1} C
inst✝³ : Preadditive C
I₁ : Type u_2
I₂ : Type u_3
I₁₂ : Type u_4
c₁ : ComplexShape I₁
c₂ : ComplexShape I₂
K : HomologicalComplex₂ C c₁ c₂
c₁₂ : ComplexShape I₁₂
inst✝² : TotalComplexShape c₁ c₂ c₁₂
inst✝¹ : DecidableEq I₁₂
inst✝ : K.HasTotal c₁₂
i₁ i₁' : I₁
h : c₁.Rel i₁ i₁'
i₂ : I₂
i₁₂ : I₁₂
h' : c₁.π c₂ c₁₂ (i₁', i₂) = i₁₂
⊢ K.d₁ c₁₂ i₁ i₂ i₁₂ =
    c₁.ε₁ c₂ c₁₂ (i₁, i₂) • (K.d i₁ i₁').f i₂ ≫ K.toGradedObject.ιMapObj (c₁.π c₂ c₁₂) (i₁', i₂) i₁₂ h'

Tactic:
rw [d₁_eq' K c₁₂ h i₂ i₁₂, K.toGradedObject.ιMapObjOrZero_eq]

Result:
no goals
-- Mathlib/MeasureTheory/Integral/SetToL1.lean
theorem setToFun_neg (hT : DominatedFinMeasAdditive μ T C) (f : α → E) :
    setToFun μ T hT (-f) = -setToFun μ T hT f

Proof state:
case neg
α : 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 α
inst✝ : CompleteSpace F
T : Set α → E →L[ℝ] F
C : ℝ
hT : DominatedFinMeasAdditive μ T C
f : α → E
hf : ¬Integrable f μ
⊢ ¬Integrable (-f) μ

Tactic:
rwa [← integrable_neg_iff] at hf

Result:
no goals

Proof state:
case pos
α : 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 α
inst✝ : CompleteSpace F
T : Set α → E →L[ℝ] F
C : ℝ
hT : DominatedFinMeasAdditive μ T C
f : α → E
hf : Integrable f μ
⊢ setToFun μ T hT (-f) = -setToFun μ T hT f

Tactic:
rw [setToFun_eq hT hf, setToFun_eq hT hf.neg, Integrable.toL1_neg,
  (L1.setToL1 hT).map_neg]

Result:
no goals

Proof state:
case neg
α : 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 α
inst✝ : CompleteSpace F
T : Set α → E →L[ℝ] F
C : ℝ
hT : DominatedFinMeasAdditive μ T C
f : α → E
hf : ¬Integrable f μ
⊢ setToFun μ T hT (-f) = -setToFun μ T hT f

Tactic:
rw [setToFun_undef hT hf, setToFun_undef hT, neg_zero]

Result:
case neg
α : 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 α
inst✝ : CompleteSpace F
T : Set α → E →L[ℝ] F
C : ℝ
hT : DominatedFinMeasAdditive μ T C
f : α → E
hf : ¬Integrable f μ
⊢ ¬Integrable (-f) μ

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 α
inst✝ : CompleteSpace F
T : Set α → E →L[ℝ] F
C : ℝ
hT : DominatedFinMeasAdditive μ T C
f : α → E
⊢ setToFun μ T hT (-f) = -setToFun μ T hT f

Tactic:
by_cases hf : Integrable f μ

Result:
case pos
α : 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 α
inst✝ : CompleteSpace F
T : Set α → E →L[ℝ] F
C : ℝ
hT : DominatedFinMeasAdditive μ T C
f : α → E
hf : Integrable f μ
⊢ setToFun μ T hT (-f) = -setToFun μ T hT f

case neg
α : 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 α
inst✝ : CompleteSpace F
T : Set α → E →L[ℝ] F
C : ℝ
hT : DominatedFinMeasAdditive μ T C
f : α → E
hf : ¬Integrable f μ
⊢ setToFun μ T hT (-f) = -setToFun μ T hT f
-- Mathlib/Algebra/Polynomial/Basic.lean
theorem monomial_one_right_eq_X_pow (n : ℕ) : monomial n (1 : R) = X ^ n

Proof state:
case zero
R : Type u
inst✝ : Semiring R
⊢ (monomial 0) 1 = X ^ 0

Tactic:
simp [monomial_zero_one]

Result:
no goals

Proof state:
case succ
R : Type u
inst✝ : Semiring R
n : ℕ
ih : (monomial n) 1 = X ^ n
⊢ (monomial (n + 1)) 1 = X ^ (n + 1)

Tactic:
rw [pow_succ, ← ih, ← monomial_one_one_eq_X, monomial_mul_monomial, mul_one]

Result:
no goals

Proof state:
R : Type u
inst✝ : Semiring R
n : ℕ
⊢ (monomial n) 1 = X ^ n

Tactic:
induction n with
| zero => simp [monomial_zero_one]
| succ n ih => rw [pow_succ, ← ih, ← monomial_one_one_eq_X, monomial_mul_monomial, mul_one]

Result:
no goals
-- Mathlib/LinearAlgebra/TensorProduct/Basic.lean
theorem rTensor_comp_map (f' : P →ₗ[R] S) (f : M →ₗ[R] P) (g : N →ₗ[R] Q) :
    (f'.rTensor _).comp (map f g) = map (f'.comp f) g

Proof state:
R : Type u_1
inst✝¹⁰ : CommSemiring R
M : Type u_5
N : Type u_6
P : Type u_7
Q : Type u_8
S : Type u_9
inst✝⁹ : AddCommMonoid M
inst✝⁸ : AddCommMonoid N
inst✝⁷ : AddCommMonoid P
inst✝⁶ : AddCommMonoid Q
inst✝⁵ : AddCommMonoid S
inst✝⁴ : Module R M
inst✝³ : Module R N
inst✝² : Module R Q
inst✝¹ : Module R S
inst✝ : Module R P
f' : P →ₗ[R] S
f : M →ₗ[R] P
g : N →ₗ[R] Q
⊢ rTensor Q f' ∘ₗ map f g = map (f' ∘ₗ f) g

Tactic:
simp only [lTensor, rTensor, ← map_comp, id_comp, comp_id]

Result:
no goals
-- Mathlib/Analysis/Calculus/ContDiff/FaaDiBruno.lean
@[simp] lemma range_extendLeft_zero (c : OrderedFinpartition n) :
    range (c.extendLeft.emb 0) = {0}

Proof state:
n : ℕ
c : OrderedFinpartition n
⊢ Nonempty (Fin (cons 1 c.partSize 0))

Tactic:
simp

Result:
n : ℕ
c : OrderedFinpartition n
⊢ Nonempty (Fin 1)

Proof state:
n : ℕ
c : OrderedFinpartition n
⊢ (range fun x => 0) = {0}

Tactic:
apply @range_const _ _ (by simp; infer_instance)

Result:
no goals

Proof state:
n : ℕ
c : OrderedFinpartition n
⊢ Nonempty (Fin 1)

Tactic:
infer_instance

Result:
no goals

Proof state:
n : ℕ
c : OrderedFinpartition n
⊢ range (c.extendLeft.emb 0) = {0}

Tactic:
simp [extendLeft]

Result:
n : ℕ
c : OrderedFinpartition n
⊢ (range fun x => 0) = {0}
-- Mathlib/Probability/Kernel/Composition/MeasureComp.lean
lemma AbsolutelyContinuous.comp_left (μ : Measure α) (hκη : ∀ᵐ a ∂μ, κ a ≪ η a) :
    κ ∘ₘ μ ≪ η ∘ₘ μ

Proof state:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ η : Kernel α β
μ : Measure α
hκη : ∀ᵐ (a : α) ∂μ, κ a ≪ η a
s : Set β
hs : MeasurableSet s
hs_zero : (⇑η ∘ₘ μ) s = 0
⊢ (⇑κ ∘ₘ μ) s = 0

Tactic:
rw [Measure.bind_apply hs (Kernel.measurable _),
  lintegral_eq_zero_iff (Kernel.measurable_coe _ hs)] at hs_zero ⊢

Result:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ η : Kernel α β
μ : Measure α
hκη : ∀ᵐ (a : α) ∂μ, κ a ≪ η a
s : Set β
hs : MeasurableSet s
hs_zero : (fun a => (η a) s) =ᶠ[ae μ] 0
⊢ (fun a => (κ a) s) =ᶠ[ae μ] 0

Proof state:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ η : Kernel α β
μ : Measure α
hκη : ∀ᵐ (a : α) ∂μ, κ a ≪ η a
⊢ ⇑κ ∘ₘ μ ≪ ⇑η ∘ₘ μ

Tactic:
refine Measure.AbsolutelyContinuous.mk fun s hs hs_zero ↦ ?_

Result:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ η : Kernel α β
μ : Measure α
hκη : ∀ᵐ (a : α) ∂μ, κ a ≪ η a
s : Set β
hs : MeasurableSet s
hs_zero : (⇑η ∘ₘ μ) s = 0
⊢ (⇑κ ∘ₘ μ) s = 0

Proof state:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ η : Kernel α β
μ : Measure α
hκη : ∀ᵐ (a : α) ∂μ, κ a ≪ η a
s : Set β
hs : MeasurableSet s
hs_zero : (fun a => (η a) s) =ᶠ[ae μ] 0
⊢ (fun a => (κ a) s) =ᶠ[ae μ] 0

Tactic:
filter_upwards [hs_zero, hκη] with a ha_zero ha_ac using ha_ac ha_zero

Result:
no goals
-- Mathlib/Analysis/Convex/GaugeRescale.lean
theorem gaugeRescale_self_apply {s : Set E} (hsa : Absorbent ℝ s) (hsb : IsVonNBounded ℝ s)
    (x : E) : gaugeRescale s s x = x

Proof state:
E : Type u_1
inst✝³ : AddCommGroup E
inst✝² : Module ℝ E
inst✝¹ : TopologicalSpace E
inst✝ : T1Space E
s : Set E
hsa : Absorbent ℝ s
hsb : IsVonNBounded ℝ s
x : E
⊢ gaugeRescale s s x = x

Tactic:
rcases eq_or_ne x 0 with rfl | hx

Result:
case inl
E : Type u_1
inst✝³ : AddCommGroup E
inst✝² : Module ℝ E
inst✝¹ : TopologicalSpace E
inst✝ : T1Space E
s : Set E
hsa : Absorbent ℝ s
hsb : IsVonNBounded ℝ s
⊢ gaugeRescale s s 0 = 0

case inr
E : Type u_1
inst✝³ : AddCommGroup E
inst✝² : Module ℝ E
inst✝¹ : TopologicalSpace E
inst✝ : T1Space E
s : Set E
hsa : Absorbent ℝ s
hsb : IsVonNBounded ℝ s
x : E
hx : x ≠ 0
⊢ gaugeRescale s s x = x

Proof state:
case inl
E : Type u_1
inst✝³ : AddCommGroup E
inst✝² : Module ℝ E
inst✝¹ : TopologicalSpace E
inst✝ : T1Space E
s : Set E
hsa : Absorbent ℝ s
hsb : IsVonNBounded ℝ s
⊢ gaugeRescale s s 0 = 0

Tactic:
simp

Result:
no goals

Proof state:
case inr
E : Type u_1
inst✝³ : AddCommGroup E
inst✝² : Module ℝ E
inst✝¹ : TopologicalSpace E
inst✝ : T1Space E
s : Set E
hsa : Absorbent ℝ s
hsb : IsVonNBounded ℝ s
x : E
hx : x ≠ 0
⊢ gaugeRescale s s x = x

Tactic:
rw [gaugeRescale, div_self, one_smul]

Result:
case inr
E : Type u_1
inst✝³ : AddCommGroup E
inst✝² : Module ℝ E
inst✝¹ : TopologicalSpace E
inst✝ : T1Space E
s : Set E
hsa : Absorbent ℝ s
hsb : IsVonNBounded ℝ s
x : E
hx : x ≠ 0
⊢ gauge s x ≠ 0

Proof state:
case inr
E : Type u_1
inst✝³ : AddCommGroup E
inst✝² : Module ℝ E
inst✝¹ : TopologicalSpace E
inst✝ : T1Space E
s : Set E
hsa : Absorbent ℝ s
hsb : IsVonNBounded ℝ s
x : E
hx : x ≠ 0
⊢ gauge s x ≠ 0

Tactic:
exact ((gauge_pos hsa hsb).2 hx).ne'

Result:
no goals
-- Mathlib/Order/BooleanAlgebra.lean
theorem sdiff_unique (s : x ⊓ y ⊔ z = x) (i : x ⊓ y ⊓ z = ⊥) : x \ y = z

Proof state:
α : Type u
x y z : α
inst✝ : GeneralizedBooleanAlgebra α
s : z ⊔ x ⊓ y = x \ y ⊔ x ⊓ y
i : x ⊓ y ⊓ z = x \ y ⊓ (x ⊓ y)
⊢ x \ y = z

Tactic:
rw [inf_comm] at i

Result:
α : Type u
x y z : α
inst✝ : GeneralizedBooleanAlgebra α
s : z ⊔ x ⊓ y = x \ y ⊔ x ⊓ y
i : z ⊓ (x ⊓ y) = x \ y ⊓ (x ⊓ y)
⊢ x \ y = z

Proof state:
α : Type u
x y z : α
inst✝ : GeneralizedBooleanAlgebra α
s : z ⊔ x ⊓ y = x \ y ⊔ x ⊓ y
i : z ⊓ (x ⊓ y) = x \ y ⊓ (x ⊓ y)
⊢ x \ y = z

Tactic:
exact (eq_of_inf_eq_sup_eq i s).symm

Result:
no goals

Proof state:
α : Type u
x y z : α
inst✝ : GeneralizedBooleanAlgebra α
s : x ⊓ y ⊔ z = x
i : x ⊓ y ⊓ z = ⊥
⊢ x \ y = z

Tactic:
conv_rhs at s => rw [← sup_inf_sdiff x y, sup_comm]

Result:
α : Type u
x y z : α
inst✝ : GeneralizedBooleanAlgebra α
s : x ⊓ y ⊔ z = x \ y ⊔ x ⊓ y
i : x ⊓ y ⊓ z = ⊥
⊢ x \ y = z

Proof state:
α : Type u
x y z : α
inst✝ : GeneralizedBooleanAlgebra α
s : z ⊔ x ⊓ y = x \ y ⊔ x ⊓ y
i : x ⊓ y ⊓ z = ⊥
⊢ x \ y = z

Tactic:
conv_rhs at i => rw [← inf_inf_sdiff x y, inf_comm]

Result:
α : Type u
x y z : α
inst✝ : GeneralizedBooleanAlgebra α
s : z ⊔ x ⊓ y = x \ y ⊔ x ⊓ y
i : x ⊓ y ⊓ z = x \ y ⊓ (x ⊓ y)
⊢ x \ y = z

Proof state:
α : Type u
x y z : α
inst✝ : GeneralizedBooleanAlgebra α
s : x ⊓ y ⊔ z = x \ y ⊔ x ⊓ y
i : x ⊓ y ⊓ z = ⊥
⊢ x \ y = z

Tactic:
rw [sup_comm] at s

Result:
α : Type u
x y z : α
inst✝ : GeneralizedBooleanAlgebra α
s : z ⊔ x ⊓ y = x \ y ⊔ x ⊓ y
i : x ⊓ y ⊓ z = ⊥
⊢ x \ y = z
-- Mathlib/Algebra/Module/LinearMap/End.lean
lemma commute_id_left : Commute LinearMap.id f

Proof state:
R : Type u_9
M : Type u_10
inst✝² : Ring R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
f : End R M
⊢ Commute LinearMap.id f

Tactic:
ext

Result:
case h
R : Type u_9
M : Type u_10
inst✝² : Ring R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
f : End R M
x✝ : M
⊢ (LinearMap.id * f) x✝ = (f * LinearMap.id) x✝

Proof state:
case h
R : Type u_9
M : Type u_10
inst✝² : Ring R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
f : End R M
x✝ : M
⊢ (LinearMap.id * f) x✝ = (f * LinearMap.id) x✝

Tactic:
simp

Result:
no goals
-- Mathlib/Order/Interval/Set/Basic.lean
theorem Ioc_diff_right : Ioc a b \ {b} = Ioo a b :=
  ext fun x => by simp [and_assoc, ← lt_iff_le_and_ne]

Proof state:
α : Type u_1
inst✝ : PartialOrder α
a b x : α
⊢ x ∈ Ioc a b \ {b} ↔ x ∈ Ioo a b

Tactic:
simp [and_assoc, ← lt_iff_le_and_ne]

Result:
no goals
-- Mathlib/Topology/Sheaves/SheafCondition/Sites.lean
theorem covering_presieve_eq_self {Y : Opens X} (R : Presieve Y) :
    presieveOfCoveringAux (coveringOfPresieve Y R) Y = R

Proof state:
X : TopCat
Y : Opens ↑X
R : Presieve Y
Z : Opens ↑X
f : Z ⟶ Y
x✝ : f ∈ presieveOfCoveringAux (coveringOfPresieve Y R) Y
f' : Z ⟶ Y
h : R f'
⊢ f ∈ R

Tactic:
rwa [Subsingleton.elim f f']

Result:
no goals

Proof state:
case h
X : TopCat
Y : Opens ↑X
R : Presieve Y
Z : Opens ↑X
⊢ presieveOfCoveringAux (coveringOfPresieve Y R) Y = R

Tactic:
ext f

Result:
case h.h
X : TopCat
Y : Opens ↑X
R : Presieve Y
Z : Opens ↑X
f : Z ⟶ Y
⊢ f ∈ presieveOfCoveringAux (coveringOfPresieve Y R) Y ↔ f ∈ R

Proof state:
X : TopCat
Y : Opens ↑X
R : Presieve Y
⊢ presieveOfCoveringAux (coveringOfPresieve Y R) Y = R

Tactic:
funext Z

Result:
case h
X : TopCat
Y : Opens ↑X
R : Presieve Y
Z : Opens ↑X
⊢ presieveOfCoveringAux (coveringOfPresieve Y R) Y = R

Proof state:
case h.h
X : TopCat
Y : Opens ↑X
R : Presieve Y
Z : Opens ↑X
f : Z ⟶ Y
⊢ f ∈ presieveOfCoveringAux (coveringOfPresieve Y R) Y ↔ f ∈ R

Tactic:
exact ⟨fun ⟨⟨_, f', h⟩, rfl⟩ => by rwa [Subsingleton.elim f f'], fun h => ⟨⟨Z, f, h⟩, rfl⟩⟩

Result:
no goals
-- Mathlib/Combinatorics/HalesJewett.lean
lemma coe_injective [Nontrivial α] : Injective ((⇑) : Line α ι → α → ι → α)

Proof state:
α : Type u_2
ι : Type u_3
inst✝ : Nontrivial α
l m : Line α ι
hlm : ↑l = ↑m
⊢ l = m

Tactic:
ext i a

Result:
case idxFun.h.a
α : Type u_2
ι : Type u_3
inst✝ : Nontrivial α
l m : Line α ι
hlm : ↑l = ↑m
i : ι
a : α
⊢ a ∈ l.idxFun i ↔ a ∈ m.idxFun i

Proof state:
case idxFun.h.a.intro.refine_1
α : Type u_2
ι : Type u_3
inst✝ : Nontrivial α
l m : Line α ι
i : ι
a b : α
hba : b ≠ a
hlm : ∀ (x : α) (x_1 : ι), ↑l x x_1 = ↑m x x_1
h : l.idxFun i = some a
⊢ m.idxFun i = some a

Tactic:
cases hi : idxFun m i <;> simpa [@eq_comm _ a, hi, h, hba] using hlm b i

Result:
no goals

Proof state:
case idxFun.h.a.intro.refine_2
α : Type u_2
ι : Type u_3
inst✝ : Nontrivial α
l m : Line α ι
i : ι
a b : α
hba : b ≠ a
hlm : ∀ (x : α) (x_1 : ι), ↑l x x_1 = ↑m x x_1
h : m.idxFun i = some a
⊢ l.idxFun i = some a

Tactic:
cases hi : idxFun l i <;> simpa [@eq_comm _ a, hi, h, hba] using hlm b i

Result:
no goals

Proof state:
case idxFun.h.a.intro
α : Type u_2
ι : Type u_3
inst✝ : Nontrivial α
l m : Line α ι
i : ι
a b : α
hba : b ≠ a
hlm : ∀ (x : α) (x_1 : ι), ↑l x x_1 = ↑m x x_1
⊢ l.idxFun i = some a ↔ m.idxFun i = some a

Tactic:
refine ⟨fun h ↦ ?_, fun h ↦ ?_⟩

Result:
case idxFun.h.a.intro.refine_1
α : Type u_2
ι : Type u_3
inst✝ : Nontrivial α
l m : Line α ι
i : ι
a b : α
hba : b ≠ a
hlm : ∀ (x : α) (x_1 : ι), ↑l x x_1 = ↑m x x_1
h : l.idxFun i = some a
⊢ m.idxFun i = some a

case idxFun.h.a.intro.refine_2
α : Type u_2
ι : Type u_3
inst✝ : Nontrivial α
l m : Line α ι
i : ι
a b : α
hba : b ≠ a
hlm : ∀ (x : α) (x_1 : ι), ↑l x x_1 = ↑m x x_1
h : m.idxFun i = some a
⊢ l.idxFun i = some a

Proof state:
α : Type u_2
ι : Type u_3
inst✝ : Nontrivial α
⊢ Injective toFun

Tactic:
rintro l m hlm

Result:
α : Type u_2
ι : Type u_3
inst✝ : Nontrivial α
l m : Line α ι
hlm : ↑l = ↑m
⊢ l = m

Proof state:
case idxFun.h.a
α : Type u_2
ι : Type u_3
inst✝ : Nontrivial α
l m : Line α ι
hlm : ↑l = ↑m
i : ι
a : α
⊢ a ∈ l.idxFun i ↔ a ∈ m.idxFun i

Tactic:
obtain ⟨b, hba⟩ := exists_ne a

Result:
case idxFun.h.a.intro
α : Type u_2
ι : Type u_3
inst✝ : Nontrivial α
l m : Line α ι
hlm : ↑l = ↑m
i : ι
a b : α
hba : b ≠ a
⊢ a ∈ l.idxFun i ↔ a ∈ m.idxFun i

Proof state:
case idxFun.h.a.intro
α : Type u_2
ι : Type u_3
inst✝ : Nontrivial α
l m : Line α ι
hlm : ↑l = ↑m
i : ι
a b : α
hba : b ≠ a
⊢ a ∈ l.idxFun i ↔ a ∈ m.idxFun i

Tactic:
simp only [Option.mem_def, funext_iff] at hlm ⊢

Result:
case idxFun.h.a.intro
α : Type u_2
ι : Type u_3
inst✝ : Nontrivial α
l m : Line α ι
i : ι
a b : α
hba : b ≠ a
hlm : ∀ (x : α) (x_1 : ι), ↑l x x_1 = ↑m x x_1
⊢ l.idxFun i = some a ↔ m.idxFun i = some a
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Nat/Bitwise/Lemmas.lean
theorem testBit_lt_two_pow {x i : Nat} (lt : x < 2^i) : x.testBit i = false

Proof state:
x i : Nat
lt : x < 2 ^ i
p : x.testBit i = true
⊢ False

Tactic:
exact Nat.not_le_of_gt lt (testBit_implies_ge p)

Result:
no goals

Proof state:
x i : Nat
lt : x < 2 ^ i
⊢ x.testBit i = false

Tactic:
match p : x.testBit i with
| false => trivial
| true =>
  exfalso
  exact Nat.not_le_of_gt lt (testBit_implies_ge p)

Result:
no goals

Proof state:
x i : Nat
lt : x < 2 ^ i
p : x.testBit i = false
⊢ false = false

Tactic:
trivial

Result:
no goals

Proof state:
x i : Nat
lt : x < 2 ^ i
p : x.testBit i = true
⊢ true = false

Tactic:
exfalso

Result:
x i : Nat
lt : x < 2 ^ i
p : x.testBit i = true
⊢ False
-- Mathlib/CategoryTheory/Sites/Sieves.lean
theorem ofArrows_pUnit : (ofArrows _ fun _ : PUnit => f) = singleton f

Proof state:
case h.h.mpr.mk
C : Type u₁
inst✝ : Category.{v₁, u₁} C
X Y✝ : C
f : Y✝ ⟶ X
Y : C
⊢ f ∈ ofArrows (fun x => Y✝) fun x => f

Tactic:
exact ofArrows.mk PUnit.unit

Result:
no goals

Proof state:
case h.h
C : Type u₁
inst✝ : Category.{v₁, u₁} C
X Y✝ : C
f : Y✝ ⟶ X
Y : C
g : Y ⟶ X
⊢ (g ∈ ofArrows (fun x => Y✝) fun x => f) ↔ g ∈ singleton f

Tactic:
constructor

Result:
case h.h.mp
C : Type u₁
inst✝ : Category.{v₁, u₁} C
X Y✝ : C
f : Y✝ ⟶ X
Y : C
g : Y ⟶ X
⊢ (g ∈ ofArrows (fun x => Y✝) fun x => f) → g ∈ singleton f

case h.h.mpr
C : Type u₁
inst✝ : Category.{v₁, u₁} C
X Y✝ : C
f : Y✝ ⟶ X
Y : C
g : Y ⟶ X
⊢ g ∈ singleton f → g ∈ ofArrows (fun x => Y✝) fun x => f

Proof state:
case h.h.mpr
C : Type u₁
inst✝ : Category.{v₁, u₁} C
X Y✝ : C
f : Y✝ ⟶ X
Y : C
g : Y ⟶ X
⊢ g ∈ singleton f → g ∈ ofArrows (fun x => Y✝) fun x => f

Tactic:
rintro ⟨_⟩

Result:
case h.h.mpr.mk
C : Type u₁
inst✝ : Category.{v₁, u₁} C
X Y✝ : C
f : Y✝ ⟶ X
Y : C
⊢ f ∈ ofArrows (fun x => Y✝) fun x => f

Proof state:
case h.h.mp.mk
C : Type u₁
inst✝ : Category.{v₁, u₁} C
X Y✝ : C
f : Y✝ ⟶ X
Y : C
i✝ : PUnit.{u_1 + 1}
⊢ f ∈ singleton f

Tactic:
apply singleton.mk

Result:
no goals

Proof state:
C : Type u₁
inst✝ : Category.{v₁, u₁} C
X Y : C
f : Y ⟶ X
⊢ (ofArrows (fun x => Y) fun x => f) = singleton f

Tactic:
funext Y

Result:
case h
C : Type u₁
inst✝ : Category.{v₁, u₁} C
X Y✝ : C
f : Y✝ ⟶ X
Y : C
⊢ (ofArrows (fun x => Y✝) fun x => f) = singleton f

Proof state:
case h
C : Type u₁
inst✝ : Category.{v₁, u₁} C
X Y✝ : C
f : Y✝ ⟶ X
Y : C
⊢ (ofArrows (fun x => Y✝) fun x => f) = singleton f

Tactic:
ext g

Result:
case h.h
C : Type u₁
inst✝ : Category.{v₁, u₁} C
X Y✝ : C
f : Y✝ ⟶ X
Y : C
g : Y ⟶ X
⊢ (g ∈ ofArrows (fun x => Y✝) fun x => f) ↔ g ∈ singleton f

Proof state:
case h.h.mp
C : Type u₁
inst✝ : Category.{v₁, u₁} C
X Y✝ : C
f : Y✝ ⟶ X
Y : C
g : Y ⟶ X
⊢ (g ∈ ofArrows (fun x => Y✝) fun x => f) → g ∈ singleton f

Tactic:
rintro ⟨_⟩

Result:
case h.h.mp.mk
C : Type u₁
inst✝ : Category.{v₁, u₁} C
X Y✝ : C
f : Y✝ ⟶ X
Y : C
i✝ : PUnit.{u_1 + 1}
⊢ f ∈ singleton f
-- Mathlib/Data/Vector/Basic.lean
theorem scanl_cons (x : α) : scanl f b (x ::ᵥ v) = b ::ᵥ scanl f (f b x) v

Proof state:
α : Type u_1
n : ℕ
β : Type u_6
f : β → α → β
b : β
v : Vector α n
x : α
⊢ ⟨b :: List.scanl f (f b x) v.toList, ⋯⟩ = b ::ᵥ ⟨List.scanl f (f b x) v.toList, ⋯⟩

Tactic:
simp only [cons]

Result:
no goals

Proof state:
α : Type u_1
n : ℕ
β : Type u_6
f : β → α → β
b : β
v : Vector α n
x : α
⊢ scanl f b (x ::ᵥ v) = b ::ᵥ scanl f (f b x) v

Tactic:
simp only [scanl, toList_cons, List.scanl]

Result:
α : Type u_1
n : ℕ
β : Type u_6
f : β → α → β
b : β
v : Vector α n
x : α
⊢ ⟨b :: List.scanl f (f b x) v.toList, ⋯⟩ = b ::ᵥ ⟨List.scanl f (f b x) v.toList, ⋯⟩