harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/Data/PNat/Find.lean
theorem find_eq_iff : PNat.find h = m ↔ p m ∧ ∀ n < m, ¬p n

Proof state:
p : ℕ+ → Prop
inst✝ : DecidablePred p
h : ∃ n, p n
m : ℕ+
⊢ PNat.find h = m ↔ p m ∧ ∀ n < m, ¬p n

Tactic:
constructor

Result:
case mp
p : ℕ+ → Prop
inst✝ : DecidablePred p
h : ∃ n, p n
m : ℕ+
⊢ PNat.find h = m → p m ∧ ∀ n < m, ¬p n

case mpr
p : ℕ+ → Prop
inst✝ : DecidablePred p
h : ∃ n, p n
m : ℕ+
⊢ (p m ∧ ∀ n < m, ¬p n) → PNat.find h = m

Proof state:
case mpr
p : ℕ+ → Prop
inst✝ : DecidablePred p
h : ∃ n, p n
m : ℕ+
⊢ (p m ∧ ∀ n < m, ¬p n) → PNat.find h = m

Tactic:
rintro ⟨hm, hlt⟩

Result:
case mpr.intro
p : ℕ+ → Prop
inst✝ : DecidablePred p
h : ∃ n, p n
m : ℕ+
hm : p m
hlt : ∀ n < m, ¬p n
⊢ PNat.find h = m

Proof state:
case mp
p : ℕ+ → Prop
inst✝ : DecidablePred p
h : ∃ n, p n
⊢ p (PNat.find h) ∧ ∀ n < PNat.find h, ¬p n

Tactic:
exact ⟨PNat.find_spec h, fun _ => PNat.find_min h⟩

Result:
no goals

Proof state:
case mp
p : ℕ+ → Prop
inst✝ : DecidablePred p
h : ∃ n, p n
m : ℕ+
⊢ PNat.find h = m → p m ∧ ∀ n < m, ¬p n

Tactic:
rintro rfl

Result:
case mp
p : ℕ+ → Prop
inst✝ : DecidablePred p
h : ∃ n, p n
⊢ p (PNat.find h) ∧ ∀ n < PNat.find h, ¬p n

Proof state:
case mpr.intro
p : ℕ+ → Prop
inst✝ : DecidablePred p
h : ∃ n, p n
m : ℕ+
hm : p m
hlt : ∀ n < m, ¬p n
⊢ PNat.find h = m

