harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/Algebra/Order/Chebyshev.lean
/-- Special case of **Jensen's inequality** for sums of powers. -/
lemma pow_sum_div_card_le_sum_pow (hf : ∀ i ∈ s, 0 ≤ f i) (n : ℕ) :
    (∑ i ∈ s, f i) ^ (n + 1) / #s ^ n ≤ ∑ i ∈ s, f i ^ (n + 1)

Proof state:
case inr
ι : Type u_1
α : Type u_2
inst✝¹ : LinearOrderedSemifield α
inst✝ : ExistsAddOfLE α
s : Finset ι
f : ι → α
hf : ∀ i ∈ s, 0 ≤ f i
n : ℕ
hs : s.Nonempty
⊢ (∑ i ∈ s, f i) ^ (n + 1) / ↑(#s) ^ n ≤ ∑ i ∈ s, f i ^ (n + 1)

Tactic:
rw [div_le_iff₀' (by positivity)]

Result:
case inr
ι : Type u_1
α : Type u_2
inst✝¹ : LinearOrderedSemifield α
inst✝ : ExistsAddOfLE α
s : Finset ι
f : ι → α
hf : ∀ i ∈ s, 0 ≤ f i
n : ℕ
hs : s.Nonempty
⊢ (∑ i ∈ s, f i) ^ (n + 1) ≤ ↑(#s) ^ n * ∑ i ∈ s, f i ^ (n + 1)

Proof state:
case inr
ι : Type u_1
α : Type u_2
inst✝¹ : LinearOrderedSemifield α
inst✝ : ExistsAddOfLE α
s : Finset ι
f : ι → α
hf : ∀ i ∈ s, 0 ≤ f i
n : ℕ
hs : s.Nonempty
⊢ (∑ i ∈ s, f i) ^ (n + 1) ≤ ↑(#s) ^ n * ∑ i ∈ s, f i ^ (n + 1)

Tactic:
exact pow_sum_le_card_mul_sum_pow hf _

Result:
no goals

Proof state:
ι : Type u_1
α : Type u_2
inst✝¹ : LinearOrderedSemifield α
inst✝ : ExistsAddOfLE α
s : Finset ι
f : ι → α
hf : ∀ i ∈ s, 0 ≤ f i
n : ℕ
hs : s.Nonempty
⊢ 0 < ↑(#s) ^ n

Tactic:
positivity

Result:
no goals

Proof state:
case inl
ι : Type u_1
α : Type u_2
inst✝¹ : LinearOrderedSemifield α
inst✝ : ExistsAddOfLE α
f : ι → α
n : ℕ
hf : ∀ i ∈ ∅, 0 ≤ f i
⊢ (∑ i ∈ ∅, f i) ^ (n + 1) / ↑(#∅) ^ n ≤ ∑ i ∈ ∅, f i ^ (n + 1)

Tactic:
simp

Result:
no goals

Proof state:
ι : Type u_1
α : Type u_2
inst✝¹ : LinearOrderedSemifield α
inst✝ : ExistsAddOfLE α
s : Finset ι
f : ι → α
hf : ∀ i ∈ s, 0 ≤ f i
n : ℕ
⊢ (∑ i ∈ s, f i) ^ (n + 1) / ↑(#s) ^ n ≤ ∑ i ∈ s, f i ^ (n + 1)

Tactic:
obtain rfl | hs := s.eq_empty_or_nonempty

Result:
case inl
ι : Type u_1
α : Type u_2
inst✝¹ : LinearOrderedSemifield α
inst✝ : ExistsAddOfLE α
f : ι → α
n : ℕ
hf : ∀ i ∈ ∅, 0 ≤ f i
⊢ (∑ i ∈ ∅, f i) ^ (n + 1) / ↑(#∅) ^ n ≤ ∑ i ∈ ∅, f i ^ (n + 1)

case inr
ι : Type u_1
α : Type u_2
inst✝¹ : LinearOrderedSemifield α
inst✝ : ExistsAddOfLE α
s : Finset ι
f : ι → α
hf : ∀ i ∈ s, 0 ≤ f i
n : ℕ
hs : s.Nonempty
⊢ (∑ i ∈ s, f i) ^ (n + 1) / ↑(#s) ^ n ≤ ∑ i ∈ s, f i ^ (n + 1)
-- Mathlib/Algebra/Group/Units/Defs.lean
@[to_additive (attr := simp, norm_cast)]
lemma val_div_eq_div_val : ∀ u₁ u₂ : αˣ, ↑(u₁ / u₂) = (u₁ / u₂ : α)

Proof state:
α : Type u
inst✝ : DivisionMonoid α
⊢ ∀ (u₁ u₂ : αˣ), ↑(u₁ / u₂) = ↑u₁ / ↑u₂

Tactic:
simp [div_eq_mul_inv]

Result:
no goals
-- Mathlib/.lake/packages/batteries/Batteries/Data/String/Lemmas.lean
theorem split_of_valid (s p) : split s p = (List.splitOnP p s.1).map mk

Proof state:
s : String
p : Char → Bool
⊢ s.split p = List.map mk (List.splitOnP p s.data)

Tactic:
simpa [split] using splitAux_of_valid p [] [] s.1 []

Result:
no goals
-- Mathlib/Analysis/ConstantSpeed.lean
theorem hasConstantSpeedOnWith_of_subsingleton (f : ℝ → E) {s : Set ℝ} (hs : s.Subsingleton)
    (l : ℝ≥0) : HasConstantSpeedOnWith f s l

Proof state:
E : Type u_2
inst✝ : PseudoEMetricSpace E
f : ℝ → E
s : Set ℝ
hs : s.Subsingleton
l : ℝ≥0
x : ℝ
hx : x ∈ s
y : ℝ
hy : y ∈ s
⊢ eVariationOn f (s ∩ Icc x y) = ENNReal.ofReal (↑l * (y - x))

Tactic:
cases hs hx hy

Result:
case refl
E : Type u_2
inst✝ : PseudoEMetricSpace E
f : ℝ → E
s : Set ℝ
hs : s.Subsingleton
l : ℝ≥0
x : ℝ
hx hy : x ∈ s
⊢ eVariationOn f (s ∩ Icc x x) = ENNReal.ofReal (↑l * (x - x))

Proof state:
case refl
E : Type u_2
inst✝ : PseudoEMetricSpace E
f : ℝ → E
s : Set ℝ
hs : s.Subsingleton
l : ℝ≥0
x : ℝ
hx hy : x ∈ s
⊢ eVariationOn f (s ∩ Icc x x) = ENNReal.ofReal (↑l * (x - x))

Tactic:
rw [eVariationOn.subsingleton f (fun y hy z hz => hs hy.1 hz.1 : (s ∩ Icc x x).Subsingleton)]

Result:
case refl
E : Type u_2
inst✝ : PseudoEMetricSpace E
f : ℝ → E
s : Set ℝ
hs : s.Subsingleton
l : ℝ≥0
x : ℝ
hx hy : x ∈ s
⊢ 0 = ENNReal.ofReal (↑l * (x - x))

Proof state:
E : Type u_2
inst✝ : PseudoEMetricSpace E
f : ℝ → E
s : Set ℝ
hs : s.Subsingleton
l : ℝ≥0
⊢ HasConstantSpeedOnWith f s l

Tactic:
rintro x hx y hy

Result:
E : Type u_2
inst✝ : PseudoEMetricSpace E
f : ℝ → E
s : Set ℝ
hs : s.Subsingleton
l : ℝ≥0
x : ℝ
hx : x ∈ s
y : ℝ
hy : y ∈ s
⊢ eVariationOn f (s ∩ Icc x y) = ENNReal.ofReal (↑l * (y - x))

Proof state:
case refl
E : Type u_2
inst✝ : PseudoEMetricSpace E
f : ℝ → E
s : Set ℝ
hs : s.Subsingleton
l : ℝ≥0
x : ℝ
hx hy : x ∈ s
⊢ 0 = ENNReal.ofReal (↑l * (x - x))

Tactic:
simp only [sub_self, mul_zero, ENNReal.ofReal_zero]

Result:
no goals
-- Mathlib/Analysis/SpecialFunctions/Trigonometric/Angle.lean
theorem toReal_injective : Function.Injective toReal

Proof state:
case h
ψ : Angle
x✝ : ℝ
h : (↑x✝).toReal = ψ.toReal
⊢ ↑x✝ = ψ

Tactic:
induction ψ using Real.Angle.induction_on

Result:
case h.h
x✝¹ x✝ : ℝ
h : (↑x✝¹).toReal = (↑x✝).toReal
⊢ ↑x✝¹ = ↑x✝

Proof state:
case h.h
x✝¹ x✝ : ℝ
h : (↑x✝¹).toReal = (↑x✝).toReal
⊢ ↑x✝¹ = ↑x✝

Tactic:
simpa [toReal_coe, toIocMod_eq_toIocMod, zsmul_eq_mul, mul_comm _ (2 * π), ←
  angle_eq_iff_two_pi_dvd_sub, eq_comm] using h

Result:
no goals

Proof state:
⊢ Function.Injective toReal

Tactic:
intro θ ψ h

Result:
θ ψ : Angle
h : θ.toReal = ψ.toReal
⊢ θ = ψ

Proof state:
θ ψ : Angle
h : θ.toReal = ψ.toReal
⊢ θ = ψ

Tactic:
induction θ using Real.Angle.induction_on

Result:
case h
ψ : Angle
x✝ : ℝ
h : (↑x✝).toReal = ψ.toReal
⊢ ↑x✝ = ψ
-- Mathlib/Order/Interval/Finset/Box.lean
@[simp] lemma mem_box : ∀ {n}, x ∈ box n ↔ max x.1.natAbs x.2.natAbs = n
  | 0 => by simp [Prod.ext_iff]
  | n + 1 => by
    simp [box_succ_eq_sdiff, Prod.le_def]
    omega

Proof state:
x : ℤ × ℤ
n : ℕ
⊢ x ∈ box (n + 1) ↔ x.1.natAbs ⊔ x.2.natAbs = n + 1

Tactic:
simp [box_succ_eq_sdiff, Prod.le_def]

Result:
x : ℤ × ℤ
n : ℕ
⊢ ((-1 ≤ x.1 + ↑n ∧ -1 ≤ x.2 + ↑n) ∧ x.1 ≤ ↑n + 1 ∧ x.2 ≤ ↑n + 1) ∧ (-↑n ≤ x.1 → -↑n ≤ x.2 → x.1 ≤ ↑n → ↑n < x.2) ↔
    x.1.natAbs ⊔ x.2.natAbs = n + 1

Proof state:
x : ℤ × ℤ
⊢ x ∈ box 0 ↔ x.1.natAbs ⊔ x.2.natAbs = 0

Tactic:
simp [Prod.ext_iff]

Result:
no goals

Proof state:
x : ℤ × ℤ
n : ℕ
⊢ ((-1 ≤ x.1 + ↑n ∧ -1 ≤ x.2 + ↑n) ∧ x.1 ≤ ↑n + 1 ∧ x.2 ≤ ↑n + 1) ∧ (-↑n ≤ x.1 → -↑n ≤ x.2 → x.1 ≤ ↑n → ↑n < x.2) ↔
    x.1.natAbs ⊔ x.2.natAbs = n + 1

Tactic:
omega

Result:
no goals
-- Mathlib/LinearAlgebra/Dimension/DivisionRing.lean
theorem rank_quotient_add_rank_of_divisionRing (p : Submodule K V) :
    Module.rank K (V ⧸ p) + Module.rank K p = Module.rank K V

Proof state:
K : Type u
V : Type v
inst✝² : DivisionRing K
inst✝¹ : AddCommGroup V
inst✝ : Module K V
p : Submodule K V
⊢ Module.rank K (V ⧸ p) + Module.rank K ↥p = Module.rank K V

Tactic:
let ⟨f⟩ := quotient_prod_linearEquiv p

Result:
K : Type u
V : Type v
inst✝² : DivisionRing K
inst✝¹ : AddCommGroup V
inst✝ : Module K V
p : Submodule K V
f : ((V ⧸ p) × ↥p) ≃ₗ[K] V
⊢ Module.rank K (V ⧸ p) + Module.rank K ↥p = Module.rank K V

Proof state:
K : Type u
V : Type v
inst✝² : DivisionRing K
inst✝¹ : AddCommGroup V
inst✝ : Module K V
p : Submodule K V
f : ((V ⧸ p) × ↥p) ≃ₗ[K] V
⊢ Module.rank K (V ⧸ p) + Module.rank K ↥p = Module.rank K V

Tactic:
exact rank_prod'.symm.trans f.rank_eq

Result:
no goals

Proof state:
K : Type u
V : Type v
inst✝² : DivisionRing K
inst✝¹ : AddCommGroup V
inst✝ : Module K V
p : Submodule K V
⊢ Module.rank K (V ⧸ p) + Module.rank K ↥p = Module.rank K V

Tactic:
classical
  let ⟨f⟩ := quotient_prod_linearEquiv p
  exact rank_prod'.symm.trans f.rank_eq

Result:
no goals
-- Mathlib/Analysis/SpecialFunctions/ContinuousFunctionalCalculus/Rpow/Basic.lean
lemma sqrt_rpow_nnreal {a : A} {x : ℝ≥0} : sqrt (a ^ (x : ℝ)) = a ^ (x / 2 : ℝ)

Proof state:
case pos
A : Type u_1
inst✝⁷ : PartialOrder A
inst✝⁶ : Ring A
inst✝⁵ : StarRing A
inst✝⁴ : TopologicalSpace A
inst✝³ : Algebra ℝ A
inst✝² : ContinuousFunctionalCalculus ℝ≥0 fun a => 0 ≤ a
inst✝¹ : IsTopologicalRing A
inst✝ : T2Space A
a : A
x : ℝ≥0
htriv : 0 ≤ a
hx : x = 0
⊢ sqrt (a ^ ↑x) = a ^ (↑x / 2)

case neg
A : Type u_1
inst✝⁷ : PartialOrder A
inst✝⁶ : Ring A
inst✝⁵ : StarRing A
inst✝⁴ : TopologicalSpace A
inst✝³ : Algebra ℝ A
inst✝² : ContinuousFunctionalCalculus ℝ≥0 fun a => 0 ≤ a
inst✝¹ : IsTopologicalRing A
inst✝ : T2Space A
a : A
x : ℝ≥0
htriv : 0 ≤ a
hx : ¬x = 0
⊢ sqrt (a ^ ↑x) = a ^ (↑x / 2)

Tactic:
case pos => simp [hx, rpow_zero _ htriv]

Result:
case neg
A : Type u_1
inst✝⁷ : PartialOrder A
inst✝⁶ : Ring A
inst✝⁵ : StarRing A
inst✝⁴ : TopologicalSpace A
inst✝³ : Algebra ℝ A
inst✝² : ContinuousFunctionalCalculus ℝ≥0 fun a => 0 ≤ a
inst✝¹ : IsTopologicalRing A
inst✝ : T2Space A
a : A
x : ℝ≥0
htriv : 0 ≤ a
hx : ¬x = 0
⊢ sqrt (a ^ ↑x) = a ^ (↑x / 2)

Proof state:
A : Type u_1
inst✝⁷ : PartialOrder A
inst✝⁶ : Ring A
inst✝⁵ : StarRing A
inst✝⁴ : TopologicalSpace A
inst✝³ : Algebra ℝ A
inst✝² : ContinuousFunctionalCalculus ℝ≥0 fun a => 0 ≤ a
inst✝¹ : IsTopologicalRing A
inst✝ : T2Space A
a : A
x : ℝ≥0
htriv : 0 ≤ a
hx : ¬x = 0
h₁ : 0 < x
h₂ : ↑x / 2 = ↑(x / 2)
h₃ : 0 < x / 2
⊢ sqrt (a ^ ↑x) = a ^ (↑x / 2)

Tactic:
rw [← nnrpow_eq_rpow h₁, h₂, ← nnrpow_eq_rpow h₃, sqrt_nnrpow (A := A)]

Result:
no goals

Proof state:
A : Type u_1
inst✝⁷ : PartialOrder A
inst✝⁶ : Ring A
inst✝⁵ : StarRing A
inst✝⁴ : TopologicalSpace A
inst✝³ : Algebra ℝ A
inst✝² : ContinuousFunctionalCalculus ℝ≥0 fun a => 0 ≤ a
inst✝¹ : IsTopologicalRing A
inst✝ : T2Space A
a : A
x : ℝ≥0
htriv : ¬0 ≤ a
⊢ sqrt (a ^ ↑x) = a ^ (↑x / 2)

Tactic:
simp [sqrt_eq_cfc, rpow_def, cfc_apply_of_not_predicate a htriv]

Result:
no goals
-- Mathlib/LinearAlgebra/Multilinear/Pi.lean
theorem piFamily_zero :
    piFamily (0 : Π (p : Π i, κ i), MultilinearMap R (fun i ↦ M i (p i)) (N p)) = 0

Proof state:
case H.h
ι : Type uι
κ : ι → Type uκ
R : Type uR
M : (i : ι) → κ i → Type uM
N : ((i : ι) → κ i) → Type uN
inst✝⁴ : Semiring R
inst✝³ : (i : ι) → (k : κ i) → AddCommMonoid (M i k)
inst✝² : (p : (i : ι) → κ i) → AddCommMonoid (N p)
inst✝¹ : (i : ι) → (k : κ i) → Module R (M i k)
inst✝ : (p : (i : ι) → κ i) → Module R (N p)
x✝¹ : (i : ι) → (j : κ i) → M i j
x✝ : (i : ι) → κ i
⊢ (piFamily 0) x✝¹ x✝ = 0 x✝¹ x✝

Tactic:
simp

Result:
no goals

Proof state:
ι : Type uι
κ : ι → Type uκ
R : Type uR
M : (i : ι) → κ i → Type uM
N : ((i : ι) → κ i) → Type uN
inst✝⁴ : Semiring R
inst✝³ : (i : ι) → (k : κ i) → AddCommMonoid (M i k)
inst✝² : (p : (i : ι) → κ i) → AddCommMonoid (N p)
inst✝¹ : (i : ι) → (k : κ i) → Module R (M i k)
inst✝ : (p : (i : ι) → κ i) → Module R (N p)
⊢ piFamily 0 = 0

Tactic:
ext

Result:
case H.h
ι : Type uι
κ : ι → Type uκ
R : Type uR
M : (i : ι) → κ i → Type uM
N : ((i : ι) → κ i) → Type uN
inst✝⁴ : Semiring R
inst✝³ : (i : ι) → (k : κ i) → AddCommMonoid (M i k)
inst✝² : (p : (i : ι) → κ i) → AddCommMonoid (N p)
inst✝¹ : (i : ι) → (k : κ i) → Module R (M i k)
inst✝ : (p : (i : ι) → κ i) → Module R (N p)
x✝¹ : (i : ι) → (j : κ i) → M i j
x✝ : (i : ι) → κ i
⊢ (piFamily 0) x✝¹ x✝ = 0 x✝¹ x✝
-- Mathlib/.lake/packages/lean4/src/lean/Init/Internal/Order/Basic.lean
theorem fix_induct {f : α → α} (hf : monotone f)
    (motive : α → Prop) (hadm: admissible motive)
    (h : ∀ x, motive x → motive (f x)) : motive (fix f hf)

Proof state:
α : Sort u
inst✝ : CCPO α
f : α → α
hf : monotone f
motive : α → Prop
hadm : admissible motive
h : ∀ (x : α), motive x → motive (f x)
x : α
hiterates : iterates f x
⊢ motive x

Tactic:
induction hiterates with
| @step x hiter ih => apply h x ih
| @sup c hchain hiter ih => apply hadm c hchain ih

Result:
no goals

Proof state:
case step
α : Sort u
inst✝ : CCPO α
f : α → α
hf : monotone f
motive : α → Prop
hadm : admissible motive
h : ∀ (x : α), motive x → motive (f x)
x✝ x : α
hiter : iterates f x
ih : motive x
⊢ motive (f x)

Tactic:
apply h x ih

Result:
no goals

Proof state:
α : Sort u
inst✝ : CCPO α
f : α → α
hf : monotone f
motive : α → Prop
hadm : admissible motive
h : ∀ (x : α), motive x → motive (f x)
⊢ ∀ (x : α), iterates f x → motive x

Tactic:
intro x hiterates

Result:
α : Sort u
inst✝ : CCPO α
f : α → α
hf : monotone f
motive : α → Prop
hadm : admissible motive
h : ∀ (x : α), motive x → motive (f x)
x : α
hiterates : iterates f x
⊢ motive x

Proof state:
case sup
α : Sort u
inst✝ : CCPO α
f : α → α
hf : monotone f
motive : α → Prop
hadm : admissible motive
h : ∀ (x : α), motive x → motive (f x)
x : α
c : α → Prop
hchain : chain c
hiter : ∀ (x : α), c x → iterates f x
ih : ∀ (x : α), c x → motive x
⊢ motive (csup c)

Tactic:
apply hadm c hchain ih

Result:
no goals

Proof state:
α : Sort u
inst✝ : CCPO α
f : α → α
hf : monotone f
motive : α → Prop
hadm : admissible motive
h : ∀ (x : α), motive x → motive (f x)
⊢ motive (fix f hf)

Tactic:
apply hadm _ (chain_iterates hf)

Result:
α : Sort u
inst✝ : CCPO α
f : α → α
hf : monotone f
motive : α → Prop
hadm : admissible motive
h : ∀ (x : α), motive x → motive (f x)
⊢ ∀ (x : α), iterates f x → motive x
-- Mathlib/GroupTheory/Perm/Cycle/Concrete.lean
theorem isCycle_formPerm (s : Cycle α) (h : Nodup s) (hn : Nontrivial s) :
    IsCycle (formPerm s h)

Proof state:
case h
α : Type u_1
inst✝ : DecidableEq α
a✝ : List α
h : Nodup (Quot.mk (⇑(IsRotated.setoid α)) a✝)
hn : Nontrivial (Quot.mk (⇑(IsRotated.setoid α)) a✝)
⊢ (formPerm (Quot.mk (⇑(IsRotated.setoid α)) a✝) h).IsCycle

Tactic:
exact List.isCycle_formPerm h (length_nontrivial hn)

Result:
no goals

Proof state:
α : Type u_1
inst✝ : DecidableEq α
s : Cycle α
h : s.Nodup
hn : s.Nontrivial
⊢ (s.formPerm h).IsCycle

Tactic:
induction s using Quot.inductionOn

Result:
case h
α : Type u_1
inst✝ : DecidableEq α
a✝ : List α
h : Nodup (Quot.mk (⇑(IsRotated.setoid α)) a✝)
hn : Nontrivial (Quot.mk (⇑(IsRotated.setoid α)) a✝)
⊢ (formPerm (Quot.mk (⇑(IsRotated.setoid α)) a✝) h).IsCycle
-- Mathlib/Data/List/SplitBy.lean
theorem flatten_splitByLoop {r : α → α → Bool} {l : List α} {a : α} {g : List α} :
    (splitBy.loop r l a g []).flatten = g.reverse ++ a :: l

Proof state:
case cons
α : Type u_1
r : α → α → Bool
b : α
l : List α
IH : ∀ {a : α} {g : List α}, (splitBy.loop r l a g []).flatten = g.reverse ++ a :: l
a : α
g : List α
⊢ (match r a b with
      | true => splitBy.loop r l b (a :: g) []
      | false => [(a :: g).reverse].reverse ++ splitBy.loop r l b [] []).flatten =
    g.reverse ++ a :: b :: l

Tactic:
split <;> simp [IH]

Result:
no goals

Proof state:
α : Type u_1
r : α → α → Bool
l : List α
a : α
g : List α
⊢ (splitBy.loop r l a g []).flatten = g.reverse ++ a :: l

Tactic:
induction l generalizing a g with
| nil => simp [splitBy.loop]
| cons b l IH =>
  rw [splitBy.loop, splitByLoop_eq_append [_]]
  split <;> simp [IH]

Result:
no goals

Proof state:
case nil
α : Type u_1
r : α → α → Bool
a : α
g : List α
⊢ (splitBy.loop r [] a g []).flatten = g.reverse ++ [a]

Tactic:
simp [splitBy.loop]

Result:
no goals

Proof state:
case cons
α : Type u_1
r : α → α → Bool
b : α
l : List α
IH : ∀ {a : α} {g : List α}, (splitBy.loop r l a g []).flatten = g.reverse ++ a :: l
a : α
g : List α
⊢ (splitBy.loop r (b :: l) a g []).flatten = g.reverse ++ a :: b :: l

Tactic:
rw [splitBy.loop, splitByLoop_eq_append [_]]

Result:
case cons
α : Type u_1
r : α → α → Bool
b : α
l : List α
IH : ∀ {a : α} {g : List α}, (splitBy.loop r l a g []).flatten = g.reverse ++ a :: l
a : α
g : List α
⊢ (match r a b with
      | true => splitBy.loop r l b (a :: g) []
      | false => [(a :: g).reverse].reverse ++ splitBy.loop r l b [] []).flatten =
    g.reverse ++ a :: b :: l
-- Mathlib/NumberTheory/Modular.lean
theorem im_T_zpow_smul (n : ℤ) : (T ^ n • z).im = z.im

Proof state:
z : ℍ
n : ℤ
⊢ (T ^ n • z).im = z.im

Tactic:
rw [← coe_im, coe_T_zpow_smul_eq, add_im, intCast_im, add_zero, coe_im]

Result:
no goals
-- Mathlib/MeasureTheory/Measure/Hausdorff.lean
theorem hausdorffMeasure_real : (μH[1] : Measure ℝ) = volume

Proof state:
⊢ μH[1] = volume

Tactic:
rw [← (volume_preserving_funUnique Unit ℝ).map_eq,
  ← (hausdorffMeasure_measurePreserving_funUnique Unit ℝ 1).map_eq,
  ← hausdorffMeasure_pi_real, Fintype.card_unit, Nat.cast_one]

Result:
no goals
-- Mathlib/CategoryTheory/Limits/Shapes/Reflexive.lean
@[simp]
lemma reflexiveCoforkEquivCofork_inverse_obj_π
    (G : Cofork (F.map left) (F.map right)) :
    ((reflexiveCoforkEquivCofork F).inverse.obj G).π = G.π

Proof state:
C : Type u
inst✝ : Category.{v, u} C
F : WalkingReflexivePair ⥤ C
G : Cofork (F.map left) (F.map right)
⊢ (Functor.Final.extendCocone.obj
            { pt := G.pt,
              ι :=
                (diagramIsoParallelPair
                      { obj := fun X => F.obj (WalkingParallelPair.inclusionWalkingReflexivePair.obj X),
                        map := fun {X Y} f => F.map (WalkingParallelPair.inclusionWalkingReflexivePair.map f),
                        map_id := ⋯, map_comp := ⋯ }).hom ≫
                  G.ι }).ι.app
      zero =
    G.π

Tactic:
rw [Functor.Final.extendCocone_obj_ι_app' (Y := .one) (f := 𝟙 zero)]

Result:
C : Type u
inst✝ : Category.{v, u} C
F : WalkingReflexivePair ⥤ C
G : Cofork (F.map left) (F.map right)
⊢ F.map (𝟙 zero) ≫
      { pt := G.pt,
              ι :=
                (diagramIsoParallelPair
                      { obj := fun X => F.obj (WalkingParallelPair.inclusionWalkingReflexivePair.obj X),
                        map := fun {X Y} f => F.map (WalkingParallelPair.inclusionWalkingReflexivePair.map f),
                        map_id := ⋯, map_comp := ⋯ }).hom ≫
                  G.ι }.ι.app
        WalkingParallelPair.one =
    G.π

Proof state:
C : Type u
inst✝ : Category.{v, u} C
F : WalkingReflexivePair ⥤ C
G : Cofork (F.map left) (F.map right)
⊢ ((reflexiveCoforkEquivCofork F).inverse.obj G).π = G.π

Tactic:
dsimp only [reflexiveCoforkEquivCofork, Equivalence.symm, Equivalence.trans,
  ReflexiveCofork.π, Cocones.precomposeEquivalence, Cocones.precompose,
  Functor.comp, Functor.Final.coconesEquiv]

Result:
C : Type u
inst✝ : Category.{v, u} C
F : WalkingReflexivePair ⥤ C
G : Cofork (F.map left) (F.map right)
⊢ (Functor.Final.extendCocone.obj
            { pt := G.pt,
              ι :=
                (diagramIsoParallelPair
                      { obj := fun X => F.obj (WalkingParallelPair.inclusionWalkingReflexivePair.obj X),
                        map := fun {X Y} f => F.map (WalkingParallelPair.inclusionWalkingReflexivePair.map f),
                        map_id := ⋯, map_comp := ⋯ }).hom ≫
                  G.ι }).ι.app
      zero =
    G.π

Proof state:
C : Type u
inst✝ : Category.{v, u} C
F : WalkingReflexivePair ⥤ C
G : Cofork (F.map left) (F.map right)
⊢ F.map (𝟙 zero) ≫
      { pt := G.pt,
              ι :=
                (diagramIsoParallelPair
                      { obj := fun X => F.obj (WalkingParallelPair.inclusionWalkingReflexivePair.obj X),
                        map := fun {X Y} f => F.map (WalkingParallelPair.inclusionWalkingReflexivePair.map f),
                        map_id := ⋯, map_comp := ⋯ }).hom ≫
                  G.ι }.ι.app
        WalkingParallelPair.one =
    G.π

Tactic:
simp

Result:
no goals
-- Mathlib/Order/Interval/Set/Basic.lean
theorem Iic_union_Ioc' (h₁ : c < b) : Iic b ∪ Ioc c d = Iic (max b d)

Proof state:
case neg
α : Type u_1
inst✝ : LinearOrder α
b c d : α
h₁ : c < b
x : α
hc : ¬c < x
⊢ x ≤ b ∨ c < x ∧ x ≤ d ↔ x ≤ b ∨ x ≤ d

Tactic:
have hxb : x ≤ b := (le_of_not_gt hc).trans h₁.le

Result:
case neg
α : Type u_1
inst✝ : LinearOrder α
b c d : α
h₁ : c < b
x : α
hc : ¬c < x
hxb : x ≤ b
⊢ x ≤ b ∨ c < x ∧ x ≤ d ↔ x ≤ b ∨ x ≤ d

Proof state:
case pos
α : Type u_1
inst✝ : LinearOrder α
b c d : α
h₁ : c < b
x : α
hc : c < x
⊢ x ≤ b ∨ c < x ∧ x ≤ d ↔ x ≤ b ∨ x ≤ d

Tactic:
simp only [hc, true_and]

Result:
no goals

Proof state:
case h
α : Type u_1
inst✝ : LinearOrder α
b c d : α
h₁ : c < b
x : α
⊢ x ≤ b ∨ c < x ∧ x ≤ d ↔ x ≤ b ∨ x ≤ d

Tactic:
by_cases hc : c < x

Result:
case pos
α : Type u_1
inst✝ : LinearOrder α
b c d : α
h₁ : c < b
x : α
hc : c < x
⊢ x ≤ b ∨ c < x ∧ x ≤ d ↔ x ≤ b ∨ x ≤ d

case neg
α : Type u_1
inst✝ : LinearOrder α
b c d : α
h₁ : c < b
x : α
hc : ¬c < x
⊢ x ≤ b ∨ c < x ∧ x ≤ d ↔ x ≤ b ∨ x ≤ d

Proof state:
case h
α : Type u_1
inst✝ : LinearOrder α
b c d : α
h₁ : c < b
x : α
⊢ x ∈ Iic b ∪ Ioc c d ↔ x ∈ Iic (b ⊔ d)

Tactic:
simp_rw [mem_union, mem_Iic, mem_Ioc, le_max_iff]

Result:
case h
α : Type u_1
inst✝ : LinearOrder α
b c d : α
h₁ : c < b
x : α
⊢ x ≤ b ∨ c < x ∧ x ≤ d ↔ x ≤ b ∨ x ≤ d

Proof state:
α : Type u_1
inst✝ : LinearOrder α
b c d : α
h₁ : c < b
⊢ Iic b ∪ Ioc c d = Iic (b ⊔ d)

Tactic:
ext1 x

Result:
case h
α : Type u_1
inst✝ : LinearOrder α
b c d : α
h₁ : c < b
x : α
⊢ x ∈ Iic b ∪ Ioc c d ↔ x ∈ Iic (b ⊔ d)

Proof state:
case neg
α : Type u_1
inst✝ : LinearOrder α
b c d : α
h₁ : c < b
x : α
hc : ¬c < x
hxb : x ≤ b
⊢ x ≤ b ∨ c < x ∧ x ≤ d ↔ x ≤ b ∨ x ≤ d

Tactic:
simp only [hxb, true_or]

Result:
no goals
-- Mathlib/Algebra/Category/Grp/EpiMono.lean
theorem agree : f.hom.range = { x | h x = g x }

Proof state:
case pos
A B : Grp
f : A ⟶ B
a : ↑A
y : ↑B
m : y ∈ (Hom.hom f).range
⊢ (h ((ConcreteCategory.hom f) a)) (fromCoset ⟨(fun x => x • ↑(Hom.hom f).range) y, ⋯⟩) =
    fromCoset ⟨(ConcreteCategory.hom f) a • ↑⟨(fun x => x • ↑(Hom.hom f).range) y, ⋯⟩, ⋯⟩

Tactic:
rw [h_apply_fromCoset' _ _ _ m, fromCoset_eq_of_mem_range _ m]

Result:
case pos
A B : Grp
f : A ⟶ B
a : ↑A
y : ↑B
m : y ∈ (Hom.hom f).range
⊢ fromCoset ⟨↑(Hom.hom f).range, ⋯⟩ =
    fromCoset ⟨(ConcreteCategory.hom f) a • ↑⟨(fun x => x • ↑(Hom.hom f).range) y, ⋯⟩, ⋯⟩

Proof state:
A B : Grp
f : A ⟶ B
⊢ ↑(Hom.hom f).range = {x | h x = g x}

Tactic:
refine Set.ext fun b => ⟨?_, fun hb : h b = g b => by_contradiction fun r => ?_⟩

Result:
case refine_1
A B : Grp
f : A ⟶ B
b : ↑B
⊢ b ∈ ↑(Hom.hom f).range → b ∈ {x | h x = g x}

case refine_2
A B : Grp
f : A ⟶ B
b : ↑B
hb : h b = g b
r : b ∉ ↑(Hom.hom f).range
⊢ False
-- Mathlib/Analysis/SpecialFunctions/Trigonometric/Inverse.lean
theorem sin_arccos (x : ℝ) : sin (arccos x) = √(1 - x ^ 2)

Proof state:
case pos
x : ℝ
hx₁ : -1 ≤ x
⊢ sin (arccos x) = √(1 - x ^ 2)

case neg
x : ℝ
hx₁ : ¬-1 ≤ x
⊢ sin (arccos x) = √(1 - x ^ 2)

Tactic:
swap

Result:
case neg
x : ℝ
hx₁ : ¬-1 ≤ x
⊢ sin (arccos x) = √(1 - x ^ 2)

case pos
x : ℝ
hx₁ : -1 ≤ x
⊢ sin (arccos x) = √(1 - x ^ 2)

Proof state:
case pos
x : ℝ
hx₁ : -1 ≤ x
hx₂ : x ≤ 1
⊢ sin (arccos x) = √(1 - x ^ 2)

Tactic:
rw [arccos_eq_pi_div_two_sub_arcsin, sin_pi_div_two_sub, cos_arcsin]

Result:
no goals

Proof state:
case neg
x : ℝ
hx₁ : -1 ≤ x
hx₂ : 1 < x
⊢ sin (arccos x) = √(1 - x ^ 2)

Tactic:
rw [arccos_of_one_le hx₂.le, sin_zero, sqrt_eq_zero_of_nonpos]

Result:
case neg
x : ℝ
hx₁ : -1 ≤ x
hx₂ : 1 < x
⊢ 1 - x ^ 2 ≤ 0

Proof state:
case pos
x : ℝ
hx₁ : -1 ≤ x
⊢ sin (arccos x) = √(1 - x ^ 2)

Tactic:
by_cases hx₂ : x ≤ 1

Result:
case pos
x : ℝ
hx₁ : -1 ≤ x
hx₂ : x ≤ 1
⊢ sin (arccos x) = √(1 - x ^ 2)

case neg
x : ℝ
hx₁ : -1 ≤ x
hx₂ : ¬x ≤ 1
⊢ sin (arccos x) = √(1 - x ^ 2)

Proof state:
case pos
x : ℝ
hx₁ : -1 ≤ x
hx₂ : x ≤ 1
⊢ sin (arccos x) = √(1 - x ^ 2)

case neg
x : ℝ
hx₁ : -1 ≤ x
hx₂ : ¬x ≤ 1
⊢ sin (arccos x) = √(1 - x ^ 2)

Tactic:
swap

Result:
case neg
x : ℝ
hx₁ : -1 ≤ x
hx₂ : ¬x ≤ 1
⊢ sin (arccos x) = √(1 - x ^ 2)

case pos
x : ℝ
hx₁ : -1 ≤ x
hx₂ : x ≤ 1
⊢ sin (arccos x) = √(1 - x ^ 2)

Proof state:
case neg
x : ℝ
hx₁ : -1 ≤ x
hx₂ : ¬x ≤ 1
⊢ sin (arccos x) = √(1 - x ^ 2)

Tactic:
rw [not_le] at hx₂

Result:
case neg
x : ℝ
hx₁ : -1 ≤ x
hx₂ : 1 < x
⊢ sin (arccos x) = √(1 - x ^ 2)

Proof state:
case neg
x : ℝ
hx₁ : x < -1
⊢ sin (arccos x) = √(1 - x ^ 2)

Tactic:
rw [arccos_of_le_neg_one hx₁.le, sin_pi, sqrt_eq_zero_of_nonpos]

Result:
case neg
x : ℝ
hx₁ : x < -1
⊢ 1 - x ^ 2 ≤ 0

Proof state:
x : ℝ
⊢ sin (arccos x) = √(1 - x ^ 2)

Tactic:
by_cases hx₁ : -1 ≤ x

Result:
case pos
x : ℝ
hx₁ : -1 ≤ x
⊢ sin (arccos x) = √(1 - x ^ 2)

case neg
x : ℝ
hx₁ : ¬-1 ≤ x
⊢ sin (arccos x) = √(1 - x ^ 2)

Proof state:
case neg
x : ℝ
hx₁ : ¬-1 ≤ x
⊢ sin (arccos x) = √(1 - x ^ 2)

Tactic:
rw [not_le] at hx₁

Result:
case neg
x : ℝ
hx₁ : x < -1
⊢ sin (arccos x) = √(1 - x ^ 2)

Proof state:
case neg
x : ℝ
hx₁ : x < -1
⊢ 1 - x ^ 2 ≤ 0

Tactic:
nlinarith

Result:
no goals

Proof state:
case neg
x : ℝ
hx₁ : -1 ≤ x
hx₂ : 1 < x
⊢ 1 - x ^ 2 ≤ 0

Tactic:
nlinarith

Result:
no goals