harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/Data/Bool/Count.lean
theorem count_not_le_count_add_one (hl : Chain' (· ≠ ·) l) (b : Bool) :
    count (!b) l ≤ count b l + 1

Proof state:
case cons
b x : Bool
l : List Bool
hl : Chain' (fun x1 x2 => x1 ≠ x2) (x :: l)
⊢ count (!b) (x :: l) ≤ count b (x :: l) + 1

Tactic:
obtain rfl | rfl : b = x ∨ b = !x := by simp only [Bool.eq_not_iff, em]

Result:
case cons.inl
b : Bool
l : List Bool
hl : Chain' (fun x1 x2 => x1 ≠ x2) (b :: l)
⊢ count (!b) (b :: l) ≤ count b (b :: l) + 1

case cons.inr
x : Bool
l : List Bool
hl : Chain' (fun x1 x2 => x1 ≠ x2) (x :: l)
⊢ count (!!x) (x :: l) ≤ count (!x) (x :: l) + 1

Proof state:
case cons.inl
b : Bool
l : List Bool
hl : Chain' (fun x1 x2 => x1 ≠ x2) (b :: l)
⊢ count (!b) (b :: l) ≤ count b (b :: l) + 1

Tactic:
rw [count_cons_of_ne b.not_ne_self, count_cons_self, hl.count_not, add_assoc]

Result:
case cons.inl
b : Bool
l : List Bool
hl : Chain' (fun x1 x2 => x1 ≠ x2) (b :: l)
⊢ count b l + l.length % 2 ≤ count b l + (1 + 1)

Proof state:
l : List Bool
hl : Chain' (fun x1 x2 => x1 ≠ x2) l
b : Bool
⊢ count (!b) l ≤ count b l + 1

Tactic:
rcases l with - | ⟨x, l⟩

Result:
case nil
b : Bool
hl : Chain' (fun x1 x2 => x1 ≠ x2) []
⊢ count (!b) [] ≤ count b [] + 1

case cons
b x : Bool
l : List Bool
hl : Chain' (fun x1 x2 => x1 ≠ x2) (x :: l)
⊢ count (!b) (x :: l) ≤ count b (x :: l) + 1

Proof state:
case cons.inl
b : Bool
l : List Bool
hl : Chain' (fun x1 x2 => x1 ≠ x2) (b :: l)
⊢ count b l + l.length % 2 ≤ count b l + (1 + 1)

Tactic:
exact add_le_add_left (Nat.mod_lt _ two_pos).le _

Result:
no goals

Proof state:
case cons.inr
x : Bool
l : List Bool
hl : Chain' (fun x1 x2 => x1 ≠ x2) (x :: l)
⊢ count x l + 1 ≤ count x l + l.length % 2 + 1

Tactic:
exact add_le_add_right (le_add_right le_rfl) _

Result:
no goals

Proof state:
b x : Bool
l : List Bool
hl : Chain' (fun x1 x2 => x1 ≠ x2) (x :: l)
⊢ b = x ∨ b = !x

Tactic:
simp only [Bool.eq_not_iff, em]

Result:
no goals

Proof state:
case nil
b : Bool
hl : Chain' (fun x1 x2 => x1 ≠ x2) []
⊢ count (!b) [] ≤ count b [] + 1

Tactic:
exact zero_le _

Result:
no goals

Proof state:
case cons.inr
x : Bool
l : List Bool
hl : Chain' (fun x1 x2 => x1 ≠ x2) (x :: l)
⊢ count (!!x) (x :: l) ≤ count (!x) (x :: l) + 1

Tactic:
rw [Bool.not_not, count_cons_self, count_cons_of_ne x.not_ne_self, hl.count_not]

Result:
case cons.inr
x : Bool
l : List Bool
hl : Chain' (fun x1 x2 => x1 ≠ x2) (x :: l)
⊢ count x l + 1 ≤ count x l + l.length % 2 + 1
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Nat/Lemmas.lean
theorem one_mod_two_pow_eq_one : 1 % 2 ^ n = 1 ↔ 0 < n

Proof state:
case succ
n : Nat
⊢ 1 = 1 ↔ 0 < n + 1

Tactic:
simp

Result:
no goals

Proof state:
n : Nat
⊢ 1 % 2 ^ n = 1 ↔ 0 < n

Tactic:
cases n with
| zero => simp
| succ n =>
  rw [mod_eq_of_lt (a := 1) (Nat.one_lt_two_pow (by omega))]
  simp

Result:
no goals

Proof state:
case zero

⊢ 1 % 2 ^ 0 = 1 ↔ 0 < 0

Tactic:
simp

Result:
no goals

Proof state:
n : Nat
⊢ n + 1 ≠ 0

Tactic:
omega

Result:
no goals

Proof state:
case succ
n : Nat
⊢ 1 % 2 ^ (n + 1) = 1 ↔ 0 < n + 1

Tactic:
rw [mod_eq_of_lt (a := 1) (Nat.one_lt_two_pow (by omega))]

Result:
case succ
n : Nat
⊢ 1 = 1 ↔ 0 < n + 1
-- Mathlib/Order/Interval/Finset/Nat.lean
theorem Iio_eq_range : Iio = range

Proof state:
case h.h
b x : ℕ
⊢ x ∈ Iio b ↔ x ∈ range b

Tactic:
rw [mem_Iio, mem_range]

Result:
no goals

Proof state:
⊢ Iio = range

Tactic:
ext b x

Result:
case h.h
b x : ℕ
⊢ x ∈ Iio b ↔ x ∈ range b
-- Mathlib/Data/ENNReal/Basic.lean
theorem lt_iff_exists_add_pos_lt : a < b ↔ ∃ r : ℝ≥0, 0 < r ∧ a + r < b

Proof state:
a b : ℝ≥0∞
⊢ a < b ↔ ∃ r, 0 < r ∧ a + ↑r < b

Tactic:
refine ⟨fun hab => ?_, fun ⟨r, _, hr⟩ => lt_of_le_of_lt le_self_add hr⟩

Result:
a b : ℝ≥0∞
hab : a < b
⊢ ∃ r, 0 < r ∧ a + ↑r < b

Proof state:
case intro.intro.intro
b : ℝ≥0∞
c : ℝ≥0
cb : ↑c < b
a : ℝ≥0
hab : ↑a < b
ac : a < c
⊢ ↑a + ↑(c - a) < b

Tactic:
rwa [← coe_add, add_tsub_cancel_of_le ac.le]

Result:
no goals

Proof state:
case intro.intro
a b : ℝ≥0∞
hab : a < b
c : ℝ≥0
ac : a < ↑c
cb : ↑c < b
⊢ ∃ r, 0 < r ∧ a + ↑r < b

Tactic:
lift a to ℝ≥0 using ac.ne_top

Result:
case intro.intro.intro
b : ℝ≥0∞
c : ℝ≥0
cb : ↑c < b
a : ℝ≥0
hab : ↑a < b
ac : ↑a < ↑c
⊢ ∃ r, 0 < r ∧ ↑a + ↑r < b

Proof state:
a b : ℝ≥0∞
hab : a < b
⊢ ∃ r, 0 < r ∧ a + ↑r < b

Tactic:
rcases lt_iff_exists_nnreal_btwn.1 hab with ⟨c, ac, cb⟩

Result:
case intro.intro
a b : ℝ≥0∞
hab : a < b
c : ℝ≥0
ac : a < ↑c
cb : ↑c < b
⊢ ∃ r, 0 < r ∧ a + ↑r < b

Proof state:
case intro.intro.intro
b : ℝ≥0∞
c : ℝ≥0
cb : ↑c < b
a : ℝ≥0
hab : ↑a < b
ac : a < c
⊢ ∃ r, 0 < r ∧ ↑a + ↑r < b

Tactic:
refine ⟨c - a, tsub_pos_iff_lt.2 ac, ?_⟩

Result:
case intro.intro.intro
b : ℝ≥0∞
c : ℝ≥0
cb : ↑c < b
a : ℝ≥0
hab : ↑a < b
ac : a < c
⊢ ↑a + ↑(c - a) < b

Proof state:
case intro.intro.intro
b : ℝ≥0∞
c : ℝ≥0
cb : ↑c < b
a : ℝ≥0
hab : ↑a < b
ac : ↑a < ↑c
⊢ ∃ r, 0 < r ∧ ↑a + ↑r < b

Tactic:
rw [coe_lt_coe] at ac

Result:
case intro.intro.intro
b : ℝ≥0∞
c : ℝ≥0
cb : ↑c < b
a : ℝ≥0
hab : ↑a < b
ac : a < c
⊢ ∃ r, 0 < r ∧ ↑a + ↑r < b
-- Mathlib/Probability/Independence/ZeroOne.lean
theorem Kernel.indep_iSup_directed_limsup (h_le : ∀ n, s n ≤ m0) (h_indep : iIndep s κ μα)
    (hf : ∀ t, p t → tᶜ ∈ f) (hns : Directed (· ≤ ·) ns) (hnsp : ∀ a, p (ns a)) :
    Indep (⨆ a, ⨆ n ∈ ns a, s n) (limsup s f) κ μα

Proof state:
case inr.intro.intro.hm.intro
α : Type u_1
Ω : Type u_2
ι : Type u_3
_mα : MeasurableSpace α
s : ι → MeasurableSpace Ω
m0 : MeasurableSpace Ω
κ : Kernel α Ω
μα : Measure α
β : Type u_4
p : Set ι → Prop
f : Filter ι
ns : β → Set ι
h_le : ∀ (n : ι), s n ≤ m0
hf : ∀ (t : Set ι), p t → tᶜ ∈ f
hns : Directed (fun x1 x2 => x1 ≤ x2) ns
hnsp : ∀ (a : β), p (ns a)
hμ : μα ≠ 0
η : Kernel α Ω
η_eq : ⇑κ =ᶠ[ae μα] ⇑η
hη : IsMarkovKernel η
h_indep : iIndep s η μα
a b c : β
hc : (fun x1 x2 => x1 ≤ x2) (ns a) (ns c) ∧ (fun x1 x2 => x1 ≤ x2) (ns b) (ns c)
⊢ ∃ z,
    (fun x1 x2 => x1 ≤ x2) ((fun i => ⨆ n ∈ ns i, s n) a) ((fun i => ⨆ n ∈ ns i, s n) z) ∧
      (fun x1 x2 => x1 ≤ x2) ((fun i => ⨆ n ∈ ns i, s n) b) ((fun i => ⨆ n ∈ ns i, s n) z)

Tactic:
refine ⟨c, ?_, ?_⟩ <;> refine iSup_mono fun n => iSup_mono' fun hn => ⟨?_, le_rfl⟩

Result:
case inr.intro.intro.hm.intro.refine_1
α : Type u_1
Ω : Type u_2
ι : Type u_3
_mα : MeasurableSpace α
s : ι → MeasurableSpace Ω
m0 : MeasurableSpace Ω
κ : Kernel α Ω
μα : Measure α
β : Type u_4
p : Set ι → Prop
f : Filter ι
ns : β → Set ι
h_le : ∀ (n : ι), s n ≤ m0
hf : ∀ (t : Set ι), p t → tᶜ ∈ f
hns : Directed (fun x1 x2 => x1 ≤ x2) ns
hnsp : ∀ (a : β), p (ns a)
hμ : μα ≠ 0
η : Kernel α Ω
η_eq : ⇑κ =ᶠ[ae μα] ⇑η
hη : IsMarkovKernel η
h_indep : iIndep s η μα
a b c : β
hc : (fun x1 x2 => x1 ≤ x2) (ns a) (ns c) ∧ (fun x1 x2 => x1 ≤ x2) (ns b) (ns c)
n : ι
hn : n ∈ ns a
⊢ n ∈ ns c

case inr.intro.intro.hm.intro.refine_2
α : Type u_1
Ω : Type u_2
ι : Type u_3
_mα : MeasurableSpace α
s : ι → MeasurableSpace Ω
m0 : MeasurableSpace Ω
κ : Kernel α Ω
μα : Measure α
β : Type u_4
p : Set ι → Prop
f : Filter ι
ns : β → Set ι
h_le : ∀ (n : ι), s n ≤ m0
hf : ∀ (t : Set ι), p t → tᶜ ∈ f
hns : Directed (fun x1 x2 => x1 ≤ x2) ns
hnsp : ∀ (a : β), p (ns a)
hμ : μα ≠ 0
η : Kernel α Ω
η_eq : ⇑κ =ᶠ[ae μα] ⇑η
hη : IsMarkovKernel η
h_indep : iIndep s η μα
a b c : β
hc : (fun x1 x2 => x1 ≤ x2) (ns a) (ns c) ∧ (fun x1 x2 => x1 ≤ x2) (ns b) (ns c)
n : ι
hn : n ∈ ns b
⊢ n ∈ ns c
-- Mathlib/MeasureTheory/PiSystem.lean
theorem generateFrom_piiUnionInter_le {m : MeasurableSpace α} (π : ι → Set (Set α))
    (h : ∀ n, generateFrom (π n) ≤ m) (S : Set ι) : generateFrom (piiUnionInter π S) ≤ m

Proof state:
case intro.intro.intro.intro
α : Type u_3
ι : Type u_4
m : MeasurableSpace α
π : ι → Set (Set α)
h : ∀ (n : ι), generateFrom (π n) ≤ m
S : Set ι
ht_p : Finset ι
w✝ : ↑ht_p ⊆ S
ft : ι → Set α
hft_mem_pi : ∀ x ∈ ht_p, ft x ∈ π x
x : ι
hx_mem : x ∈ ht_p
⊢ MeasurableSet (ft x)

Tactic:
exact measurableSet_generateFrom (hft_mem_pi x hx_mem)

Result:
no goals

Proof state:
α : Type u_3
ι : Type u_4
m : MeasurableSpace α
π : ι → Set (Set α)
h : ∀ (n : ι), generateFrom (π n) ≤ m
S : Set ι
⊢ generateFrom (piiUnionInter π S) ≤ m

Tactic:
refine generateFrom_le ?_

Result:
α : Type u_3
ι : Type u_4
m : MeasurableSpace α
π : ι → Set (Set α)
h : ∀ (n : ι), generateFrom (π n) ≤ m
S : Set ι
⊢ ∀ t ∈ piiUnionInter π S, MeasurableSet t

Proof state:
case intro.intro.intro.intro
α : Type u_3
ι : Type u_4
m : MeasurableSpace α
π : ι → Set (Set α)
h : ∀ (n : ι), generateFrom (π n) ≤ m
S : Set ι
ht_p : Finset ι
w✝ : ↑ht_p ⊆ S
ft : ι → Set α
hft_mem_pi : ∀ x ∈ ht_p, ft x ∈ π x
⊢ MeasurableSet (⋂ x ∈ ht_p, ft x)

Tactic:
refine Finset.measurableSet_biInter _ fun x hx_mem => (h x) _ ?_

Result:
case intro.intro.intro.intro
α : Type u_3
ι : Type u_4
m : MeasurableSpace α
π : ι → Set (Set α)
h : ∀ (n : ι), generateFrom (π n) ≤ m
S : Set ι
ht_p : Finset ι
w✝ : ↑ht_p ⊆ S
ft : ι → Set α
hft_mem_pi : ∀ x ∈ ht_p, ft x ∈ π x
x : ι
hx_mem : x ∈ ht_p
⊢ MeasurableSet (ft x)

Proof state:
α : Type u_3
ι : Type u_4
m : MeasurableSpace α
π : ι → Set (Set α)
h : ∀ (n : ι), generateFrom (π n) ≤ m
S : Set ι
⊢ ∀ t ∈ piiUnionInter π S, MeasurableSet t

Tactic:
rintro t ⟨ht_p, _, ft, hft_mem_pi, rfl⟩

Result:
case intro.intro.intro.intro
α : Type u_3
ι : Type u_4
m : MeasurableSpace α
π : ι → Set (Set α)
h : ∀ (n : ι), generateFrom (π n) ≤ m
S : Set ι
ht_p : Finset ι
w✝ : ↑ht_p ⊆ S
ft : ι → Set α
hft_mem_pi : ∀ x ∈ ht_p, ft x ∈ π x
⊢ MeasurableSet (⋂ x ∈ ht_p, ft x)
-- Mathlib/MeasureTheory/Function/L1Space/Integrable.lean
lemma MemLp.integrable_norm_pow {f : α → β} {p : ℕ} (hf : MemLp f p μ) (hp : p ≠ 0) :
    Integrable (fun x : α => ‖f x‖ ^ p) μ

Proof state:
α : Type u_1
β : Type u_2
m : MeasurableSpace α
μ : Measure α
inst✝ : NormedAddCommGroup β
f : α → β
p : ℕ
hf : MemLp f (↑p) μ
hp : p ≠ 0
⊢ ↑p ≠ ⊤

Tactic:
simp

Result:
no goals

Proof state:
α : Type u_1
β : Type u_2
m : MeasurableSpace α
μ : Measure α
inst✝ : NormedAddCommGroup β
f : α → β
p : ℕ
hf : MemLp f (↑p) μ
hp : p ≠ 0
⊢ Integrable (fun x => ‖f x‖ ^ p) μ

Tactic:
simpa using hf.integrable_norm_rpow (mod_cast hp) (by simp)

Result:
no goals
-- Mathlib/Order/Sublattice.lean
lemma le_prod_iff {M : Sublattice β} {N : Sublattice (α × β)} :
    N ≤ L.prod M ↔ N ≤ comap LatticeHom.fst L ∧ N ≤ comap LatticeHom.snd M

Proof state:
α : Type u_2
β : Type u_3
inst✝¹ : Lattice α
inst✝ : Lattice β
L : Sublattice α
M : Sublattice β
N : Sublattice (α × β)
⊢ N ≤ L.prod M ↔ N ≤ comap LatticeHom.fst L ∧ N ≤ comap LatticeHom.snd M

Tactic:
simp [SetLike.le_def, forall_and]

Result:
no goals
-- Mathlib/Algebra/Module/ZLattice/Basic.lean
theorem fundamentalDomain_subset_parallelepiped [Fintype ι] :
    fundamentalDomain b ⊆ parallelepiped b

Proof state:
E : Type u_1
ι : Type u_2
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
b : Basis ι ℝ E
inst✝ : Fintype ι
⊢ fundamentalDomain b ⊆ parallelepiped ⇑b

Tactic:
rw [fundamentalDomain, parallelepiped_basis_eq, Set.setOf_subset_setOf]

Result:
E : Type u_1
ι : Type u_2
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
b : Basis ι ℝ E
inst✝ : Fintype ι
⊢ ∀ (a : E), (∀ (i : ι), (b.repr a) i ∈ Set.Ico 0 1) → ∀ (i : ι), (b.repr a) i ∈ Set.Icc 0 1

Proof state:
E : Type u_1
ι : Type u_2
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
b : Basis ι ℝ E
inst✝ : Fintype ι
⊢ ∀ (a : E), (∀ (i : ι), (b.repr a) i ∈ Set.Ico 0 1) → ∀ (i : ι), (b.repr a) i ∈ Set.Icc 0 1

Tactic:
exact fun _ h i ↦ Set.Ico_subset_Icc_self (h i)

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Array/Lemmas.lean
theorem size_filterMap_le (f : α → Option β) (l : Array α) :
    (filterMap f l).size ≤ l.size

Proof state:
α : Type u_1
β : Type u_2
f : α → Option β
l : Array α
⊢ (filterMap f l).size ≤ l.size

Tactic:
cases l

Result:
case mk
α : Type u_1
β : Type u_2
f : α → Option β
toList✝ : List α
⊢ (filterMap f { toList := toList✝ }).size ≤ { toList := toList✝ }.size

Proof state:
case mk
α : Type u_1
β : Type u_2
f : α → Option β
toList✝ : List α
⊢ (filterMap f { toList := toList✝ }).size ≤ { toList := toList✝ }.size

Tactic:
simp [List.length_filterMap_le]

Result:
no goals
-- Mathlib/MeasureTheory/VectorMeasure/Basic.lean
theorem zero_le_toSignedMeasure : 0 ≤ μ.toSignedMeasure

Proof state:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
inst✝ : IsFiniteMeasure μ
j : Set α
hj₁ : MeasurableSet j
x✝ : j ⊆ univ
⊢ ↑0 j ≤ ↑μ.toSignedMeasure j

Tactic:
simp only [Measure.toSignedMeasure_apply_measurable hj₁, coe_zero, Pi.zero_apply,
  ENNReal.toReal_nonneg, VectorMeasure.coe_zero]

Result:
no goals

Proof state:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
inst✝ : IsFiniteMeasure μ
⊢ 0 ≤ μ.toSignedMeasure

Tactic:
rw [← le_restrict_univ_iff_le]

Result:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
inst✝ : IsFiniteMeasure μ
⊢ 0 ≤[univ] μ.toSignedMeasure

Proof state:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
inst✝ : IsFiniteMeasure μ
⊢ 0 ≤[univ] μ.toSignedMeasure

Tactic:
refine restrict_le_restrict_of_subset_le _ _ fun j hj₁ _ => ?_

Result:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
inst✝ : IsFiniteMeasure μ
j : Set α
hj₁ : MeasurableSet j
x✝ : j ⊆ univ
⊢ ↑0 j ≤ ↑μ.toSignedMeasure j
-- Mathlib/Data/Holor.lean
theorem cast_type (is : List ℕ) (eq : ds₁ = ds₂) (h : Forall₂ (· < ·) is ds₁) :
    (cast (congr_arg HolorIndex eq) ⟨is, h⟩).val = is

Proof state:
ds₁ is : List ℕ
h : Forall₂ (fun x1 x2 => x1 < x2) is ds₁
⊢ ↑(cast ⋯ ⟨is, h⟩) = is

Tactic:
rfl

Result:
no goals

Proof state:
ds₁ ds₂ is : List ℕ
eq : ds₁ = ds₂
h : Forall₂ (fun x1 x2 => x1 < x2) is ds₁
⊢ ↑(cast ⋯ ⟨is, h⟩) = is

Tactic:
subst eq

Result:
ds₁ is : List ℕ
h : Forall₂ (fun x1 x2 => x1 < x2) is ds₁
⊢ ↑(cast ⋯ ⟨is, h⟩) = is
-- Mathlib/SetTheory/Ordinal/Arithmetic.lean
theorem add_one_of_aleph0_le {c} (h : ℵ₀ ≤ c) : c + 1 = c

Proof state:
c : Cardinal.{u_1}
h : ℵ₀ ≤ c
⊢ c + 1 = c

Tactic:
rw [add_comm, ← card_ord c, ← card_one, ← card_add, one_add_of_omega0_le]

Result:
c : Cardinal.{u_1}
h : ℵ₀ ≤ c
⊢ ω ≤ c.ord

Proof state:
c : Cardinal.{u_1}
h : ℵ₀ ≤ c
⊢ ω ≤ c.ord

Tactic:
rwa [← ord_aleph0, ord_le_ord]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Std/Data/DHashMap/Lemmas.lean
theorem get_alter_self [EquivBEq α] [LawfulHashable α] {k : α} {f : Option β → Option β}
    {h : k ∈ Const.alter m k f} :
    haveI h' : (f (Const.get? m k)).isSome := mem_alter_self.mp h
    Const.get (Const.alter m k f) k h = (f (Const.get? m k)).get h'

Proof state:
α : Type u
x✝¹ : BEq α
x✝ : Hashable α
β : Type v
m : DHashMap α fun x => β
inst✝¹ : EquivBEq α
inst✝ : LawfulHashable α
k : α
f : Option β → Option β
h : k ∈ alter m k f
⊢ get (alter m k f) k h = (f (get? m k)).get ⋯

Tactic:
simp [get_alter]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Std/Data/DHashMap/Internal/RawLemmas.lean
theorem get!_eq_get! [LawfulBEq α] [Inhabited β] (h : m.1.WF) {a : α} :
    get! m a = m.get! a

Proof state:
α : Type u
inst✝³ : BEq α
inst✝² : Hashable α
β : Type v
m : Raw₀ α fun x => β
inst✝¹ : LawfulBEq α
inst✝ : Inhabited β
h : m.val.WF
a : α
⊢ get! m a = m.get! a

Tactic:
simp_to_model using List.getValue!_eq_getValueCast!

Result:
no goals
-- Mathlib/CategoryTheory/NatIso.lean
theorem isIso_of_isIso_app (α : F ⟶ G) [∀ X : C, IsIso (α.app X)] : IsIso α :=
  (ofComponents (fun X => asIso (α.app X)) (by simp)).isIso_hom

Proof state:
C : Type u₁
inst✝² : Category.{v₁, u₁} C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
F G : C ⥤ D
α : F ⟶ G
inst✝ : ∀ (X : C), IsIso (α.app X)
⊢ ∀ {X Y : C} (f : X ⟶ Y), F.map f ≫ ((fun X => asIso (α.app X)) Y).hom = ((fun X => asIso (α.app X)) X).hom ≫ G.map f

Tactic:
simp

Result:
no goals
-- Mathlib/Algebra/CubicDiscriminant.lean
theorem disc_ne_zero_iff_roots_ne (ha : P.a ≠ 0) (h3 : (map φ P).roots = {x, y, z}) :
    P.disc ≠ 0 ↔ x ≠ y ∧ x ≠ z ∧ y ≠ z

Proof state:
F : Type u_3
K : Type u_4
P : Cubic F
inst✝¹ : Field F
inst✝ : Field K
φ : F →+* K
x y z : K
ha : P.a ≠ 0
h3 : (map φ P).roots = {x, y, z}
⊢ P.disc ≠ 0 ↔ x ≠ y ∧ x ≠ z ∧ y ≠ z

Tactic:
rw [← _root_.map_ne_zero φ, disc_eq_prod_three_roots ha h3, pow_two]

Result:
F : Type u_3
K : Type u_4
P : Cubic F
inst✝¹ : Field F
inst✝ : Field K
φ : F →+* K
x y z : K
ha : P.a ≠ 0
h3 : (map φ P).roots = {x, y, z}
⊢ φ P.a * φ P.a * (x - y) * (x - z) * (y - z) * (φ P.a * φ P.a * (x - y) * (x - z) * (y - z)) ≠ 0 ↔
    x ≠ y ∧ x ≠ z ∧ y ≠ z

Proof state:
F : Type u_3
K : Type u_4
P : Cubic F
inst✝¹ : Field F
inst✝ : Field K
φ : F →+* K
x y z : K
ha : P.a ≠ 0
h3 : (map φ P).roots = {x, y, z}
⊢ φ P.a * φ P.a * (x - y) * (x - z) * (y - z) * (φ P.a * φ P.a * (x - y) * (x - z) * (y - z)) ≠ 0 ↔
    x ≠ y ∧ x ≠ z ∧ y ≠ z

Tactic:
simp_rw [mul_ne_zero_iff, sub_ne_zero, _root_.map_ne_zero, and_self_iff, and_iff_right ha,
  and_assoc]

Result:
no goals
-- Mathlib/Data/Seq/Computation.lean
theorem map_congr {s1 s2 : Computation α} {f : α → β}
    (h1 : s1 ~ s2) : map f s1 ~ map f s2

Proof state:
α : Type u
β : Type v
s1 s2 : Computation α
f : α → β
h1 : s1 ~ s2
⊢ map f s1 ~ map f s2

Tactic:
rw [← lift_eq_iff_equiv]

Result:
α : Type u
β : Type v
s1 s2 : Computation α
f : α → β
h1 : s1 ~ s2
⊢ LiftRel (fun x1 x2 => x1 = x2) (map f s1) (map f s2)

Proof state:
α : Type u
β : Type v
s1 s2 : Computation α
f : α → β
h1 : s1 ~ s2
⊢ LiftRel (fun x1 x2 => x1 = x2) (map f s1) (map f s2)

Tactic:
exact liftRel_map Eq _ ((lift_eq_iff_equiv _ _).2 h1) fun {a} b => congr_arg _

Result:
no goals
-- Mathlib/Combinatorics/Enumerative/DyckWord.lean
@[simp]
lemma outsidePart_nest : p.nest.outsidePart = 0

Proof state:
case h
p : DyckWord
⊢ 1 + (↑p).length + 1 ≤ (↑p).length + 1 + 1

Tactic:
omega

Result:
no goals

Proof state:
p : DyckWord
⊢ ↑(p.nest.drop ((↑p).length + 1 + 1) ⋯) = ↑0

Tactic:
apply drop_of_length_le

Result:
case h
p : DyckWord
⊢ (↑p.nest).length ≤ (↑p).length + 1 + 1

Proof state:
case h
p : DyckWord
⊢ (↑p.nest).length ≤ (↑p).length + 1 + 1

Tactic:
simp_rw [nest, length_append, length_singleton]

Result:
case h
p : DyckWord
⊢ 1 + (↑p).length + 1 ≤ (↑p).length + 1 + 1

Proof state:
p : DyckWord
⊢ p.nest.drop ((↑p).length + 1 + 1) ⋯ = 0

Tactic:
rw [DyckWord.ext_iff]

Result:
p : DyckWord
⊢ ↑(p.nest.drop ((↑p).length + 1 + 1) ⋯) = ↑0

Proof state:
p : DyckWord
⊢ p.nest.outsidePart = 0

Tactic:
simp_rw [outsidePart, nest_ne_zero, dite_false, firstReturn_nest]

Result:
p : DyckWord
⊢ p.nest.drop ((↑p).length + 1 + 1) ⋯ = 0
-- Mathlib/Probability/Distributions/Pareto.lean
/-- CDF of the Pareto distribution equals the integral of the PDF. -/
lemma paretoCDFReal_eq_integral (ht : 0 < t) (hr : 0 < r) (x : ℝ) :
    cdf (paretoMeasure t r) x = ∫ x in Iic x, paretoPDFReal t r x

Proof state:
t r : ℝ
ht : 0 < t
hr : 0 < r
x : ℝ
⊢ ↑(cdf (paretoMeasure t r)) x = ∫ (x : ℝ) in Iic x, paretoPDFReal t r x

Tactic:
have : IsProbabilityMeasure (paretoMeasure t r) := isProbabilityMeasure_paretoMeasure ht hr

Result:
t r : ℝ
ht : 0 < t
hr : 0 < r
x : ℝ
this : IsProbabilityMeasure (paretoMeasure t r)
⊢ ↑(cdf (paretoMeasure t r)) x = ∫ (x : ℝ) in Iic x, paretoPDFReal t r x

Proof state:
t r : ℝ
ht : 0 < t
hr : 0 < r
x : ℝ
this : IsProbabilityMeasure (paretoMeasure t r)
x✝ : ℝ
⊢ 0 x✝ ≤ paretoPDFReal t r x✝

Tactic:
simp only [Pi.zero_apply, paretoPDFReal_nonneg ht.le hr.le]

Result:
no goals

Proof state:
t r : ℝ
ht : 0 < t
hr : 0 < r
x : ℝ
this : IsProbabilityMeasure (paretoMeasure t r)
⊢ ↑(cdf (paretoMeasure t r)) x = ∫ (x : ℝ) in Iic x, paretoPDFReal t r x

Tactic:
rw [cdf_eq_toReal, paretoMeasure, withDensity_apply _ measurableSet_Iic]

Result:
t r : ℝ
ht : 0 < t
hr : 0 < r
x : ℝ
this : IsProbabilityMeasure (paretoMeasure t r)
⊢ (∫⁻ (a : ℝ) in Iic x, paretoPDF t r a).toReal = ∫ (x : ℝ) in Iic x, paretoPDFReal t r x

Proof state:
case refine_2
t r : ℝ
ht : 0 < t
hr : 0 < r
x : ℝ
this : IsProbabilityMeasure (paretoMeasure t r)
⊢ AEStronglyMeasurable (paretoPDFReal t r) (ℙ.restrict (Iic x))

Tactic:
exact (measurable_paretoPDFReal t r).aestronglyMeasurable.restrict

Result:
no goals

Proof state:
t r : ℝ
ht : 0 < t
hr : 0 < r
x : ℝ
this : IsProbabilityMeasure (paretoMeasure t r)
⊢ (∫⁻ (a : ℝ) in Iic x, paretoPDF t r a).toReal = ∫ (x : ℝ) in Iic x, paretoPDFReal t r x

Tactic:
refine (integral_eq_lintegral_of_nonneg_ae ?_ ?_).symm

Result:
case refine_1
t r : ℝ
ht : 0 < t
hr : 0 < r
x : ℝ
this : IsProbabilityMeasure (paretoMeasure t r)
⊢ 0 ≤ᶠ[ae (ℙ.restrict (Iic x))] paretoPDFReal t r

case refine_2
t r : ℝ
ht : 0 < t
hr : 0 < r
x : ℝ
this : IsProbabilityMeasure (paretoMeasure t r)
⊢ AEStronglyMeasurable (paretoPDFReal t r) (ℙ.restrict (Iic x))

Proof state:
case refine_1
t r : ℝ
ht : 0 < t
hr : 0 < r
x : ℝ
this : IsProbabilityMeasure (paretoMeasure t r)
⊢ 0 ≤ᶠ[ae (ℙ.restrict (Iic x))] paretoPDFReal t r

Tactic:
exact ae_of_all _ fun _ ↦ by simp only [Pi.zero_apply, paretoPDFReal_nonneg ht.le hr.le]

Result:
no goals
-- Mathlib/LinearAlgebra/TensorAlgebra/ToTensorPower.lean
theorem ofDirectSum_comp_toDirectSum :
    ofDirectSum.comp toDirectSum = AlgHom.id R (TensorAlgebra R M)

Proof state:
R : Type u_1
M : Type u_2
inst✝² : CommSemiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
⊢ ofDirectSum.comp toDirectSum = AlgHom.id R (TensorAlgebra R M)

Tactic:
ext

Result:
case w.h
R : Type u_1
M : Type u_2
inst✝² : CommSemiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
x✝ : M
⊢ ((ofDirectSum.comp toDirectSum).toLinearMap ∘ₗ ι R) x✝ = ((AlgHom.id R (TensorAlgebra R M)).toLinearMap ∘ₗ ι R) x✝

Proof state:
case w.h
R : Type u_1
M : Type u_2
inst✝² : CommSemiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
x✝ : M
⊢ ((ofDirectSum.comp toDirectSum).toLinearMap ∘ₗ ι R) x✝ = ((AlgHom.id R (TensorAlgebra R M)).toLinearMap ∘ₗ ι R) x✝

Tactic:
simp [DirectSum.lof_eq_of, tprod_apply]

Result:
no goals
-- Mathlib/CategoryTheory/Abelian/Projective/Dimension.lean
lemma Retract.hasProjectiveDimensionLT {X Y : C} (h : Retract X Y) (n : ℕ)
    [HasProjectiveDimensionLT Y n] :
    HasProjectiveDimensionLT X n

Proof state:
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : Abelian C
X Y : C
h : Retract X Y
n : ℕ
inst✝ : HasProjectiveDimensionLT Y n
this : HasExt C := HasExt.standard C
i : ℕ
hi : n ≤ i
T : C
x : Ext X T i
⊢ x = 0

Tactic:
rw [← x.mk₀_id_comp, ← h.retract, ← Ext.mk₀_comp_mk₀,
  Ext.comp_assoc_of_second_deg_zero,
  ((Ext.mk₀ h.r).comp x (zero_add i)).eq_zero_of_hasProjectiveDimensionLT n hi,
  Ext.comp_zero]

Result:
no goals

Proof state:
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : Abelian C
X Y : C
h : Retract X Y
n : ℕ
inst✝ : HasProjectiveDimensionLT Y n
⊢ HasProjectiveDimensionLT X n

Tactic:
letI := HasExt.standard C

Result:
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : Abelian C
X Y : C
h : Retract X Y
n : ℕ
inst✝ : HasProjectiveDimensionLT Y n
this : HasExt C := HasExt.standard C
⊢ HasProjectiveDimensionLT X n

Proof state:
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : Abelian C
X Y : C
h : Retract X Y
n : ℕ
inst✝ : HasProjectiveDimensionLT Y n
this : HasExt C := HasExt.standard C
⊢ HasProjectiveDimensionLT X n

Tactic:
rw [hasProjectiveDimensionLT_iff]

Result:
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : Abelian C
X Y : C
h : Retract X Y
n : ℕ
inst✝ : HasProjectiveDimensionLT Y n
this : HasExt C := HasExt.standard C
⊢ ∀ (i : ℕ), n ≤ i → ∀ ⦃Y : C⦄ (e : Ext X Y i), e = 0

Proof state:
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : Abelian C
X Y : C
h : Retract X Y
n : ℕ
inst✝ : HasProjectiveDimensionLT Y n
this : HasExt C := HasExt.standard C
⊢ ∀ (i : ℕ), n ≤ i → ∀ ⦃Y : C⦄ (e : Ext X Y i), e = 0

Tactic:
intro i hi T x

Result:
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : Abelian C
X Y : C
h : Retract X Y
n : ℕ
inst✝ : HasProjectiveDimensionLT Y n
this : HasExt C := HasExt.standard C
i : ℕ
hi : n ≤ i
T : C
x : Ext X T i
⊢ x = 0
-- Mathlib/Data/List/Sym.lean
theorem right_mem_of_mk_mem_sym2 {xs : List α} {a b : α}
    (h : s(a, b) ∈ xs.sym2) : b ∈ xs

Proof state:
α : Type u_1
xs : List α
a b : α
h : s(b, a) ∈ xs.sym2
⊢ b ∈ xs

Tactic:
exact left_mem_of_mk_mem_sym2 h

Result:
no goals

Proof state:
α : Type u_1
xs : List α
a b : α
h : s(a, b) ∈ xs.sym2
⊢ b ∈ xs

Tactic:
rw [Sym2.eq_swap] at h

Result:
α : Type u_1
xs : List α
a b : α
h : s(b, a) ∈ xs.sym2
⊢ b ∈ xs