harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/Combinatorics/SetFamily/LYM.lean
theorem sum_card_slice_div_choose_le_one [Fintype α]
    (h𝒜 : IsAntichain (· ⊆ ·) (𝒜 : Set (Finset α))) :
    (∑ r ∈ range (Fintype.card α + 1), (#(𝒜 # r) : 𝕜) / (Fintype.card α).choose r) ≤ 1

Proof state:
𝕜 : Type u_1
α : Type u_2
inst✝¹ : LinearOrderedField 𝕜
𝒜 : Finset (Finset α)
inst✝ : Fintype α
h𝒜 : IsAntichain (fun x1 x2 => x1 ⊆ x2) ↑𝒜
⊢ 0 < 1

Tactic:
exact zero_lt_one

Result:
no goals

Proof state:
𝕜 : Type u_1
α : Type u_2
inst✝¹ : LinearOrderedField 𝕜
𝒜 : Finset (Finset α)
inst✝ : Fintype α
h𝒜 : IsAntichain (fun x1 x2 => x1 ⊆ x2) ↑𝒜
⊢ ∑ r ∈ range (Fintype.card α + 1), ↑(#(𝒜 # (Fintype.card α - r))) / ↑((Fintype.card α).choose (Fintype.card α - r)) ≤ 1

Tactic:
refine (le_card_falling_div_choose le_rfl h𝒜).trans ?_

Result:
𝕜 : Type u_1
α : Type u_2
inst✝¹ : LinearOrderedField 𝕜
𝒜 : Finset (Finset α)
inst✝ : Fintype α
h𝒜 : IsAntichain (fun x1 x2 => x1 ⊆ x2) ↑𝒜
⊢ ↑(#(falling (Fintype.card α - Fintype.card α) 𝒜)) / ↑((Fintype.card α).choose (Fintype.card α - Fintype.card α)) ≤ 1

Proof state:
𝕜 : Type u_1
α : Type u_2
inst✝¹ : LinearOrderedField 𝕜
𝒜 : Finset (Finset α)
inst✝ : Fintype α
h𝒜 : IsAntichain (fun x1 x2 => x1 ⊆ x2) ↑𝒜
⊢ #(falling (Fintype.card α - Fintype.card α) 𝒜) ≤ 1 * (Fintype.card α).choose (Fintype.card α - Fintype.card α)

Tactic:
simpa only [Nat.sub_self, one_mul, Nat.choose_zero_right, falling] using
  Set.Sized.card_le (sized_falling 0 𝒜)

Result:
no goals

Proof state:
𝕜 : Type u_1
α : Type u_2
inst✝¹ : LinearOrderedField 𝕜
𝒜 : Finset (Finset α)
inst✝ : Fintype α
h𝒜 : IsAntichain (fun x1 x2 => x1 ⊆ x2) ↑𝒜
⊢ ∑ r ∈ range (Fintype.card α + 1), ↑(#(𝒜 # r)) / ↑((Fintype.card α).choose r) ≤ 1

Tactic:
rw [← sum_flip]

Result:
𝕜 : Type u_1
α : Type u_2
inst✝¹ : LinearOrderedField 𝕜
𝒜 : Finset (Finset α)
inst✝ : Fintype α
h𝒜 : IsAntichain (fun x1 x2 => x1 ⊆ x2) ↑𝒜
⊢ ∑ r ∈ range (Fintype.card α + 1), ↑(#(𝒜 # (Fintype.card α - r))) / ↑((Fintype.card α).choose (Fintype.card α - r)) ≤ 1

Proof state:
𝕜 : Type u_1
α : Type u_2
inst✝¹ : LinearOrderedField 𝕜
𝒜 : Finset (Finset α)
inst✝ : Fintype α
h𝒜 : IsAntichain (fun x1 x2 => x1 ⊆ x2) ↑𝒜
⊢ ↑(#(falling (Fintype.card α - Fintype.card α) 𝒜)) / ↑((Fintype.card α).choose (Fintype.card α - Fintype.card α)) ≤ 1

Tactic:
rw [div_le_iff₀] <;> norm_cast

Result:
𝕜 : Type u_1
α : Type u_2
inst✝¹ : LinearOrderedField 𝕜
𝒜 : Finset (Finset α)
inst✝ : Fintype α
h𝒜 : IsAntichain (fun x1 x2 => x1 ⊆ x2) ↑𝒜
⊢ #(falling (Fintype.card α - Fintype.card α) 𝒜) ≤ 1 * (Fintype.card α).choose (Fintype.card α - Fintype.card α)

𝕜 : Type u_1
α : Type u_2
inst✝¹ : LinearOrderedField 𝕜
𝒜 : Finset (Finset α)
inst✝ : Fintype α
h𝒜 : IsAntichain (fun x1 x2 => x1 ⊆ x2) ↑𝒜
⊢ 0 < (Fintype.card α).choose (Fintype.card α - Fintype.card α)

Proof state:
𝕜 : Type u_1
α : Type u_2
inst✝¹ : LinearOrderedField 𝕜
𝒜 : Finset (Finset α)
inst✝ : Fintype α
h𝒜 : IsAntichain (fun x1 x2 => x1 ⊆ x2) ↑𝒜
⊢ 0 < (Fintype.card α).choose (Fintype.card α - Fintype.card α)

Tactic:
rw [tsub_self, choose_zero_right]

Result:
𝕜 : Type u_1
α : Type u_2
inst✝¹ : LinearOrderedField 𝕜
𝒜 : Finset (Finset α)
inst✝ : Fintype α
h𝒜 : IsAntichain (fun x1 x2 => x1 ⊆ x2) ↑𝒜
⊢ 0 < 1
-- Mathlib/Analysis/Asymptotics/Theta.lean
theorem isTheta_const_mul_right {c : 𝕜} {g : α → 𝕜} (hc : c ≠ 0) :
    (f =Θ[l] fun x ↦ c * g x) ↔ f =Θ[l] g

Proof state:
α : Type u_1
E : Type u_3
𝕜 : Type u_14
inst✝¹ : Norm E
inst✝ : NormedField 𝕜
f : α → E
l : Filter α
c : 𝕜
g : α → 𝕜
hc : c ≠ 0
⊢ (f =Θ[l] fun x => c * g x) ↔ f =Θ[l] g

Tactic:
simpa only [← smul_eq_mul] using isTheta_const_smul_right hc

Result:
no goals
-- Mathlib/SetTheory/Ordinal/Notation.lean
theorem split_dvd {o o' m} [NF o] (h : split o = (o', m)) : ω ∣ repr o'

Proof state:
case mk
o o' : ONote
m : ℕ
inst✝ : o.NF
a : ONote
n : ℕ
e : o.split' = (a, n)
fst_eq✝ : scale 1 a = o'
snd_eq✝ : n = m
⊢ ω ∣ o'.repr

Tactic:
subst o'

Result:
case mk
o : ONote
m : ℕ
inst✝ : o.NF
a : ONote
n : ℕ
e : o.split' = (a, n)
snd_eq✝ : n = m
⊢ ω ∣ (scale 1 a).repr

Proof state:
o o' : ONote
m : ℕ
inst✝ : o.NF
h : o.split = (o', m)
⊢ ω ∣ o'.repr

Tactic:
rcases e : split' o with ⟨a, n⟩

Result:
case mk
o o' : ONote
m : ℕ
inst✝ : o.NF
h : o.split = (o', m)
a : ONote
n : ℕ
e : o.split' = (a, n)
⊢ ω ∣ o'.repr

Proof state:
case mk
o o' : ONote
m : ℕ
inst✝ : o.NF
a : ONote
n : ℕ
h : (scale 1 a, n) = (o', m)
e : o.split' = (a, n)
⊢ ω ∣ o'.repr

Tactic:
injection h

Result:
case mk
o o' : ONote
m : ℕ
inst✝ : o.NF
a : ONote
n : ℕ
e : o.split' = (a, n)
fst_eq✝ : scale 1 a = o'
snd_eq✝ : n = m
⊢ ω ∣ o'.repr

Proof state:
case mk
o o' : ONote
m : ℕ
inst✝ : o.NF
h : o.split = (o', m)
a : ONote
n : ℕ
e : o.split' = (a, n)
⊢ ω ∣ o'.repr

Tactic:
rw [split_eq_scale_split' e] at h

Result:
case mk
o o' : ONote
m : ℕ
inst✝ : o.NF
a : ONote
n : ℕ
h : (scale 1 a, n) = (o', m)
e : o.split' = (a, n)
⊢ ω ∣ o'.repr

Proof state:
case mk.intro
o : ONote
m : ℕ
inst✝ : o.NF
a : ONote
n : ℕ
e : o.split' = (a, n)
snd_eq✝ : n = m
left✝ : a.NF
right✝ : o.repr = ω * a.repr + ↑n
⊢ ω ∣ (scale 1 a).repr

Tactic:
simp

Result:
no goals

Proof state:
case mk
o : ONote
m : ℕ
inst✝ : o.NF
a : ONote
n : ℕ
e : o.split' = (a, n)
snd_eq✝ : n = m
⊢ ω ∣ (scale 1 a).repr

Tactic:
cases nf_repr_split' e

Result:
case mk.intro
o : ONote
m : ℕ
inst✝ : o.NF
a : ONote
n : ℕ
e : o.split' = (a, n)
snd_eq✝ : n = m
left✝ : a.NF
right✝ : o.repr = ω * a.repr + ↑n
⊢ ω ∣ (scale 1 a).repr
-- Mathlib/Analysis/SpecialFunctions/Trigonometric/Deriv.lean
theorem sinh_sub_id_strictMono : StrictMono fun x => sinh x - x

Proof state:
case refine_2
x : ℝ
hx : 0 < x
⊢ x ≠ 0

case refine_2.hf
x : ℝ
hx : 0 < x
⊢ DifferentiableAt ℝ sinh x

case refine_2.hg
x : ℝ
hx : 0 < x
⊢ DifferentiableAt ℝ (fun x => x) x

Tactic:
exacts [hx.ne', differentiableAt_sinh, differentiableAt_id]

Result:
no goals

Proof state:
⊢ StrictMonoOn (fun x => sinh x - x) (Ici 0)

Tactic:
refine strictMonoOn_of_deriv_pos (convex_Ici _) ?_ fun x hx => ?_

Result:
case refine_1

⊢ ContinuousOn (fun x => sinh x - x) (Ici 0)

case refine_2
x : ℝ
hx : x ∈ interior (Ici 0)
⊢ 0 < deriv (fun x => sinh x - x) x

Proof state:
case refine_2
x : ℝ
hx : x ∈ interior (Ici 0)
⊢ 0 < deriv (fun x => sinh x - x) x

Tactic:
rw [interior_Ici, mem_Ioi] at hx

Result:
case refine_2
x : ℝ
hx : 0 < x
⊢ 0 < deriv (fun x => sinh x - x) x

Proof state:
⊢ StrictMono fun x => sinh x - x

Tactic:
refine strictMono_of_odd_strictMonoOn_nonneg (fun x => by simp; abel) ?_

Result:
⊢ StrictMonoOn (fun x => sinh x - x) (Ici 0)

Proof state:
case refine_1

⊢ ContinuousOn (fun x => sinh x - x) (Ici 0)

Tactic:
exact (continuous_sinh.sub continuous_id).continuousOn

Result:
no goals

Proof state:
x : ℝ
⊢ -sinh x + x = x - sinh x

Tactic:
abel

Result:
no goals

Proof state:
x : ℝ
⊢ sinh (-x) - -x = -(sinh x - x)

Tactic:
simp

Result:
x : ℝ
⊢ -sinh x + x = x - sinh x

Proof state:
case refine_2
x : ℝ
hx : 0 < x
⊢ 0 < deriv (fun x => sinh x - x) x

Tactic:
rw [deriv_sub, deriv_sinh, deriv_id'', sub_pos, one_lt_cosh]

Result:
case refine_2
x : ℝ
hx : 0 < x
⊢ x ≠ 0

case refine_2.hf
x : ℝ
hx : 0 < x
⊢ DifferentiableAt ℝ sinh x

case refine_2.hg
x : ℝ
hx : 0 < x
⊢ DifferentiableAt ℝ (fun x => x) x
-- Mathlib/Order/CompleteLatticeIntervals.lean
theorem coe_iSup : (↑(⨆ i, f i) : α) = ⨆ i, (f i : α)

Proof state:
case e_a
ι : Sort u_1
α : Type u_2
inst✝ : CompleteLattice α
a : α
f : ι → ↑(Iic a)
⊢ (Subtype.val '' range fun i => f i) = range fun i => ↑(f i)

Tactic:
ext

Result:
case e_a.h
ι : Sort u_1
α : Type u_2
inst✝ : CompleteLattice α
a : α
f : ι → ↑(Iic a)
x✝ : α
⊢ (x✝ ∈ Subtype.val '' range fun i => f i) ↔ x✝ ∈ range fun i => ↑(f i)

Proof state:
ι : Sort u_1
α : Type u_2
inst✝ : CompleteLattice α
a : α
f : ι → ↑(Iic a)
⊢ sSup (Subtype.val '' range fun i => f i) = ⨆ i, ↑(f i)

Tactic:
congr

Result:
case e_a
ι : Sort u_1
α : Type u_2
inst✝ : CompleteLattice α
a : α
f : ι → ↑(Iic a)
⊢ (Subtype.val '' range fun i => f i) = range fun i => ↑(f i)

Proof state:
ι : Sort u_1
α : Type u_2
inst✝ : CompleteLattice α
a : α
f : ι → ↑(Iic a)
⊢ ↑(⨆ i, f i) = ⨆ i, ↑(f i)

Tactic:
rw [iSup, coe_sSup]

Result:
ι : Sort u_1
α : Type u_2
inst✝ : CompleteLattice α
a : α
f : ι → ↑(Iic a)
⊢ sSup (Subtype.val '' range fun i => f i) = ⨆ i, ↑(f i)

Proof state:
case e_a.h
ι : Sort u_1
α : Type u_2
inst✝ : CompleteLattice α
a : α
f : ι → ↑(Iic a)
x✝ : α
⊢ (x✝ ∈ Subtype.val '' range fun i => f i) ↔ x✝ ∈ range fun i => ↑(f i)

Tactic:
simp

Result:
no goals
-- Mathlib/Probability/Martingale/BorelCantelli.lean
theorem tendsto_sum_indicator_atTop_iff [IsFiniteMeasure μ]
    (hfmono : ∀ᵐ ω ∂μ, ∀ n, f n ω ≤ f (n + 1) ω) (hf : Adapted ℱ f) (hint : ∀ n, Integrable (f n) μ)
    (hbdd : ∀ᵐ ω ∂μ, ∀ n, |f (n + 1) ω - f n ω| ≤ R) :
    ∀ᵐ ω ∂μ, Tendsto (fun n => f n ω) atTop atTop ↔
      Tendsto (fun n => predictablePart f ℱ μ n ω) atTop atTop

Proof state:
case h.mp.refine_1
Ω : Type u_1
m0 : MeasurableSpace Ω
μ : Measure Ω
ℱ : Filtration ℕ m0
f : ℕ → Ω → ℝ
R : ℝ≥0
inst✝ : IsFiniteMeasure μ
hfmono : ∀ᵐ (ω : Ω) ∂μ, ∀ (n : ℕ), f n ω ≤ f (n + 1) ω
hf : Adapted ℱ f
hint : ∀ (n : ℕ), Integrable (f n) μ
hbdd : ∀ᵐ (ω : Ω) ∂μ, ∀ (n : ℕ), |f (n + 1) ω - f n ω| ≤ ↑R
h₁ : ∀ᵐ (ω : Ω) ∂μ, ¬Tendsto (fun n => martingalePart f ℱ μ n ω) atTop atTop
h₂ : ∀ᵐ (ω : Ω) ∂μ, ¬Tendsto (fun n => martingalePart f ℱ μ n ω) atTop atBot
h₃ : ∀ᵐ (ω : Ω) ∂μ, ∀ (n : ℕ), 0 ≤ (μ[f (n + 1) - f n|↑ℱ n]) ω
ω : Ω
hω₁ : ¬Tendsto (fun n => martingalePart f ℱ μ n ω) atTop atTop
hω₂ : ¬Tendsto (fun n => martingalePart f ℱ μ n ω) atTop atBot
hω₃ : ∀ (n : ℕ), 0 ≤ (μ[f (n + 1) - f n|↑ℱ n]) ω
hω₄ : ∀ (n : ℕ), f n ω ≤ f (n + 1) ω
ht : Tendsto (fun n => f n ω) atTop atTop
n m : ℕ
hnm : n ≤ m
⊢ (fun n => predictablePart f ℱ μ n ω) n ≤ (fun n => predictablePart f ℱ μ n ω) m

Tactic:
simp only [predictablePart, Finset.sum_apply]

Result:
case h.mp.refine_1
Ω : Type u_1
m0 : MeasurableSpace Ω
μ : Measure Ω
ℱ : Filtration ℕ m0
f : ℕ → Ω → ℝ
R : ℝ≥0
inst✝ : IsFiniteMeasure μ
hfmono : ∀ᵐ (ω : Ω) ∂μ, ∀ (n : ℕ), f n ω ≤ f (n + 1) ω
hf : Adapted ℱ f
hint : ∀ (n : ℕ), Integrable (f n) μ
hbdd : ∀ᵐ (ω : Ω) ∂μ, ∀ (n : ℕ), |f (n + 1) ω - f n ω| ≤ ↑R
h₁ : ∀ᵐ (ω : Ω) ∂μ, ¬Tendsto (fun n => martingalePart f ℱ μ n ω) atTop atTop
h₂ : ∀ᵐ (ω : Ω) ∂μ, ¬Tendsto (fun n => martingalePart f ℱ μ n ω) atTop atBot
h₃ : ∀ᵐ (ω : Ω) ∂μ, ∀ (n : ℕ), 0 ≤ (μ[f (n + 1) - f n|↑ℱ n]) ω
ω : Ω
hω₁ : ¬Tendsto (fun n => martingalePart f ℱ μ n ω) atTop atTop
hω₂ : ¬Tendsto (fun n => martingalePart f ℱ μ n ω) atTop atBot
hω₃ : ∀ (n : ℕ), 0 ≤ (μ[f (n + 1) - f n|↑ℱ n]) ω
hω₄ : ∀ (n : ℕ), f n ω ≤ f (n + 1) ω
ht : Tendsto (fun n => f n ω) atTop atTop
n m : ℕ
hnm : n ≤ m
⊢ ∑ c ∈ Finset.range n, (μ[f (c + 1) - f c|↑ℱ c]) ω ≤ ∑ c ∈ Finset.range m, (μ[f (c + 1) - f c|↑ℱ c]) ω
-- Mathlib/Algebra/Polynomial/Basic.lean
theorem coeff_ofFinsupp (p) : coeff (⟨p⟩ : R[X]) = p

Proof state:
R : Type u
inst✝ : Semiring R
p : R[ℕ]
⊢ { toFinsupp := p }.coeff = ⇑p

Tactic:
rw [coeff]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Array/Monadic.lean
theorem foldlM_filter [Monad m] [LawfulMonad m] (p : α → Bool) (g : β → α → m β)
    (l : Array α) (init : β) (w : stop = (l.filter p).size) :
    (l.filter p).foldlM g init 0 stop =
      l.foldlM (fun x y => if p y then g x y else pure x) init

Proof state:
case mk
m : Type u_1 → Type u_2
α : Type u_3
β : Type u_1
inst✝¹ : Monad m
inst✝ : LawfulMonad m
p : α → Bool
g : β → α → m β
init : β
toList✝ : List α
⊢ foldlM g init (filter p { toList := toList✝ }) =
    foldlM (fun x y => if p y = true then g x y else pure x) init { toList := toList✝ }

Tactic:
simp [List.foldlM_filter]

Result:
no goals

Proof state:
m : Type u_1 → Type u_2
α : Type u_3
β : Type u_1
stop : Nat
inst✝¹ : Monad m
inst✝ : LawfulMonad m
p : α → Bool
g : β → α → m β
l : Array α
init : β
w : stop = (filter p l).size
⊢ foldlM g init (filter p l) 0 stop = foldlM (fun x y => if p y = true then g x y else pure x) init l

Tactic:
subst w

Result:
m : Type u_1 → Type u_2
α : Type u_3
β : Type u_1
inst✝¹ : Monad m
inst✝ : LawfulMonad m
p : α → Bool
g : β → α → m β
l : Array α
init : β
⊢ foldlM g init (filter p l) = foldlM (fun x y => if p y = true then g x y else pure x) init l

Proof state:
m : Type u_1 → Type u_2
α : Type u_3
β : Type u_1
inst✝¹ : Monad m
inst✝ : LawfulMonad m
p : α → Bool
g : β → α → m β
l : Array α
init : β
⊢ foldlM g init (filter p l) = foldlM (fun x y => if p y = true then g x y else pure x) init l

Tactic:
cases l

Result:
case mk
m : Type u_1 → Type u_2
α : Type u_3
β : Type u_1
inst✝¹ : Monad m
inst✝ : LawfulMonad m
p : α → Bool
g : β → α → m β
init : β
toList✝ : List α
⊢ foldlM g init (filter p { toList := toList✝ }) =
    foldlM (fun x y => if p y = true then g x y else pure x) init { toList := toList✝ }
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/List/Sublist.lean
theorem IsInfix.filterMap {β} (f : α → Option β) ⦃l₁ l₂ : List α⦄ (h : l₁ <:+: l₂) :
    filterMap f l₁ <:+: filterMap f l₂

Proof state:
case intro.intro
α : Type u_1
β : Type u_2
f : α → Option β
l₁ xs ys : List α
⊢ List.filterMap f l₁ <:+: List.filterMap f (xs ++ l₁ ++ ys)

Tactic:
rw [filterMap_append, filterMap_append]

Result:
case intro.intro
α : Type u_1
β : Type u_2
f : α → Option β
l₁ xs ys : List α
⊢ List.filterMap f l₁ <:+: List.filterMap f xs ++ List.filterMap f l₁ ++ List.filterMap f ys

Proof state:
α : Type u_1
β : Type u_2
f : α → Option β
l₁ l₂ : List α
h : l₁ <:+: l₂
⊢ List.filterMap f l₁ <:+: List.filterMap f l₂

Tactic:
obtain ⟨xs, ys, rfl⟩ := h

Result:
case intro.intro
α : Type u_1
β : Type u_2
f : α → Option β
l₁ xs ys : List α
⊢ List.filterMap f l₁ <:+: List.filterMap f (xs ++ l₁ ++ ys)

Proof state:
case intro.intro
α : Type u_1
β : Type u_2
f : α → Option β
l₁ xs ys : List α
⊢ List.filterMap f l₁ <:+: List.filterMap f xs ++ List.filterMap f l₁ ++ List.filterMap f ys

Tactic:
apply infix_append

Result:
no goals
-- Mathlib/Dynamics/Ergodic/AddCircle.lean
theorem ergodic_zsmul_add (x : AddCircle T) {n : ℤ} (h : 1 < |n|) : Ergodic fun y => n • y + x

Proof state:
T : ℝ
hT : Fact (0 < T)
x : AddCircle T
n : ℤ
f : AddCircle T → AddCircle T := fun y => n • y + x
e : AddCircle T ≃ᵐ AddCircle T := MeasurableEquiv.addLeft (DivisibleBy.div x (n - 1))
he : MeasurePreserving (⇑e) volume volume
h : n - 1 ≠ 0
⊢ ⇑e ∘ f ∘ ⇑e.symm = fun y => n • y

Tactic:
have hnx : n • DivisibleBy.div x (n - 1) = x + DivisibleBy.div x (n - 1) := by
  conv_rhs => congr; rw [← DivisibleBy.div_cancel x h]
  rw [sub_smul, one_smul, sub_add_cancel]

Result:
T : ℝ
hT : Fact (0 < T)
x : AddCircle T
n : ℤ
f : AddCircle T → AddCircle T := fun y => n • y + x
e : AddCircle T ≃ᵐ AddCircle T := MeasurableEquiv.addLeft (DivisibleBy.div x (n - 1))
he : MeasurePreserving (⇑e) volume volume
h : n - 1 ≠ 0
hnx : n • DivisibleBy.div x (n - 1) = x + DivisibleBy.div x (n - 1)
⊢ ⇑e ∘ f ∘ ⇑e.symm = fun y => n • y

Proof state:
T : ℝ
hT : Fact (0 < T)
x : AddCircle T
n : ℤ
h : 1 < |n|
⊢ Ergodic (fun y => n • y + x) volume

Tactic:
set f : AddCircle T → AddCircle T := fun y => n • y + x

Result:
T : ℝ
hT : Fact (0 < T)
x : AddCircle T
n : ℤ
h : 1 < |n|
f : AddCircle T → AddCircle T := fun y => n • y + x
⊢ Ergodic f volume

Proof state:
T : ℝ
hT : Fact (0 < T)
x : AddCircle T
n : ℤ
f : AddCircle T → AddCircle T := fun y => n • y + x
e : AddCircle T ≃ᵐ AddCircle T := MeasurableEquiv.addLeft (DivisibleBy.div x (n - 1))
he : MeasurePreserving (⇑e) volume volume
h : n - 1 ≠ 0
⊢ n • DivisibleBy.div x (n - 1) = x + DivisibleBy.div x (n - 1)

Tactic:
conv_rhs => congr; rw [← DivisibleBy.div_cancel x h]

Result:
T : ℝ
hT : Fact (0 < T)
x : AddCircle T
n : ℤ
f : AddCircle T → AddCircle T := fun y => n • y + x
e : AddCircle T ≃ᵐ AddCircle T := MeasurableEquiv.addLeft (DivisibleBy.div x (n - 1))
he : MeasurePreserving (⇑e) volume volume
h : n - 1 ≠ 0
⊢ n • DivisibleBy.div x (n - 1) = (n - 1) • DivisibleBy.div x (n - 1) + DivisibleBy.div x (n - 1)
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Array/Lemmas.lean
theorem foldlM_append' [Monad m] [LawfulMonad m] (f : β → α → m β) (b) (l l' : Array α)
    (w : stop = l.size + l'.size) :
    (l ++ l').foldlM f b 0 stop = l.foldlM f b >>= l'.foldlM f

Proof state:
case mk
m : Type u_1 → Type u_2
β : Type u_1
α : Type u_3
inst✝¹ : Monad m
inst✝ : LawfulMonad m
f : β → α → m β
b : β
l' : Array α
l : List α
⊢ foldlM f b ({ toList := l } ++ l') 0 ({ toList := l }.size + l'.size) = do
    let init ← foldlM f b { toList := l }
    foldlM f init l'

Tactic:
rcases l' with ⟨l'⟩

Result:
case mk.mk
m : Type u_1 → Type u_2
β : Type u_1
α : Type u_3
inst✝¹ : Monad m
inst✝ : LawfulMonad m
f : β → α → m β
b : β
l l' : List α
⊢ foldlM f b ({ toList := l } ++ { toList := l' }) 0 ({ toList := l }.size + { toList := l' }.size) = do
    let init ← foldlM f b { toList := l }
    foldlM f init { toList := l' }

Proof state:
m : Type u_1 → Type u_2
β : Type u_1
α : Type u_3
stop : Nat
inst✝¹ : Monad m
inst✝ : LawfulMonad m
f : β → α → m β
b : β
l l' : Array α
w : stop = l.size + l'.size
⊢ foldlM f b (l ++ l') 0 stop = do
    let init ← foldlM f b l
    foldlM f init l'

Tactic:
subst w

Result:
m : Type u_1 → Type u_2
β : Type u_1
α : Type u_3
inst✝¹ : Monad m
inst✝ : LawfulMonad m
f : β → α → m β
b : β
l l' : Array α
⊢ foldlM f b (l ++ l') 0 (l.size + l'.size) = do
    let init ← foldlM f b l
    foldlM f init l'

Proof state:
m : Type u_1 → Type u_2
β : Type u_1
α : Type u_3
inst✝¹ : Monad m
inst✝ : LawfulMonad m
f : β → α → m β
b : β
l l' : Array α
⊢ foldlM f b (l ++ l') 0 (l.size + l'.size) = do
    let init ← foldlM f b l
    foldlM f init l'

Tactic:
rcases l with ⟨l⟩

Result:
case mk
m : Type u_1 → Type u_2
β : Type u_1
α : Type u_3
inst✝¹ : Monad m
inst✝ : LawfulMonad m
f : β → α → m β
b : β
l' : Array α
l : List α
⊢ foldlM f b ({ toList := l } ++ l') 0 ({ toList := l }.size + l'.size) = do
    let init ← foldlM f b { toList := l }
    foldlM f init l'

Proof state:
case mk.mk
m : Type u_1 → Type u_2
β : Type u_1
α : Type u_3
inst✝¹ : Monad m
inst✝ : LawfulMonad m
f : β → α → m β
b : β
l l' : List α
⊢ foldlM f b ({ toList := l } ++ { toList := l' }) 0 ({ toList := l }.size + { toList := l' }.size) = do
    let init ← foldlM f b { toList := l }
    foldlM f init { toList := l' }

Tactic:
simp

Result:
no goals
-- Mathlib/Geometry/Euclidean/Angle/Unoriented/RightAngle.lean
theorem dist_div_cos_angle_of_angle_eq_pi_div_two {p₁ p₂ p₃ : P} (h : ∠ p₁ p₂ p₃ = π / 2)
    (h0 : p₁ = p₂ ∨ p₃ ≠ p₂) : dist p₃ p₂ / Real.cos (∠ p₂ p₃ p₁) = dist p₁ p₃

Proof state:
V : Type u_1
P : Type u_2
inst✝³ : NormedAddCommGroup V
inst✝² : InnerProductSpace ℝ V
inst✝¹ : MetricSpace P
inst✝ : NormedAddTorsor V P
p₁ p₂ p₃ : P
h : inner (p₂ -ᵥ p₃) (p₁ -ᵥ p₂) = 0
h0 : p₁ = p₂ ∨ p₃ ≠ p₂
⊢ dist p₃ p₂ / Real.cos (∠ p₂ p₃ p₁) = dist p₁ p₃

Tactic:
rw [ne_comm, ← @vsub_ne_zero V, ← @vsub_eq_zero_iff_eq V, or_comm] at h0

Result:
V : Type u_1
P : Type u_2
inst✝³ : NormedAddCommGroup V
inst✝² : InnerProductSpace ℝ V
inst✝¹ : MetricSpace P
inst✝ : NormedAddTorsor V P
p₁ p₂ p₃ : P
h : inner (p₂ -ᵥ p₃) (p₁ -ᵥ p₂) = 0
h0 : p₂ -ᵥ p₃ ≠ 0 ∨ p₁ -ᵥ p₂ = 0
⊢ dist p₃ p₂ / Real.cos (∠ p₂ p₃ p₁) = dist p₁ p₃

Proof state:
V : Type u_1
P : Type u_2
inst✝³ : NormedAddCommGroup V
inst✝² : InnerProductSpace ℝ V
inst✝¹ : MetricSpace P
inst✝ : NormedAddTorsor V P
p₁ p₂ p₃ : P
h : ∠ p₁ p₂ p₃ = π / 2
h0 : p₁ = p₂ ∨ p₃ ≠ p₂
⊢ dist p₃ p₂ / Real.cos (∠ p₂ p₃ p₁) = dist p₁ p₃

Tactic:
rw [angle, ← inner_eq_zero_iff_angle_eq_pi_div_two, real_inner_comm, ← neg_eq_zero, ←
  inner_neg_left, neg_vsub_eq_vsub_rev] at h

Result:
V : Type u_1
P : Type u_2
inst✝³ : NormedAddCommGroup V
inst✝² : InnerProductSpace ℝ V
inst✝¹ : MetricSpace P
inst✝ : NormedAddTorsor V P
p₁ p₂ p₃ : P
h : inner (p₂ -ᵥ p₃) (p₁ -ᵥ p₂) = 0
h0 : p₁ = p₂ ∨ p₃ ≠ p₂
⊢ dist p₃ p₂ / Real.cos (∠ p₂ p₃ p₁) = dist p₁ p₃

Proof state:
V : Type u_1
P : Type u_2
inst✝³ : NormedAddCommGroup V
inst✝² : InnerProductSpace ℝ V
inst✝¹ : MetricSpace P
inst✝ : NormedAddTorsor V P
p₁ p₂ p₃ : P
h : inner (p₂ -ᵥ p₃) (p₁ -ᵥ p₂) = 0
h0 : p₂ -ᵥ p₃ ≠ 0 ∨ p₁ -ᵥ p₂ = 0
⊢ dist p₃ p₂ / Real.cos (∠ p₂ p₃ p₁) = dist p₁ p₃

Tactic:
rw [angle, dist_eq_norm_vsub' V p₃ p₂, dist_eq_norm_vsub V p₁ p₃, ← vsub_add_vsub_cancel p₁ p₂ p₃,
  add_comm, norm_div_cos_angle_add_of_inner_eq_zero h h0]

Result:
no goals
-- Mathlib/Analysis/Normed/Affine/Simplex.lean
lemma scalene_iff_dist_ne_and_dist_ne_and_dist_ne {t : Triangle R P} :
    t.Scalene ↔ dist (t.points 0) (t.points 1) ≠ dist (t.points 0) (t.points 2) ∧
      dist (t.points 0) (t.points 1) ≠ dist (t.points 1) (t.points 2) ∧
      dist (t.points 0) (t.points 2) ≠ dist (t.points 1) (t.points 2)

Proof state:
R : Type u_1
V : Type u_2
P : Type u_3
inst✝⁴ : Ring R
inst✝³ : SeminormedAddCommGroup V
inst✝² : PseudoMetricSpace P
inst✝¹ : Module R V
inst✝ : NormedAddTorsor V P
t : Triangle R P
x✝ :
  dist (t.points 0) (t.points 1) ≠ dist (t.points 0) (t.points 2) ∧
    dist (t.points 0) (t.points 1) ≠ dist (t.points 1) (t.points 2) ∧
      dist (t.points 0) (t.points 2) ≠ dist (t.points 1) (t.points 2)
h₁ : dist (t.points 0) (t.points 1) ≠ dist (t.points 0) (t.points 2)
h₂ : dist (t.points 0) (t.points 1) ≠ dist (t.points 1) (t.points 2)
h₃ : dist (t.points 0) (t.points 2) ≠ dist (t.points 1) (t.points 2)
x₁ x₂ : Fin (2 + 1)
hx : x₁ < x₂
y₁ y₂ : Fin (2 + 1)
hy : y₁ < y₂
hxy : dist (t.points x₁) (t.points x₂) = dist (t.points y₁) (t.points y₂)
⊢ x₁ = y₁ ∧ x₂ = y₂

Tactic:
fin_cases x₁ <;> fin_cases x₂ <;> simp +decide only at hx <;>
  fin_cases y₁ <;> fin_cases y₂ <;> simp +decide only at hy <;>
  simp [h₁, h₂, h₃, h₁.symm, h₂.symm, h₃.symm] at hxy ⊢

Result:
no goals

Proof state:
R : Type u_1
V : Type u_2
P : Type u_3
inst✝⁴ : Ring R
inst✝³ : SeminormedAddCommGroup V
inst✝² : PseudoMetricSpace P
inst✝¹ : Module R V
inst✝ : NormedAddTorsor V P
t : Triangle R P
⊢ Simplex.Scalene t ↔
    dist (t.points 0) (t.points 1) ≠ dist (t.points 0) (t.points 2) ∧
      dist (t.points 0) (t.points 1) ≠ dist (t.points 1) (t.points 2) ∧
        dist (t.points 0) (t.points 2) ≠ dist (t.points 1) (t.points 2)

Tactic:
refine ⟨fun h ↦
  ⟨h.dist_ne (by decide : (0 : Fin 3) ≠ 1) (by decide : (0 : Fin 3) ≠ 2) (by decide) (by decide),
   h.dist_ne (by decide : (0 : Fin 3) ≠ 1) (by decide : (1 : Fin 3) ≠ 2) (by decide) (by decide),
   h.dist_ne (by decide : (0 : Fin 3) ≠ 2) (by decide : (1 : Fin 3) ≠ 2) (by decide) (by decide)⟩,
  fun ⟨h₁, h₂, h₃⟩ ↦ ?_⟩

Result:
R : Type u_1
V : Type u_2
P : Type u_3
inst✝⁴ : Ring R
inst✝³ : SeminormedAddCommGroup V
inst✝² : PseudoMetricSpace P
inst✝¹ : Module R V
inst✝ : NormedAddTorsor V P
t : Triangle R P
x✝ :
  dist (t.points 0) (t.points 1) ≠ dist (t.points 0) (t.points 2) ∧
    dist (t.points 0) (t.points 1) ≠ dist (t.points 1) (t.points 2) ∧
      dist (t.points 0) (t.points 2) ≠ dist (t.points 1) (t.points 2)
h₁ : dist (t.points 0) (t.points 1) ≠ dist (t.points 0) (t.points 2)
h₂ : dist (t.points 0) (t.points 1) ≠ dist (t.points 1) (t.points 2)
h₃ : dist (t.points 0) (t.points 2) ≠ dist (t.points 1) (t.points 2)
⊢ Simplex.Scalene t
-- Mathlib/CategoryTheory/Limits/Shapes/Pullback/CommSq.lean
theorem inl_snd' {b : BinaryBicone X Y} (h : b.IsBilimit) :
    IsPullback b.inl (0 : X ⟶ 0) b.snd (0 : 0 ⟶ Y)

Proof state:
C : Type u₁
inst✝² : Category.{v₁, u₁} C
X Y : C
inst✝¹ : HasZeroObject C
inst✝ : HasZeroMorphisms C
b : BinaryBicone X Y
h : b.IsBilimit
⊢ IsPullback b.inl 0 b.snd 0

Tactic:
refine of_right ?_ (by simp) (of_isBilimit h)

Result:
C : Type u₁
inst✝² : Category.{v₁, u₁} C
X Y : C
inst✝¹ : HasZeroObject C
inst✝ : HasZeroMorphisms C
b : BinaryBicone X Y
h : b.IsBilimit
⊢ IsPullback (b.inl ≫ b.fst) 0 0 (0 ≫ 0)

Proof state:
C : Type u₁
inst✝² : Category.{v₁, u₁} C
X Y : C
inst✝¹ : HasZeroObject C
inst✝ : HasZeroMorphisms C
b : BinaryBicone X Y
h : b.IsBilimit
⊢ b.inl ≫ b.snd = 0 ≫ 0

Tactic:
simp

Result:
no goals

Proof state:
C : Type u₁
inst✝² : Category.{v₁, u₁} C
X Y : C
inst✝¹ : HasZeroObject C
inst✝ : HasZeroMorphisms C
b : BinaryBicone X Y
h : b.IsBilimit
⊢ IsPullback (b.inl ≫ b.fst) 0 0 (0 ≫ 0)

Tactic:
simp

Result:
no goals