harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/Data/List/Basic.lean
theorem foldl_eq_of_comm_of_assoc [hcomm : Std.Commutative f] [hassoc : Std.Associative f] :
    ∀ a b l, foldl f a (b :: l) = f b (foldl f a l)
  | a, b, nil => hcomm.comm a b
  | a, b, c :: l => by
    simp only [foldl_cons]
    have : RightCommutative f := inferInstance
    rw [← foldl_eq_of_comm_of_assoc .., this.right_comm, foldl_cons]

Proof state:
α : Type u
f : α → α → α
hcomm : Std.Commutative f
hassoc : Std.Associative f
a b c : α
l : List α
⊢ foldl f (f (f a b) c) l = f b (foldl f (f a c) l)

Tactic:
have : RightCommutative f := inferInstance

Result:
α : Type u
f : α → α → α
hcomm : Std.Commutative f
hassoc : Std.Associative f
a b c : α
l : List α
this : RightCommutative f
⊢ foldl f (f (f a b) c) l = f b (foldl f (f a c) l)

Proof state:
α : Type u
f : α → α → α
hcomm : Std.Commutative f
hassoc : Std.Associative f
a b c : α
l : List α
this : RightCommutative f
⊢ foldl f (f (f a b) c) l = f b (foldl f (f a c) l)

Tactic:
rw [← foldl_eq_of_comm_of_assoc .., this.right_comm, foldl_cons]

Result:
no goals

Proof state:
α : Type u
f : α → α → α
hcomm : Std.Commutative f
hassoc : Std.Associative f
a b c : α
l : List α
⊢ foldl f a (b :: c :: l) = f b (foldl f a (c :: l))

Tactic:
simp only [foldl_cons]