Tactic:
exact le_antisymm (PNat.find_min' h hm) (not_lt.1 <| imp_not_comm.1 (hlt _) <| PNat.find_spec h)

Result:
no goals
-- Mathlib/LinearAlgebra/AffineSpace/Combination.lean
theorem weightedVSubOfPoint_congr {w₁ w₂ : ι → k} (hw : ∀ i ∈ s, w₁ i = w₂ i) {p₁ p₂ : ι → P}
    (hp : ∀ i ∈ s, p₁ i = p₂ i) (b : P) :
    s.weightedVSubOfPoint p₁ b w₁ = s.weightedVSubOfPoint p₂ b w₂

Proof state:
k : Type u_1
V : Type u_2
P : Type u_3
inst✝² : Ring k
inst✝¹ : AddCommGroup V
inst✝ : Module k V
S : AffineSpace V P
ι : Type u_4
s : Finset ι
w₁ w₂ : ι → k
hw : ∀ i ∈ s, w₁ i = w₂ i
p₁ p₂ : ι → P
hp : ∀ i ∈ s, p₁ i = p₂ i
b : P
i : ι
hi : i ∈ s
⊢ w₁ i • (p₁ i -ᵥ b) = w₂ i • (p₂ i -ᵥ b)

Tactic:
rw [hw i hi, hp i hi]

Result:
no goals

Proof state:
k : Type u_1
V : Type u_2
P : Type u_3
inst✝² : Ring k
inst✝¹ : AddCommGroup V
inst✝ : Module k V
S : AffineSpace V P
ι : Type u_4
s : Finset ι
w₁ w₂ : ι → k
hw : ∀ i ∈ s, w₁ i = w₂ i
p₁ p₂ : ι → P
hp : ∀ i ∈ s, p₁ i = p₂ i
b : P
⊢ ∑ i ∈ s, w₁ i • (p₁ i -ᵥ b) = ∑ i ∈ s, w₂ i • (p₂ i -ᵥ b)

Tactic:
refine sum_congr rfl fun i hi => ?_

Result:
k : Type u_1
V : Type u_2
P : Type u_3
inst✝² : Ring k
inst✝¹ : AddCommGroup V
inst✝ : Module k V
S : AffineSpace V P
ι : Type u_4
s : Finset ι
w₁ w₂ : ι → k
hw : ∀ i ∈ s, w₁ i = w₂ i
p₁ p₂ : ι → P
hp : ∀ i ∈ s, p₁ i = p₂ i
b : P
i : ι
hi : i ∈ s
⊢ w₁ i • (p₁ i -ᵥ b) = w₂ i • (p₂ i -ᵥ b)

Proof state:
k : Type u_1
V : Type u_2
P : Type u_3
inst✝² : Ring k
inst✝¹ : AddCommGroup V
inst✝ : Module k V
S : AffineSpace V P
ι : Type u_4
s : Finset ι
w₁ w₂ : ι → k
hw : ∀ i ∈ s, w₁ i = w₂ i
p₁ p₂ : ι → P
hp : ∀ i ∈ s, p₁ i = p₂ i
b : P
⊢ (s.weightedVSubOfPoint p₁ b) w₁ = (s.weightedVSubOfPoint p₂ b) w₂

Tactic:
simp_rw [weightedVSubOfPoint_apply]

Result:
k : Type u_1
V : Type u_2
P : Type u_3
inst✝² : Ring k
inst✝¹ : AddCommGroup V
inst✝ : Module k V
S : AffineSpace V P
ι : Type u_4
s : Finset ι
w₁ w₂ : ι → k
hw : ∀ i ∈ s, w₁ i = w₂ i
p₁ p₂ : ι → P
hp : ∀ i ∈ s, p₁ i = p₂ i
b : P
⊢ ∑ i ∈ s, w₁ i • (p₁ i -ᵥ b) = ∑ i ∈ s, w₂ i • (p₂ i -ᵥ b)
-- Mathlib/AlgebraicTopology/SimplexCategory/GeneratorsRelations/EpiMono.lean
/-- A low-dimensional special case of the previous -/
private lemma switch_δ_σ₀ (i : Fin 1) (i' : Fin 2) :
    δ i' ≫ σ i = 𝟙 _

Proof state:
case «0».«0»

⊢ δ ((fun i => i) ⟨0, ⋯⟩) ≫ σ ((fun i => i) ⟨0, ⋯⟩) = 𝟙 (mk 0)

Tactic:
exact δ_comp_σ_self

Result:
no goals

Proof state:
case «0»
i' : Fin 2
⊢ δ i' ≫ σ ((fun i => i) ⟨0, ⋯⟩) = 𝟙 (mk 0)

Tactic:
fin_cases i'

Result:
case «0».«0»

⊢ δ ((fun i => i) ⟨0, ⋯⟩) ≫ σ ((fun i => i) ⟨0, ⋯⟩) = 𝟙 (mk 0)

case «0».«1»

⊢ δ ((fun i => i) ⟨1, ⋯⟩) ≫ σ ((fun i => i) ⟨0, ⋯⟩) = 𝟙 (mk 0)

Proof state:
i : Fin 1
i' : Fin 2
⊢ δ i' ≫ σ i = 𝟙 (mk 0)

Tactic:
fin_cases i

Result:
case «0»
i' : Fin 2
⊢ δ i' ≫ σ ((fun i => i) ⟨0, ⋯⟩) = 𝟙 (mk 0)

Proof state:
case «0».«1»

⊢ δ ((fun i => i) ⟨1, ⋯⟩) ≫ σ ((fun i => i) ⟨0, ⋯⟩) = 𝟙 (mk 0)

Tactic:
exact δ_comp_σ_succ

Result:
no goals
-- Mathlib/Probability/Kernel/Disintegration/CDFToKernel.lean
lemma IsRatCondKernelCDFAux.measurable_right (hf : IsRatCondKernelCDFAux f κ ν) (a : α) (q : ℚ) :
    Measurable (fun t ↦ f (a, t) q)

Proof state:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ : Kernel α (β × ℝ)
ν : Kernel α β
f : α × β → ℚ → ℝ
hf : IsRatCondKernelCDFAux f κ ν
a : α
q : ℚ
h : ∀ (a : ℚ), Measurable fun x => f x a
⊢ Measurable fun t => f (a, t) q

Tactic:
exact (h q).comp measurable_prod_mk_left

Result:
no goals

Proof state:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ : Kernel α (β × ℝ)
ν : Kernel α β
f : α × β → ℚ → ℝ
hf : IsRatCondKernelCDFAux f κ ν
a : α
q : ℚ
h : Measurable f := hf.measurable
⊢ Measurable fun t => f (a, t) q

Tactic:
rw [measurable_pi_iff] at h

Result:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ : Kernel α (β × ℝ)
ν : Kernel α β
f : α × β → ℚ → ℝ
hf : IsRatCondKernelCDFAux f κ ν
a : α
q : ℚ
h : ∀ (a : ℚ), Measurable fun x => f x a
⊢ Measurable fun t => f (a, t) q

Proof state:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ : Kernel α (β × ℝ)
ν : Kernel α β
f : α × β → ℚ → ℝ
hf : IsRatCondKernelCDFAux f κ ν
a : α
q : ℚ
⊢ Measurable fun t => f (a, t) q

Tactic:
let h := hf.measurable

Result:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ : Kernel α (β × ℝ)
ν : Kernel α β
f : α × β → ℚ → ℝ
hf : IsRatCondKernelCDFAux f κ ν
a : α
q : ℚ
h : Measurable f := hf.measurable
⊢ Measurable fun t => f (a, t) q
-- Mathlib/Analysis/SpecialFunctions/BinaryEntropy.lean
/-- Binary entropy has derivative `log (1 - p) - log p`.
It's not differentiable at `0` or `1` but the junk values of `deriv` and `log` coincide there. -/
lemma deriv_binEntropy (p : ℝ) : deriv binEntropy p = log (1 - p) - log p

Proof state:
case pos.intro
p : ℝ
hp₀ : p ≠ 0
hp₁ : 1 - p ≠ 0
⊢ deriv binEntropy p = log (1 - p) - log p

Tactic:
rw [binEntropy_eq_negMulLog_add_negMulLog_one_sub', deriv_add, deriv_comp_const_sub,
  deriv_negMulLog hp₀, deriv_negMulLog hp₁]

Result:
case pos.intro
p : ℝ
hp₀ : p ≠ 0
hp₁ : 1 - p ≠ 0
⊢ -log p - 1 + -(-log (1 - p) - 1) = log (1 - p) - log p

case pos.intro.hf
p : ℝ
hp₀ : p ≠ 0
hp₁ : 1 - p ≠ 0
⊢ DifferentiableAt ℝ negMulLog p

case pos.intro.hg
p : ℝ
hp₀ : p ≠ 0
hp₁ : 1 - p ≠ 0
⊢ DifferentiableAt ℝ (fun p => (1 - p).negMulLog) p

Proof state:
case pos.intro.hg
p : ℝ
hp₀ : p ≠ 0
hp₁ : 1 - p ≠ 0
⊢ DifferentiableAt ℝ (fun p => (1 - p).negMulLog) p

Tactic:
fun_prop (disch := assumption)

Result:
no goals

Proof state:
case pos.intro
p : ℝ
hp₀ : p ≠ 0
hp₁ : 1 - p ≠ 0
⊢ -log p - 1 + -(-log (1 - p) - 1) = log (1 - p) - log p

Tactic:
ring

Result:
no goals

Proof state:
case neg
p : ℝ
hp : p = 0 ∨ p = 1
⊢ 0 = log (1 - p) - log p

Tactic:
obtain rfl | rfl := hp <;> simp

Result:
no goals

Proof state:
case pos.intro
p : ℝ
hp₀ : p ≠ 0
hp₁ : p ≠ 1
⊢ deriv binEntropy p = log (1 - p) - log p

Tactic:
rw [ne_comm, ← sub_ne_zero] at hp₁

Result:
case pos.intro
p : ℝ
hp₀ : p ≠ 0
hp₁ : 1 - p ≠ 0
⊢ deriv binEntropy p = log (1 - p) - log p

Proof state:
p : ℝ
⊢ deriv binEntropy p = log (1 - p) - log p

Tactic:
by_cases hp : p ≠ 0 ∧ p ≠ 1

Result:
case pos
p : ℝ
hp : p ≠ 0 ∧ p ≠ 1
⊢ deriv binEntropy p = log (1 - p) - log p

case neg
p : ℝ
hp : ¬(p ≠ 0 ∧ p ≠ 1)
⊢ deriv binEntropy p = log (1 - p) - log p

Proof state:
case neg
p : ℝ
hp : ¬(p ≠ 0 ∧ p ≠ 1)
⊢ 0 = log (1 - p) - log p

Tactic:
push_neg at hp

Result:
case neg
p : ℝ
hp : p = 0 ∨ p = 1
⊢ 0 = log (1 - p) - log p

Proof state:
case neg
p : ℝ
hp : ¬(p ≠ 0 ∧ p ≠ 1)
⊢ deriv binEntropy p = log (1 - p) - log p

Tactic:
rw [deriv_zero_of_not_differentiableAt (differentiableAt_binEntropy_iff_ne_zero_one.not.2 hp)]

Result:
case neg
p : ℝ
hp : ¬(p ≠ 0 ∧ p ≠ 1)
⊢ 0 = log (1 - p) - log p

Proof state:
case pos.intro.hf
p : ℝ
hp₀ : p ≠ 0
hp₁ : 1 - p ≠ 0
⊢ DifferentiableAt ℝ negMulLog p

case pos.intro.hg
p : ℝ
hp₀ : p ≠ 0
hp₁ : 1 - p ≠ 0
⊢ DifferentiableAt ℝ (fun p => (1 - p).negMulLog) p

Tactic:
all_goals fun_prop (disch := assumption)

Result:
no goals

Proof state:
case funProp.discharger
p : ℝ
hp₀ : p ≠ 0
hp₁ : 1 - p ≠ 0
⊢ 1 - p ≠ 0

Tactic:
assumption

Result:
no goals

Proof state:
case pos
p : ℝ
hp : p ≠ 0 ∧ p ≠ 1
⊢ deriv binEntropy p = log (1 - p) - log p

Tactic:
obtain ⟨hp₀, hp₁⟩ := hp

Result:
case pos.intro
p : ℝ
hp₀ : p ≠ 0
hp₁ : p ≠ 1
⊢ deriv binEntropy p = log (1 - p) - log p
-- Mathlib/Data/Multiset/Pi.lean
theorem card_pi (m : Multiset α) (t : ∀ a, Multiset (β a)) :
    card (pi m t) = prod (m.map fun a => card (t a)) :=
  Multiset.induction_on m (by simp) (by simp +contextual [mul_comm])

Proof state:
α : Type u_1
inst✝ : DecidableEq α
β : α → Type u_2
m : Multiset α
t : (a : α) → Multiset (β a)
⊢ (pi 0 t).card = (map (fun a => (t a).card) 0).prod

Tactic:
simp

Result:
no goals

Proof state:
α : Type u_1
inst✝ : DecidableEq α
β : α → Type u_2
m : Multiset α
t : (a : α) → Multiset (β a)
⊢ ∀ (a : α) (s : Multiset α),
    (s.pi t).card = (map (fun a => (t a).card) s).prod →
      ((a ::ₘ s).pi t).card = (map (fun a => (t a).card) (a ::ₘ s)).prod

Tactic:
simp +contextual [mul_comm]

Result:
no goals
-- Mathlib/Logic/Relation.lean
theorem head_induction_on {P : ∀ a : α, ReflTransGen r a b → Prop} {a : α} (h : ReflTransGen r a b)
    (refl : P b refl)
    (head : ∀ {a c} (h' : r a c) (h : ReflTransGen r c b), P c h → P a (h.head h')) : P a h

Proof state:
case tail.head
α : Type u_1
r : α → α → Prop
b✝ a b c : α
a✝ : ReflTransGen r a b
hbc : r b c
ih :
  ∀ {P : (a : α) → ReflTransGen r a b → Prop},
    P b ⋯ → (∀ {a c : α} (h' : r a c) (h : ReflTransGen r c b), P c h → P a ⋯) → P a a✝
P : (a : α) → ReflTransGen r a c → Prop
refl : P c ⋯
head : ∀ {a c_1 : α} (h' : r a c_1) (h : ReflTransGen r c_1 c), P c_1 h → P a ⋯
⊢ ∀ {a c_1 : α} (h' : r a c_1) (h : ReflTransGen r c_1 b), P c_1 ⋯ → P a ⋯

Tactic:
exact fun h1 h2 ↦ head h1 (h2.tail hbc)

Result:
no goals

Proof state:
case refl
α : Type u_1
r : α → α → Prop
b a : α
P : (a_1 : α) → ReflTransGen r a_1 a → Prop
refl : P a ⋯
head : ∀ {a_1 c : α} (h' : r a_1 c) (h : ReflTransGen r c a), P c h → P a_1 ⋯
⊢ P a ⋯

Tactic:
exact refl

Result:
no goals

Proof state:
case tail.refl
α : Type u_1
r : α → α → Prop
b✝ a b c : α
a✝ : ReflTransGen r a b
hbc : r b c
ih :
  ∀ {P : (a : α) → ReflTransGen r a b → Prop},
    P b ⋯ → (∀ {a c : α} (h' : r a c) (h : ReflTransGen r c b), P c h → P a ⋯) → P a a✝
P : (a : α) → ReflTransGen r a c → Prop
refl : P c ⋯
head : ∀ {a c_1 : α} (h' : r a c_1) (h : ReflTransGen r c_1 c), P c_1 h → P a ⋯
⊢ P b ⋯

Tactic:
exact head hbc _ refl

Result:
no goals

Proof state:
case tail
α : Type u_1
r : α → α → Prop
b✝ a b c : α
a✝ : ReflTransGen r a b
hbc : r b c
ih :
  ∀ {P : (a : α) → ReflTransGen r a b → Prop},
    P b ⋯ → (∀ {a c : α} (h' : r a c) (h : ReflTransGen r c b), P c h → P a ⋯) → P a a✝
P : (a : α) → ReflTransGen r a c → Prop
refl : P c ⋯
head : ∀ {a c_1 : α} (h' : r a c_1) (h : ReflTransGen r c_1 c), P c_1 h → P a ⋯
⊢ P a ⋯

Tactic:
apply ih

Result:
case tail.refl
α : Type u_1
r : α → α → Prop
b✝ a b c : α
a✝ : ReflTransGen r a b
hbc : r b c
ih :
  ∀ {P : (a : α) → ReflTransGen r a b → Prop},
    P b ⋯ → (∀ {a c : α} (h' : r a c) (h : ReflTransGen r c b), P c h → P a ⋯) → P a a✝
P : (a : α) → ReflTransGen r a c → Prop
refl : P c ⋯
head : ∀ {a c_1 : α} (h' : r a c_1) (h : ReflTransGen r c_1 c), P c_1 h → P a ⋯
⊢ P b ⋯

case tail.head
α : Type u_1
r : α → α → Prop
b✝ a b c : α
a✝ : ReflTransGen r a b
hbc : r b c
ih :
  ∀ {P : (a : α) → ReflTransGen r a b → Prop},
    P b ⋯ → (∀ {a c : α} (h' : r a c) (h : ReflTransGen r c b), P c h → P a ⋯) → P a a✝
P : (a : α) → ReflTransGen r a c → Prop
refl : P c ⋯
head : ∀ {a c_1 : α} (h' : r a c_1) (h : ReflTransGen r c_1 c), P c_1 h → P a ⋯
⊢ ∀ {a c_1 : α} (h' : r a c_1) (h : ReflTransGen r c_1 b), P c_1 ⋯ → P a ⋯
-- Mathlib/MeasureTheory/Measure/WithDensity.lean
@[simp]
lemma withDensity_zero_left (f : α → ℝ≥0∞) : (0 : Measure α).withDensity f = 0

Proof state:
case h
α : Type u_1
m0 : MeasurableSpace α
f : α → ℝ≥0∞
s : Set α
hs : MeasurableSet s
⊢ ∫⁻ (a : α) in s, f a ∂0 = 0 s

Tactic:
simp

Result:
no goals

Proof state:
case h
α : Type u_1
m0 : MeasurableSpace α
f : α → ℝ≥0∞
s : Set α
hs : MeasurableSet s
⊢ (withDensity 0 f) s = 0 s

Tactic:
rw [withDensity_apply _ hs]

Result:
case h
α : Type u_1
m0 : MeasurableSpace α
f : α → ℝ≥0∞
s : Set α
hs : MeasurableSet s
⊢ ∫⁻ (a : α) in s, f a ∂0 = 0 s

Proof state:
α : Type u_1
m0 : MeasurableSpace α
f : α → ℝ≥0∞
⊢ withDensity 0 f = 0

Tactic:
ext s hs

Result:
case h
α : Type u_1
m0 : MeasurableSpace α
f : α → ℝ≥0∞
s : Set α
hs : MeasurableSet s
⊢ (withDensity 0 f) s = 0 s
-- Mathlib/GroupTheory/GroupAction/FixedPoints.lean
theorem fixedBy_mem_fixedBy_of_commute {g h : G} (comm : Commute g h) :
    (fixedBy α g) ∈ fixedBy (Set α) h

Proof state:
α : Type u_1
G : Type u_2
inst✝¹ : Group G
inst✝ : MulAction G α
g h : G
comm : Commute g h
⊢ fixedBy α g ∈ fixedBy (Set α) h

Tactic:
ext x

Result:
case h
α : Type u_1
G : Type u_2
inst✝¹ : Group G
inst✝ : MulAction G α
g h : G
comm : Commute g h
x : α
⊢ x ∈ h • fixedBy α g ↔ x ∈ fixedBy α g

Proof state:
case h
α : Type u_1
G : Type u_2
inst✝¹ : Group G
inst✝ : MulAction G α
g h : G
comm : Commute g h
x : α
⊢ x ∈ h • fixedBy α g ↔ x ∈ fixedBy α g

Tactic:
rw [Set.mem_smul_set_iff_inv_smul_mem, mem_fixedBy, ← mul_smul, comm.inv_right, mul_smul,
  smul_left_cancel_iff, mem_fixedBy]

Result:
no goals
-- Mathlib/RingTheory/MvPowerSeries/Order.lean
theorem weightedOrder_add_of_weightedOrder_lt.aux
    (H : f.weightedOrder w < g.weightedOrder w) :
    (f + g).weightedOrder w = f.weightedOrder w

Proof state:
σ : Type u_1
R : Type u_2
inst✝ : Semiring R
w : σ → ℕ
f g : MvPowerSeries σ R
H : weightedOrder w f < weightedOrder w g
⊢ weightedOrder w (f + g) = weightedOrder w f

Tactic:
obtain ⟨n, hn : (n : ℕ∞) = _⟩ := ENat.ne_top_iff_exists.mp (ne_top_of_lt H)

Result:
case intro
σ : Type u_1
R : Type u_2
inst✝ : Semiring R
w : σ → ℕ
f g : MvPowerSeries σ R
H : weightedOrder w f < weightedOrder w g
n : ℕ
hn : ↑n = weightedOrder w f
⊢ weightedOrder w (f + g) = weightedOrder w f
-- Mathlib/Algebra/Order/ToIntervalMod.lean
theorem toIocMod_eq_sub_fract_mul (a b : α) :
    toIocMod hp a b = a + p - Int.fract ((a + p - b) / p) * p

Proof state:
α : Type u_1
inst✝¹ : LinearOrderedField α
inst✝ : FloorRing α
p : α
hp : 0 < p
a b : α
⊢ b + ↑⌊(a + p - b) / p⌋ * p = a + p - (a + p - b - p * ↑⌊(a + p - b) / p⌋)

Tactic:
ring

Result:
no goals

Proof state:
α : Type u_1
inst✝¹ : LinearOrderedField α
inst✝ : FloorRing α
p : α
hp : 0 < p
a b : α
⊢ b - -⌊(a + p - b) / p⌋ • p = a + p - ((a + p - b) / p - ↑⌊(a + p - b) / p⌋) * p

Tactic:
field_simp

Result:
α : Type u_1
inst✝¹ : LinearOrderedField α
inst✝ : FloorRing α
p : α
hp : 0 < p
a b : α
⊢ b + ↑⌊(a + p - b) / p⌋ * p = a + p - (a + p - b - p * ↑⌊(a + p - b) / p⌋)

Proof state:
α : Type u_1
inst✝¹ : LinearOrderedField α
inst✝ : FloorRing α
p : α
hp : 0 < p
a b : α
⊢ toIocMod hp a b = a + p - Int.fract ((a + p - b) / p) * p

Tactic:
rw [toIocMod, toIocDiv_eq_neg_floor, Int.fract]

Result:
α : Type u_1
inst✝¹ : LinearOrderedField α
inst✝ : FloorRing α
p : α
hp : 0 < p
a b : α
⊢ b - -⌊(a + p - b) / p⌋ • p = a + p - ((a + p - b) / p - ↑⌊(a + p - b) / p⌋) * p
-- Mathlib/GroupTheory/Perm/Cycle/Factors.lean
theorem cycleOf_apply (f : Perm α) [DecidableRel f.SameCycle] (x y : α) :
    cycleOf f x y = if SameCycle f x y then f y else y

Proof state:
case neg.ha
α : Type u_2
f : Perm α
inst✝ : DecidableRel f.SameCycle
x y : α
h : ¬f.SameCycle x y
⊢ ¬f.SameCycle x y

Tactic:
exact h

Result:
no goals

Proof state:
case pos.ha
α : Type u_2
f : Perm α
inst✝ : DecidableRel f.SameCycle
x y : α
h : f.SameCycle x y
⊢ f.SameCycle x y

Tactic:
exact h

Result:
no goals

Proof state:
α : Type u_2
f : Perm α
inst✝ : DecidableRel f.SameCycle
x y : α
⊢ (f.cycleOf x) y = if f.SameCycle x y then f y else y

Tactic:
dsimp only [cycleOf]

Result:
α : Type u_2
f : Perm α
inst✝ : DecidableRel f.SameCycle
x y : α
⊢ (ofSubtype (f.subtypePerm ⋯)) y = if f.SameCycle x y then f y else y

Proof state:
α : Type u_2
f : Perm α
inst✝ : DecidableRel f.SameCycle
x y : α
⊢ (ofSubtype (f.subtypePerm ⋯)) y = if f.SameCycle x y then f y else y

Tactic:
split_ifs with h

Result:
case pos
α : Type u_2
f : Perm α
inst✝ : DecidableRel f.SameCycle
x y : α
h : f.SameCycle x y
⊢ (ofSubtype (f.subtypePerm ⋯)) y = f y

case neg
α : Type u_2
f : Perm α
inst✝ : DecidableRel f.SameCycle
x y : α
h : ¬f.SameCycle x y
⊢ (ofSubtype (f.subtypePerm ⋯)) y = y

Proof state:
case pos
α : Type u_2
f : Perm α
inst✝ : DecidableRel f.SameCycle
x y : α
h : f.SameCycle x y
⊢ (ofSubtype (f.subtypePerm ⋯)) y = f y

Tactic:
apply ofSubtype_apply_of_mem

Result:
case pos.ha
α : Type u_2
f : Perm α
inst✝ : DecidableRel f.SameCycle
x y : α
h : f.SameCycle x y
⊢ f.SameCycle x y

Proof state:
case neg
α : Type u_2
f : Perm α
inst✝ : DecidableRel f.SameCycle
x y : α
h : ¬f.SameCycle x y
⊢ (ofSubtype (f.subtypePerm ⋯)) y = y

Tactic:
apply ofSubtype_apply_of_not_mem

Result:
case neg.ha
α : Type u_2
f : Perm α
inst✝ : DecidableRel f.SameCycle
x y : α
h : ¬f.SameCycle x y
⊢ ¬f.SameCycle x y
-- Mathlib/Geometry/Euclidean/Angle/Unoriented/Basic.lean
theorem cos_eq_one_iff_angle_eq_zero : cos (angle x y) = 1 ↔ angle x y = 0

Proof state:
V : Type u_1
inst✝¹ : NormedAddCommGroup V
inst✝ : InnerProductSpace ℝ V
x y : V
⊢ cos (angle x y) = 1 ↔ angle x y = 0

Tactic:
rw [← cos_zero]

Result:
V : Type u_1
inst✝¹ : NormedAddCommGroup V
inst✝ : InnerProductSpace ℝ V
x y : V
⊢ cos (angle x y) = cos 0 ↔ angle x y = 0

Proof state:
V : Type u_1
inst✝¹ : NormedAddCommGroup V
inst✝ : InnerProductSpace ℝ V
x y : V
⊢ cos (angle x y) = cos 0 ↔ angle x y = 0

Tactic:
exact injOn_cos.eq_iff ⟨angle_nonneg x y, angle_le_pi x y⟩ (left_mem_Icc.2 pi_pos.le)

Result:
no goals
-- Mathlib/Data/Matroid/Sum.lean
@[simp] lemma sum'_isBasis_iff {I X} :
    (Matroid.sum' M).IsBasis I X ↔ ∀ i, (M i).IsBasis (Prod.mk i ⁻¹' I) (Prod.mk i ⁻¹' X)

Proof state:
α : Type u_1
ι : Type u_2
M : ι → Matroid α
I X : Set (ι × α)
a✝ : ι
⊢ ∀ (x : α), x ∈ Prod.mk a✝ ⁻¹' X ↔ x ∈ Sigma.mk a✝ ⁻¹' ((fun a => ⟨a.1, a.2⟩) '' X)

Tactic:
simp

Result:
no goals

Proof state:
α : Type u_1
ι : Type u_2
M : ι → Matroid α
I X : Set (ι × α)
⊢ (∀ (i : ι),
      (M i).IsBasis (Sigma.mk i ⁻¹' ((fun a => ⟨a.1, a.2⟩) '' I)) (Sigma.mk i ⁻¹' ((fun a => ⟨a.1, a.2⟩) '' X))) ↔
    ∀ (i : ι), (M i).IsBasis (Prod.mk i ⁻¹' I) (Prod.mk i ⁻¹' X)

Tactic:
convert Iff.rfl <;>
exact ext <| by simp

Result:
no goals

Proof state:
α : Type u_1
ι : Type u_2
M : ι → Matroid α
I X : Set (ι × α)
⊢ (Matroid.sum' M).IsBasis I X ↔ ∀ (i : ι), (M i).IsBasis (Prod.mk i ⁻¹' I) (Prod.mk i ⁻¹' X)

Tactic:
simp [Matroid.sum']

Result:
α : Type u_1
ι : Type u_2
M : ι → Matroid α
I X : Set (ι × α)
⊢ (∀ (i : ι),
      (M i).IsBasis (Sigma.mk i ⁻¹' ((fun a => ⟨a.1, a.2⟩) '' I)) (Sigma.mk i ⁻¹' ((fun a => ⟨a.1, a.2⟩) '' X))) ↔
    ∀ (i : ι), (M i).IsBasis (Prod.mk i ⁻¹' I) (Prod.mk i ⁻¹' X)
-- Mathlib/Order/KrullDimension.lean
private lemma exists_eq_iSup_of_iSup_eq_coe {α : Type*} [Nonempty α] {f : α → ℕ∞} {n : ℕ}
    (h : (⨆ x, f x) = n) : ∃ x, f x = n

Proof state:
α : Type u_3
inst✝ : Nonempty α
f : α → ℕ∞
n : ℕ
h : ⨆ x, f x = ↑n
⊢ ∃ x, f x = ↑n

Tactic:
obtain ⟨x, hx⟩ := ENat.sSup_mem_of_nonempty_of_lt_top (h ▸ ENat.coe_lt_top _)

Result:
case intro
α : Type u_3
inst✝ : Nonempty α
f : α → ℕ∞
n : ℕ
h : ⨆ x, f x = ↑n
x : α
hx : (fun x => f x) x = sSup (Set.range fun x => f x)
⊢ ∃ x, f x = ↑n

Proof state:
case intro
α : Type u_3
inst✝ : Nonempty α
f : α → ℕ∞
n : ℕ
h : ⨆ x, f x = ↑n
x : α
hx : (fun x => f x) x = sSup (Set.range fun x => f x)
⊢ ∃ x, f x = ↑n

Tactic:
use x

Result:
case h
α : Type u_3
inst✝ : Nonempty α
f : α → ℕ∞
n : ℕ
h : ⨆ x, f x = ↑n
x : α
hx : (fun x => f x) x = sSup (Set.range fun x => f x)
⊢ f x = ↑n

Proof state:
case h
α : Type u_3
inst✝ : Nonempty α
f : α → ℕ∞
n : ℕ
h : ⨆ x, f x = ↑n
x : α
hx : (fun x => f x) x = sSup (Set.range fun x => f x)
⊢ f x = ↑n

Tactic:
simpa [hx] using h

Result:
no goals
-- Mathlib/MeasureTheory/Measure/WithDensity.lean
theorem exists_measurable_le_withDensity_eq [SFinite μ] (f : α → ℝ≥0∞) :
    ∃ g, Measurable g ∧ g ≤ f ∧ μ.withDensity g = μ.withDensity f

Proof state:
case right.h
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
inst✝ : SFinite μ
f g : α → ℝ≥0∞
hgm : Measurable g
hgf : g ≤ f
hint : ∀ (s : Set α), ∫⁻ (a : α) in s, f a ∂μ = ∫⁻ (a : α) in s, g a ∂μ
s : Set α
hs : MeasurableSet s
⊢ (μ.withDensity g) s = (μ.withDensity f) s

Tactic:
simp only [hint, withDensity_apply _ hs]

Result:
no goals

Proof state:
case intro.intro.intro
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
inst✝ : SFinite μ
f g : α → ℝ≥0∞
hgm : Measurable g
hgf : g ≤ f
hint : ∀ (s : Set α), ∫⁻ (a : α) in s, f a ∂μ = ∫⁻ (a : α) in s, g a ∂μ
⊢ ∃ g, Measurable g ∧ g ≤ f ∧ μ.withDensity g = μ.withDensity f

Tactic:
use g, hgm, hgf

Result:
case right
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
inst✝ : SFinite μ
f g : α → ℝ≥0∞
hgm : Measurable g
hgf : g ≤ f
hint : ∀ (s : Set α), ∫⁻ (a : α) in s, f a ∂μ = ∫⁻ (a : α) in s, g a ∂μ
⊢ μ.withDensity g = μ.withDensity f

Proof state:
case right
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
inst✝ : SFinite μ
f g : α → ℝ≥0∞
hgm : Measurable g
hgf : g ≤ f
hint : ∀ (s : Set α), ∫⁻ (a : α) in s, f a ∂μ = ∫⁻ (a : α) in s, g a ∂μ
⊢ μ.withDensity g = μ.withDensity f

Tactic:
ext s hs

Result:
case right.h
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
inst✝ : SFinite μ
f g : α → ℝ≥0∞
hgm : Measurable g
hgf : g ≤ f
hint : ∀ (s : Set α), ∫⁻ (a : α) in s, f a ∂μ = ∫⁻ (a : α) in s, g a ∂μ
s : Set α
hs : MeasurableSet s
⊢ (μ.withDensity g) s = (μ.withDensity f) s

Proof state:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
inst✝ : SFinite μ
f : α → ℝ≥0∞
⊢ ∃ g, Measurable g ∧ g ≤ f ∧ μ.withDensity g = μ.withDensity f

Tactic:
obtain ⟨g, hgm, hgf, hint⟩ := exists_measurable_le_forall_setLIntegral_eq μ f

Result:
case intro.intro.intro
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
inst✝ : SFinite μ
f g : α → ℝ≥0∞
hgm : Measurable g
hgf : g ≤ f
hint : ∀ (s : Set α), ∫⁻ (a : α) in s, f a ∂μ = ∫⁻ (a : α) in s, g a ∂μ
⊢ ∃ g, Measurable g ∧ g ≤ f ∧ μ.withDensity g = μ.withDensity f
-- Mathlib/Order/CompactlyGenerated/Basic.lean
theorem sSup_compact_le_eq (b) :
    sSup { c : α | CompleteLattice.IsCompactElement c ∧ c ≤ b } = b

Proof state:
case intro.intro
α : Type u_2
inst✝¹ : CompleteLattice α
inst✝ : IsCompactlyGenerated α
s : Set α
hs : ∀ x ∈ s, CompleteLattice.IsCompactElement x
⊢ sSup {c | CompleteLattice.IsCompactElement c ∧ c ≤ sSup s} = sSup s

Tactic:
exact le_antisymm (sSup_le fun c hc => hc.2) (sSup_le_sSup fun c cs => ⟨hs c cs, le_sSup cs⟩)

Result:
no goals

Proof state:
α : Type u_2
inst✝¹ : CompleteLattice α
inst✝ : IsCompactlyGenerated α
b : α
⊢ sSup {c | CompleteLattice.IsCompactElement c ∧ c ≤ b} = b

Tactic:
rcases IsCompactlyGenerated.exists_sSup_eq b with ⟨s, hs, rfl⟩

Result:
case intro.intro
α : Type u_2
inst✝¹ : CompleteLattice α
inst✝ : IsCompactlyGenerated α
s : Set α
hs : ∀ x ∈ s, CompleteLattice.IsCompactElement x
⊢ sSup {c | CompleteLattice.IsCompactElement c ∧ c ≤ sSup s} = sSup s