Result:
α : Type u
f : α → α → α
hcomm : Std.Commutative f
hassoc : Std.Associative f
a b c : α
l : List α
⊢ foldl f (f (f a b) c) l = f b (foldl f (f a c) l)
-- Mathlib/.lake/packages/batteries/Batteries/Logic.lean
theorem eqRec_eq_cast {α : Sort _} {a : α} {motive : (a' : α) → a = a' → Sort _}
    (x : motive a rfl) {a' : α} (e : a = a') :
    @Eq.rec α a motive x a' e = cast (e ▸ rfl) x

Proof state:
α : Sort u_1
a : α
motive : (a' : α) → a = a' → Sort u_2
x : motive a ⋯
a' : α
e : a = a'
⊢ e ▸ x = cast ⋯ x

Tactic:
subst e

Result:
α : Sort u_1
a : α
motive : (a' : α) → a = a' → Sort u_2
x : motive a ⋯
⊢ ⋯ ▸ x = cast ⋯ x

Proof state:
α : Sort u_1
a : α
motive : (a' : α) → a = a' → Sort u_2
x : motive a ⋯
⊢ ⋯ ▸ x = cast ⋯ x

Tactic:
rfl

Result:
no goals
-- Mathlib/Algebra/Central/Basic.lean
lemma mem_center_iff {x : D} : x ∈ Subalgebra.center K D ↔ ∃ (a : K), x = algebraMap K D a

Proof state:
K : Type u
inst✝² : CommSemiring K
D : Type v
inst✝¹ : Semiring D
inst✝ : Algebra K D
h : IsCentral K D
x : D
⊢ x ∈ Set.range ⇑(algebraMap K D) ↔ ∃ a, x = (algebraMap K D) a

Tactic:
simp [eq_comm]

Result:
no goals

Proof state:
K : Type u
inst✝² : CommSemiring K
D : Type v
inst✝¹ : Semiring D
inst✝ : Algebra K D
h : IsCentral K D
x : D
⊢ x ∈ Subalgebra.center K D ↔ ∃ a, x = (algebraMap K D) a

Tactic:
rw [center_eq_bot, Algebra.mem_bot]

Result:
K : Type u
inst✝² : CommSemiring K
D : Type v
inst✝¹ : Semiring D
inst✝ : Algebra K D
h : IsCentral K D
x : D
⊢ x ∈ Set.range ⇑(algebraMap K D) ↔ ∃ a, x = (algebraMap K D) a
-- Mathlib/Algebra/Order/Group/Unbundled/Abs.lean
@[to_additive] lemma max_div_min_eq_mabs' (a b : α) : max a b / min a b = |a / b|ₘ

Proof state:
case inr
α : Type u_1
inst✝³ : Group α
inst✝² : LinearOrder α
inst✝¹ : MulLeftMono α
inst✝ : MulRightMono α
a b : α
ba : b ≤ a
⊢ 1 ≤ a / b

Tactic:
rwa [one_le_div']

Result:
no goals

Proof state:
case inl
α : Type u_1
inst✝³ : Group α
inst✝² : LinearOrder α
inst✝¹ : MulLeftMono α
inst✝ : MulRightMono α
a b : α
ab : a ≤ b
⊢ (a ⊔ b) / (a ⊓ b) = mabs (a / b)

Tactic:
rw [max_eq_right ab, min_eq_left ab, mabs_of_le_one, inv_div]

Result:
case inl
α : Type u_1
inst✝³ : Group α
inst✝² : LinearOrder α
inst✝¹ : MulLeftMono α
inst✝ : MulRightMono α
a b : α
ab : a ≤ b
⊢ a / b ≤ 1

Proof state:
α : Type u_1
inst✝³ : Group α
inst✝² : LinearOrder α
inst✝¹ : MulLeftMono α
inst✝ : MulRightMono α
a b : α
⊢ (a ⊔ b) / (a ⊓ b) = mabs (a / b)

Tactic:
rcases le_total a b with ab | ba

Result:
case inl
α : Type u_1
inst✝³ : Group α
inst✝² : LinearOrder α
inst✝¹ : MulLeftMono α
inst✝ : MulRightMono α
a b : α
ab : a ≤ b
⊢ (a ⊔ b) / (a ⊓ b) = mabs (a / b)

case inr
α : Type u_1
inst✝³ : Group α
inst✝² : LinearOrder α
inst✝¹ : MulLeftMono α
inst✝ : MulRightMono α
a b : α
ba : b ≤ a
⊢ (a ⊔ b) / (a ⊓ b) = mabs (a / b)

Proof state:
case inl
α : Type u_1
inst✝³ : Group α
inst✝² : LinearOrder α
inst✝¹ : MulLeftMono α
inst✝ : MulRightMono α
a b : α
ab : a ≤ b
⊢ a / b ≤ 1

Tactic:
rwa [div_le_one']

Result:
no goals

Proof state:
case inr
α : Type u_1
inst✝³ : Group α
inst✝² : LinearOrder α
inst✝¹ : MulLeftMono α
inst✝ : MulRightMono α
a b : α
ba : b ≤ a
⊢ (a ⊔ b) / (a ⊓ b) = mabs (a / b)

Tactic:
rw [max_eq_left ba, min_eq_right ba, mabs_of_one_le]

Result:
case inr
α : Type u_1
inst✝³ : Group α
inst✝² : LinearOrder α
inst✝¹ : MulLeftMono α
inst✝ : MulRightMono α
a b : α
ba : b ≤ a
⊢ 1 ≤ a / b
-- Mathlib/NumberTheory/LSeries/HurwitzZetaEven.lean
/-- The residue of `completedHurwitzZetaEven a s` at `s = 1` is equal to `1`. -/
lemma completedHurwitzZetaEven_residue_one (a : UnitAddCircle) :
    Tendsto (fun s ↦ (s - 1) * completedHurwitzZetaEven a s) (𝓝[≠] 1) (𝓝 1)

Proof state:
a : UnitAddCircle
h1 : Tendsto (fun s => (s - 1 / 2) * (hurwitzEvenFEPair a).Λ s) (𝓝[≠] (1 / 2)) (𝓝 1)
⊢ Tendsto (fun s => (s - 1) * completedHurwitzZetaEven a s) (𝓝[≠] 1) (𝓝 1)

Tactic:
refine (h1.comp <| tendsto_div_two_punctured_nhds 1).congr (fun s ↦ ?_)

Result:
a : UnitAddCircle
h1 : Tendsto (fun s => (s - 1 / 2) * (hurwitzEvenFEPair a).Λ s) (𝓝[≠] (1 / 2)) (𝓝 1)
s : ℂ
⊢ ((fun s => (s - 1 / 2) * (hurwitzEvenFEPair a).Λ s) ∘ fun s => s / 2) s = (s - 1) * completedHurwitzZetaEven a s

Proof state:
a : UnitAddCircle
h1 : Tendsto (fun s => (s - ↑(1 / 2)) * (hurwitzEvenFEPair a).Λ s) (𝓝[≠] ↑(1 / 2)) (𝓝 (1 * 1))
⊢ Tendsto (fun s => (s - 1) * completedHurwitzZetaEven a s) (𝓝[≠] 1) (𝓝 1)

Tactic:
simp only [push_cast, one_mul] at h1

Result:
a : UnitAddCircle
h1 : Tendsto (fun s => (s - 1 / 2) * (hurwitzEvenFEPair a).Λ s) (𝓝[≠] (1 / 2)) (𝓝 1)
⊢ Tendsto (fun s => (s - 1) * completedHurwitzZetaEven a s) (𝓝[≠] 1) (𝓝 1)

Proof state:
a : UnitAddCircle
h1 : Tendsto (fun s => (s - 1 / 2) * (hurwitzEvenFEPair a).Λ s) (𝓝[≠] (1 / 2)) (𝓝 1)
s : ℂ
⊢ ((fun s => (s - 1 / 2) * (hurwitzEvenFEPair a).Λ s) ∘ fun s => s / 2) s = (s - 1) * completedHurwitzZetaEven a s

Tactic:
rw [completedHurwitzZetaEven, Function.comp_apply, ← sub_div, div_mul_eq_mul_div, mul_div_assoc]

Result:
no goals

Proof state:
a : UnitAddCircle
⊢ Tendsto (fun s => (s - 1) * completedHurwitzZetaEven a s) (𝓝[≠] 1) (𝓝 1)

Tactic:
have h1 : Tendsto (fun s : ℂ ↦ (s - ↑(1  / 2 : ℝ)) * _) (𝓝[≠] ↑(1  / 2 : ℝ))
  (𝓝 ((1 : ℂ) * (1 : ℂ))) := (hurwitzEvenFEPair a).Λ_residue_k

Result:
a : UnitAddCircle
h1 : Tendsto (fun s => (s - ↑(1 / 2)) * (hurwitzEvenFEPair a).Λ s) (𝓝[≠] ↑(1 / 2)) (𝓝 (1 * 1))
⊢ Tendsto (fun s => (s - 1) * completedHurwitzZetaEven a s) (𝓝[≠] 1) (𝓝 1)
-- Mathlib/RingTheory/Perfectoid/Untilt.lean
theorem mk_untilt_eq_coeff_zero (x : PreTilt O p) :
    Ideal.Quotient.mk (Ideal.span {(p : O)}) (x.untilt) = coeff (ModP O p) p 0 x

Proof state:
O : Type u_1
inst✝³ : CommRing O
p : ℕ
inst✝² : Fact (Nat.Prime p)
inst✝¹ : Fact ¬IsUnit ↑p
inst✝ : IsAdicComplete (span {↑p}) O
x : PreTilt O p
⊢ (Ideal.Quotient.mk (span {↑p})) (untilt x) = (coeff (ModP O p) p 0) x

Tactic:
simp only [untilt]

Result:
O : Type u_1
inst✝³ : CommRing O
p : ℕ
inst✝² : Fact (Nat.Prime p)
inst✝¹ : Fact ¬IsUnit ↑p
inst✝ : IsAdicComplete (span {↑p}) O
x : PreTilt O p
⊢ (Ideal.Quotient.mk (span {↑p})) ({ toFun := untiltFun, map_one' := ⋯, map_mul' := ⋯ } x) = (coeff (ModP O p) p 0) x

Proof state:
O : Type u_1
inst✝³ : CommRing O
p : ℕ
inst✝² : Fact (Nat.Prime p)
inst✝¹ : Fact ¬IsUnit ↑p
inst✝ : IsAdicComplete (span {↑p}) O
x : PreTilt O p
⊢ (Ideal.Quotient.mk (span {↑p})) ({ toFun := untiltFun, map_one' := ⋯, map_mul' := ⋯ } x) = (coeff (ModP O p) p 0) x

Tactic:
rw [← Ideal.Quotient.mk_out ((coeff (ModP O p) p 0) x), Ideal.Quotient.eq, ← SModEq.sub_mem]

Result:
O : Type u_1
inst✝³ : CommRing O
p : ℕ
inst✝² : Fact (Nat.Prime p)
inst✝¹ : Fact ¬IsUnit ↑p
inst✝ : IsAdicComplete (span {↑p}) O
x : PreTilt O p
⊢ { toFun := untiltFun, map_one' := ⋯, map_mul' := ⋯ } x ≡ Quotient.out ((coeff (ModP O p) p 0) x) [SMOD span {↑p}]

Proof state:
O : Type u_1
inst✝³ : CommRing O
p : ℕ
inst✝² : Fact (Nat.Prime p)
inst✝¹ : Fact ¬IsUnit ↑p
inst✝ : IsAdicComplete (span {↑p}) O
x : PreTilt O p
⊢ { toFun := untiltFun, map_one' := ⋯, map_mul' := ⋯ } x ≡ Quotient.out ((coeff (ModP O p) p 0) x) [SMOD span {↑p}]

Tactic:
simpa [untiltAux] using (x.untiltAux_smodEq_untiltFun 1).symm

Result:
no goals
-- Mathlib/Analysis/Calculus/FDeriv/Prod.lean
theorem differentiableWithinAt_apply (i : ι) (f : ∀ i, F' i) (s' : Set (∀ i, F' i)) :
    DifferentiableWithinAt (𝕜 := 𝕜) (fun f : ∀ i, F' i => f i) s' f

Proof state:
case h
𝕜 : Type u_1
inst✝³ : NontriviallyNormedField 𝕜
ι : Type u_6
inst✝² : Fintype ι
F' : ι → Type u_7
inst✝¹ : (i : ι) → NormedAddCommGroup (F' i)
inst✝ : (i : ι) → NormedSpace 𝕜 (F' i)
i : ι
f : (i : ι) → F' i
s' : Set ((i : ι) → F' i)
⊢ HasFDerivWithinAt (fun f => f i) ?f' s' f

case f'
𝕜 : Type u_1
inst✝³ : NontriviallyNormedField 𝕜
ι : Type u_6
inst✝² : Fintype ι
F' : ι → Type u_7
inst✝¹ : (i : ι) → NormedAddCommGroup (F' i)
inst✝ : (i : ι) → NormedSpace 𝕜 (F' i)
i : ι
f : (i : ι) → F' i
s' : Set ((i : ι) → F' i)
⊢ ((i : ι) → F' i) →L[𝕜] F' i

Tactic:
fun_prop

Result:
no goals

Proof state:
𝕜 : Type u_1
inst✝³ : NontriviallyNormedField 𝕜
ι : Type u_6
inst✝² : Fintype ι
F' : ι → Type u_7
inst✝¹ : (i : ι) → NormedAddCommGroup (F' i)
inst✝ : (i : ι) → NormedSpace 𝕜 (F' i)
i : ι
f : (i : ι) → F' i
s' : Set ((i : ι) → F' i)
⊢ DifferentiableWithinAt 𝕜 (fun f => f i) s' f

Tactic:
apply HasFDerivWithinAt.differentiableWithinAt

Result:
case h
𝕜 : Type u_1
inst✝³ : NontriviallyNormedField 𝕜
ι : Type u_6
inst✝² : Fintype ι
F' : ι → Type u_7
inst✝¹ : (i : ι) → NormedAddCommGroup (F' i)
inst✝ : (i : ι) → NormedSpace 𝕜 (F' i)
i : ι
f : (i : ι) → F' i
s' : Set ((i : ι) → F' i)
⊢ HasFDerivWithinAt (fun f => f i) ?f' s' f

case f'
𝕜 : Type u_1
inst✝³ : NontriviallyNormedField 𝕜
ι : Type u_6
inst✝² : Fintype ι
F' : ι → Type u_7
inst✝¹ : (i : ι) → NormedAddCommGroup (F' i)
inst✝ : (i : ι) → NormedSpace 𝕜 (F' i)
i : ι
f : (i : ι) → F' i
s' : Set ((i : ι) → F' i)
⊢ ((i : ι) → F' i) →L[𝕜] F' i
-- Mathlib/MeasureTheory/Measure/QuasiMeasurePreserving.lean
theorem smul_measure {R : Type*} [SMul R ℝ≥0∞] [IsScalarTower R ℝ≥0∞ ℝ≥0∞]
    (hf : QuasiMeasurePreserving f μa μb) (c : R) : QuasiMeasurePreserving f (c • μa) (c • μb) :=
  ⟨hf.1, by rw [Measure.map_smul]; exact hf.2.smul c⟩

Proof state:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
μa : Measure α
μb : Measure β
f : α → β
R : Type u_5
inst✝¹ : SMul R ℝ≥0∞
inst✝ : IsScalarTower R ℝ≥0∞ ℝ≥0∞
hf : QuasiMeasurePreserving f μa μb
c : R
⊢ map f (c • μa) ≪ c • μb

Tactic:
rw [Measure.map_smul]

Result:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
μa : Measure α
μb : Measure β
f : α → β
R : Type u_5
inst✝¹ : SMul R ℝ≥0∞
inst✝ : IsScalarTower R ℝ≥0∞ ℝ≥0∞
hf : QuasiMeasurePreserving f μa μb
c : R
⊢ c • map f μa ≪ c • μb

Proof state:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
μa : Measure α
μb : Measure β
f : α → β
R : Type u_5
inst✝¹ : SMul R ℝ≥0∞
inst✝ : IsScalarTower R ℝ≥0∞ ℝ≥0∞
hf : QuasiMeasurePreserving f μa μb
c : R
⊢ c • map f μa ≪ c • μb

Tactic:
exact hf.2.smul c

Result:
no goals
-- Mathlib/Computability/PartrecCode.lean
theorem fixed_point {f : Code → Code} (hf : Computable f) : ∃ c : Code, eval (f c) = eval c :=
  let g (x y : ℕ) : Part ℕ := eval (ofNat Code x) x >>= fun b => eval (ofNat Code b) y
  have : Partrec₂ g :=
    (eval_part.comp ((Computable.ofNat _).comp fst) fst).bind
      (eval_part.comp ((Computable.ofNat _).comp snd) (snd.comp fst)).to₂
  let ⟨cg, eg⟩ := exists_code.1 this
  have eg' : ∀ a n, eval cg (Nat.pair a n) = Part.map encode (g a n)

Proof state:
f : Code → Code
hf : Computable f
g : ℕ → ℕ → Part ℕ :=
  fun x y => do
    let b ← (ofNat Code x).eval x
    (ofNat Code b).eval y
this✝ : Partrec₂ g
cg : Code
eg : cg.eval = fun n => (↑(decode n)).bind fun a => Part.map encode ((fun p => g p.1 p.2) a)
eg' : ∀ (a n : ℕ), cg.eval (Nat.pair a n) = Part.map encode (g a n)
F : ℕ → Code := fun x => f (cg.curry x)
this : Computable F
cF : Code
eF : cF.eval = fun n => (↑(decode n)).bind fun a => Part.map encode (↑F a)
eF' : cF.eval (encode cF) = Part.some (encode (F (encode cF)))
n : ℕ
⊢ (f (cg.curry (encode cF))).eval n = (cg.curry (encode cF)).eval n

Tactic:
simp [F, g, eg', eF', Part.map_id']

Result:
no goals

Proof state:
f : Code → Code
hf : Computable f
g : ℕ → ℕ → Part ℕ :=
  fun x y => do
    let b ← (ofNat Code x).eval x
    (ofNat Code b).eval y
this✝ : Partrec₂ g
cg : Code
eg : cg.eval = fun n => (↑(decode n)).bind fun a => Part.map encode ((fun p => g p.1 p.2) a)
eg' : ∀ (a n : ℕ), cg.eval (Nat.pair a n) = Part.map encode (g a n)
F : ℕ → Code := fun x => f (cg.curry x)
this : Computable F
cF : Code
eF : cF.eval = fun n => (↑(decode n)).bind fun a => Part.map encode (↑F a)
⊢ cF.eval (encode cF) = Part.some (encode (F (encode cF)))

Tactic:
simp [eF]

Result:
no goals

Proof state:
f : Code → Code
hf : Computable f
g : ℕ → ℕ → Part ℕ :=
  fun x y => do
    let b ← (ofNat Code x).eval x
    (ofNat Code b).eval y
this : Partrec₂ g
cg : Code
eg : cg.eval = fun n => (↑(decode n)).bind fun a => Part.map encode ((fun p => g p.1 p.2) a)
⊢ ∀ (a n : ℕ), cg.eval (Nat.pair a n) = Part.map encode (g a n)

Tactic:
simp [eg]

Result:
no goals
-- Mathlib/NumberTheory/ModularForms/JacobiTheta/OneVariable.lean
theorem jacobiTheta_two_add (τ : ℂ) : jacobiTheta (2 + τ) = jacobiTheta τ

Proof state:
τ : ℂ
⊢ jacobiTheta (2 + τ) = jacobiTheta τ

Tactic:
simp_rw [jacobiTheta_eq_jacobiTheta₂, add_comm, jacobiTheta₂_add_right]

Result:
no goals
-- Mathlib/GroupTheory/Exponent.lean
theorem exponent_eq_max'_orderOf [Fintype G] :
    exponent G = ((@Finset.univ G _).image orderOf).max' ⟨1, by simp⟩

Proof state:
G : Type u
inst✝¹ : CancelCommMonoid G
inst✝ : Fintype G
⊢ exponent G = iSup orderOf

Tactic:
exact exponent_eq_iSup_orderOf orderOf_pos

Result:
no goals

Proof state:
G : Type u
inst✝¹ : CancelCommMonoid G
inst✝ : Fintype G
⊢ exponent G = (Finset.image orderOf Finset.univ).max' ⋯

Tactic:
rw [← Finset.Nonempty.csSup_eq_max', Finset.coe_image, Finset.coe_univ, Set.image_univ, ← iSup]

Result:
G : Type u
inst✝¹ : CancelCommMonoid G
inst✝ : Fintype G
⊢ exponent G = iSup orderOf

Proof state:
G : Type u
inst✝¹ : CancelCommMonoid G
inst✝ : Fintype G
⊢ 1 ∈ Finset.image orderOf Finset.univ

Tactic:
simp

Result:
no goals
-- Mathlib/LinearAlgebra/DirectSum/Finsupp.lean
theorem finsuppTensorFinsuppRid_self :
    finsuppTensorFinsuppRid R R ι κ = finsuppTensorFinsupp' R ι κ

Proof state:
R : Type u_1
ι : Type u_5
κ : Type u_6
inst✝ : CommSemiring R
⊢ finsuppTensorFinsuppRid R R ι κ = finsuppTensorFinsupp' R ι κ

Tactic:
rw [finsuppTensorFinsupp', finsuppTensorFinsuppLid, finsuppTensorFinsuppRid,
  TensorProduct.lid_eq_rid]

Result:
no goals
-- Mathlib/CategoryTheory/Bicategory/Functor/Pseudofunctor.lean
@[reassoc, to_app]
lemma mapComp_id_left_inv (f : a ⟶ b) : (F.mapComp (𝟙 a) f).inv =
    (F.mapId a).hom ▷ F.map f ≫ (λ_ (F.map f)).hom ≫ F.map₂ (λ_ f).inv

Proof state:
B : Type u₁
inst✝¹ : Bicategory B
C : Type u₂
inst✝ : Bicategory C
F : Pseudofunctor B C
a b : B
f : a ⟶ b
⊢ (F.mapComp (𝟙 a) f).inv = (F.mapId a).hom ▷ F.map f ≫ (λ_ (F.map f)).hom ≫ F.map₂ (λ_ f).inv

Tactic:
simp [mapComp_id_left]

Result:
no goals
-- Mathlib/Data/Rel.lean
theorem core_inter (s t : Set β) : r.core (s ∩ t) = r.core s ∩ r.core t :=
  Set.ext (by simp [mem_core, imp_and, forall_and])

Proof state:
α : Type u_1
β : Type u_2
r : Rel α β
s t : Set β
⊢ ∀ (x : α), x ∈ r.core (s ∩ t) ↔ x ∈ r.core s ∩ r.core t

Tactic:
simp [mem_core, imp_and, forall_and]

Result:
no goals
-- Mathlib/Data/Ordmap/Ordset.lean
theorem merge_nil_left (t : Ordnode α) : merge t nil = t

Proof state:
α : Type u_1
t : Ordnode α
⊢ t.merge nil = t

Tactic:
cases t <;> rfl

Result:
no goals
-- Mathlib/Algebra/Prime/Lemmas.lean
theorem not_irreducible_pow {M} [Monoid M] {x : M} {n : ℕ} (hn : n ≠ 1) :
    ¬ Irreducible (x ^ n)

Proof state:
case zero
M : Type u_3
inst✝ : Monoid M
x : M
hn : 0 ≠ 1
⊢ ¬Irreducible (x ^ 0)

Tactic:
simp

Result:
no goals

Proof state:
case succ
M : Type u_3
inst✝ : Monoid M
x : M
n : ℕ
hn : n + 1 ≠ 1
h₁ : ¬IsUnit (x ^ (n + 1))
h₂ : ∀ (a b : M), x ^ (n + 1) = a * b → IsUnit a ∨ IsUnit b
this : IsUnit x
⊢ False

Tactic:
exact h₁ (this.pow _)

Result:
no goals

Proof state:
case succ
M : Type u_3
inst✝ : Monoid M
x : M
n : ℕ
hn : n + 1 ≠ 1
h₁ : ¬IsUnit (x ^ (n + 1))
h₂ : ∀ (a b : M), x ^ (n + 1) = a * b → IsUnit a ∨ IsUnit b
⊢ False

Tactic:
have := h₂ _ _ (pow_succ _ _)

Result:
case succ
M : Type u_3
inst✝ : Monoid M
x : M
n : ℕ
hn : n + 1 ≠ 1
h₁ : ¬IsUnit (x ^ (n + 1))
h₂ : ∀ (a b : M), x ^ (n + 1) = a * b → IsUnit a ∨ IsUnit b
this : IsUnit (x ^ n) ∨ IsUnit x
⊢ False

Proof state:
case succ
M : Type u_3
inst✝ : Monoid M
x : M
n : ℕ
hn : n + 1 ≠ 1
⊢ ¬Irreducible (x ^ (n + 1))

Tactic:
intro ⟨h₁, h₂⟩

Result:
case succ
M : Type u_3
inst✝ : Monoid M
x : M
n : ℕ
hn : n + 1 ≠ 1
h₁ : ¬IsUnit (x ^ (n + 1))
h₂ : ∀ (a b : M), x ^ (n + 1) = a * b → IsUnit a ∨ IsUnit b
⊢ False

Proof state:
M : Type u_3
inst✝ : Monoid M
x : M
n : ℕ
hn : n ≠ 1
⊢ ¬Irreducible (x ^ n)

Tactic:
cases n with
| zero => simp
| succ n =>
  intro ⟨h₁, h₂⟩
  have := h₂ _ _ (pow_succ _ _)
  rw [isUnit_pow_iff (Nat.succ_ne_succ.mp hn), or_self] at this
  exact h₁ (this.pow _)

Result:
no goals

Proof state:
case succ
M : Type u_3
inst✝ : Monoid M
x : M
n : ℕ
hn : n + 1 ≠ 1
h₁ : ¬IsUnit (x ^ (n + 1))
h₂ : ∀ (a b : M), x ^ (n + 1) = a * b → IsUnit a ∨ IsUnit b
this : IsUnit (x ^ n) ∨ IsUnit x
⊢ False

Tactic:
rw [isUnit_pow_iff (Nat.succ_ne_succ.mp hn), or_self] at this

Result:
case succ
M : Type u_3
inst✝ : Monoid M
x : M
n : ℕ
hn : n + 1 ≠ 1
h₁ : ¬IsUnit (x ^ (n + 1))
h₂ : ∀ (a b : M), x ^ (n + 1) = a * b → IsUnit a ∨ IsUnit b
this : IsUnit x
⊢ False
-- Mathlib/Topology/DiscreteQuotient.lean
theorem proj_bot_inj [DiscreteTopology X] {x y : X} : proj ⊥ x = proj ⊥ y ↔ x = y

Proof state:
X : Type u_2
inst✝¹ : TopologicalSpace X
inst✝ : DiscreteTopology X
x y : X
⊢ ⊥.proj x = ⊥.proj y ↔ x = y

Tactic:
simp

Result:
no goals
-- Mathlib/Analysis/InnerProductSpace/Basic.lean
theorem real_inner_add_add_self (x y : F) :
    ⟪x + y, x + y⟫_ℝ = ⟪x, x⟫_ℝ + 2 * ⟪x, y⟫_ℝ + ⟪y, y⟫_ℝ

Proof state:
F : Type u_3
inst✝¹ : SeminormedAddCommGroup F
inst✝ : InnerProductSpace ℝ F
x y : F
⊢ (starRingEnd ℝ) ⟪x, y⟫_ℝ = ⟪x, y⟫_ℝ

Tactic:
rfl

Result:
no goals

Proof state:
F : Type u_3
inst✝¹ : SeminormedAddCommGroup F
inst✝ : InnerProductSpace ℝ F
x y : F
this : ⟪y, x⟫_ℝ = ⟪x, y⟫_ℝ
⊢ ⟪x + y, x + y⟫_ℝ = ⟪x, x⟫_ℝ + 2 * ⟪x, y⟫_ℝ + ⟪y, y⟫_ℝ

Tactic:
simp only [inner_add_add_self, this, add_left_inj]

Result:
F : Type u_3
inst✝¹ : SeminormedAddCommGroup F
inst✝ : InnerProductSpace ℝ F
x y : F
this : ⟪y, x⟫_ℝ = ⟪x, y⟫_ℝ
⊢ ⟪x, x⟫_ℝ + ⟪x, y⟫_ℝ + ⟪x, y⟫_ℝ = ⟪x, x⟫_ℝ + 2 * ⟪x, y⟫_ℝ

Proof state:
F : Type u_3
inst✝¹ : SeminormedAddCommGroup F
inst✝ : InnerProductSpace ℝ F
x y : F
⊢ ⟪y, x⟫_ℝ = ⟪x, y⟫_ℝ

Tactic:
rw [← inner_conj_symm]

Result:
F : Type u_3
inst✝¹ : SeminormedAddCommGroup F
inst✝ : InnerProductSpace ℝ F
x y : F
⊢ (starRingEnd ℝ) ⟪x, y⟫_ℝ = ⟪x, y⟫_ℝ

Proof state:
F : Type u_3
inst✝¹ : SeminormedAddCommGroup F
inst✝ : InnerProductSpace ℝ F
x y : F
⊢ ⟪x + y, x + y⟫_ℝ = ⟪x, x⟫_ℝ + 2 * ⟪x, y⟫_ℝ + ⟪y, y⟫_ℝ

Tactic:
have : ⟪y, x⟫_ℝ = ⟪x, y⟫_ℝ := by rw [← inner_conj_symm]; rfl

Result:
F : Type u_3
inst✝¹ : SeminormedAddCommGroup F
inst✝ : InnerProductSpace ℝ F
x y : F
this : ⟪y, x⟫_ℝ = ⟪x, y⟫_ℝ
⊢ ⟪x + y, x + y⟫_ℝ = ⟪x, x⟫_ℝ + 2 * ⟪x, y⟫_ℝ + ⟪y, y⟫_ℝ

Proof state:
F : Type u_3
inst✝¹ : SeminormedAddCommGroup F
inst✝ : InnerProductSpace ℝ F
x y : F
this : ⟪y, x⟫_ℝ = ⟪x, y⟫_ℝ
⊢ ⟪x, x⟫_ℝ + ⟪x, y⟫_ℝ + ⟪x, y⟫_ℝ = ⟪x, x⟫_ℝ + 2 * ⟪x, y⟫_ℝ

Tactic:
ring

Result:
no goals
-- Mathlib/Data/Finset/Card.lean
theorem exists_ne_map_eq_of_card_lt_of_maps_to {t : Finset β} (hc : #t < #s) {f : α → β}
    (hf : ∀ a ∈ s, f a ∈ t) : ∃ x ∈ s, ∃ y ∈ s, x ≠ y ∧ f x = f y

Proof state:
α : Type u_1
β : Type u_2
s : Finset α
t : Finset β
hc : #t < #s
f : α → β
hf : ∀ a ∈ s, f a ∈ t
⊢ ∃ x ∈ s, ∃ y ∈ s, x ≠ y ∧ f x = f y

Tactic:
by_contra! hz

Result:
α : Type u_1
β : Type u_2
s : Finset α
t : Finset β
hc : #t < #s
f : α → β
hf : ∀ a ∈ s, f a ∈ t
hz : ∀ x ∈ s, ∀ y ∈ s, x ≠ y → f x ≠ f y
⊢ False

Proof state:
α : Type u_1
β : Type u_2
s : Finset α
t : Finset β
hc : #t < #s
f : α → β
hf : ∀ a ∈ s, f a ∈ t
hz : ∀ x ∈ s, ∀ y ∈ s, x ≠ y → f x ≠ f y
⊢ False

Tactic:
refine hc.not_le (card_le_card_of_injOn f hf ?_)

Result:
α : Type u_1
β : Type u_2
s : Finset α
t : Finset β
hc : #t < #s
f : α → β
hf : ∀ a ∈ s, f a ∈ t
hz : ∀ x ∈ s, ∀ y ∈ s, x ≠ y → f x ≠ f y
⊢ Set.InjOn f ↑s

Proof state:
α : Type u_1
β : Type u_2
s : Finset α
t : Finset β
hc : #t < #s
f : α → β
hf : ∀ a ∈ s, f a ∈ t
hz : ∀ x ∈ s, ∀ y ∈ s, x ≠ y → f x ≠ f y
⊢ Set.InjOn f ↑s

Tactic:
intro x hx y hy

Result:
α : Type u_1
β : Type u_2
s : Finset α
t : Finset β
hc : #t < #s
f : α → β
hf : ∀ a ∈ s, f a ∈ t
hz : ∀ x ∈ s, ∀ y ∈ s, x ≠ y → f x ≠ f y
x : α
hx : x ∈ ↑s
y : α
hy : y ∈ ↑s
⊢ f x = f y → x = y

Proof state:
α : Type u_1
β : Type u_2
s : Finset α
t : Finset β
hc : #t < #s
f : α → β
hf : ∀ a ∈ s, f a ∈ t
⊢ ∃ x ∈ s, ∃ y ∈ s, x ≠ y ∧ f x = f y

Tactic:
classical
by_contra! hz
refine hc.not_le (card_le_card_of_injOn f hf ?_)
intro x hx y hy
contrapose
exact hz x hx y hy

Result:
no goals

Proof state:
α : Type u_1
β : Type u_2
s : Finset α
t : Finset β
hc : #t < #s
f : α → β
hf : ∀ a ∈ s, f a ∈ t
hz : ∀ x ∈ s, ∀ y ∈ s, x ≠ y → f x ≠ f y
x : α
hx : x ∈ ↑s
y : α
hy : y ∈ ↑s
⊢ ¬x = y → ¬f x = f y

Tactic:
exact hz x hx y hy

Result:
no goals

Proof state:
α : Type u_1
β : Type u_2
s : Finset α
t : Finset β
hc : #t < #s
f : α → β
hf : ∀ a ∈ s, f a ∈ t
hz : ∀ x ∈ s, ∀ y ∈ s, x ≠ y → f x ≠ f y
x : α
hx : x ∈ ↑s
y : α
hy : y ∈ ↑s
⊢ f x = f y → x = y

Tactic:
contrapose

Result:
α : Type u_1
β : Type u_2
s : Finset α
t : Finset β
hc : #t < #s
f : α → β
hf : ∀ a ∈ s, f a ∈ t
hz : ∀ x ∈ s, ∀ y ∈ s, x ≠ y → f x ≠ f y
x : α
hx : x ∈ ↑s
y : α
hy : y ∈ ↑s
⊢ ¬x = y → ¬f x = f y
-- Mathlib/Combinatorics/SimpleGraph/Connectivity/WalkDecomp.lean
lemma snd_takeUntil (hsu : w ≠ u) (p : G.Walk u v) (h : w ∈ p.support) :
    (p.takeUntil w h).snd = p.snd

Proof state:
V : Type u
G : SimpleGraph V
v w u : V
inst✝ : DecidableEq V
hsu : w ≠ u
p : G.Walk u v
h : w ∈ p.support
⊢ 1 ≤ (p.takeUntil w h).length

Tactic:
by_contra! hc

Result:
V : Type u
G : SimpleGraph V
v w u : V
inst✝ : DecidableEq V
hsu : w ≠ u
p : G.Walk u v
h : w ∈ p.support
hc : (p.takeUntil w h).length < 1
⊢ False

Proof state:
V : Type u
G : SimpleGraph V
v w u : V
inst✝ : DecidableEq V
hsu : w ≠ u
p : G.Walk u v
h : w ∈ p.support
⊢ (p.takeUntil w h).snd = p.snd

Tactic:
apply p.getVert_takeUntil h

Result:
V : Type u
G : SimpleGraph V
v w u : V
inst✝ : DecidableEq V
hsu : w ≠ u
p : G.Walk u v
h : w ∈ p.support
⊢ 1 ≤ (p.takeUntil w h).length

Proof state:
V : Type u
G : SimpleGraph V
v w u : V
inst✝ : DecidableEq V
hsu : w ≠ u
p : G.Walk u v
h : w ∈ p.support
hc : u = w
⊢ False

Tactic:
exact hsu hc.symm

Result:
no goals

Proof state:
V : Type u
G : SimpleGraph V
v w u : V
inst✝ : DecidableEq V
hsu : w ≠ u
p : G.Walk u v
h : w ∈ p.support
hc : (p.takeUntil w h).length < 1
⊢ False

Tactic:
simp only [Nat.lt_one_iff, ← nil_iff_length_eq, nil_takeUntil] at hc

Result:
V : Type u
G : SimpleGraph V
v w u : V
inst✝ : DecidableEq V
hsu : w ≠ u
p : G.Walk u v
h : w ∈ p.support
hc : u = w
⊢ False
-- Mathlib/Algebra/Order/Interval/Set/Group.lean
theorem sub_mem_Icc_zero_iff_right : b - a ∈ Icc 0 b ↔ a ∈ Icc 0 b

Proof state:
α : Type u_1
inst✝ : OrderedAddCommGroup α
a b : α
⊢ b - a ∈ Icc 0 b ↔ a ∈ Icc 0 b

Tactic:
simp only [sub_mem_Icc_iff_right, sub_self, sub_zero]

Result:
no goals