harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/Data/Nat/MaxPowDiv.lean
theorem go_succ {k p n : ℕ} : go (k+1) p n = go k p n + 1

Proof state:
k✝ p✝ n✝ : ℕ
h : 1 < p✝ ∧ 0 < n✝ ∧ n✝ % p✝ = 0
ih : go (k✝ + 1 + 1) p✝ (n✝ / p✝) = go (k✝ + 1) p✝ (n✝ / p✝) + 1
⊢ go (k✝ + 1) p✝ n✝ = go k✝ p✝ n✝ + 1

Tactic:
unfold go

Result:
k✝ p✝ n✝ : ℕ
h : 1 < p✝ ∧ 0 < n✝ ∧ n✝ % p✝ = 0
ih : go (k✝ + 1 + 1) p✝ (n✝ / p✝) = go (k✝ + 1) p✝ (n✝ / p✝) + 1
⊢ (if 1 < p✝ ∧ 0 < n✝ ∧ n✝ % p✝ = 0 then go (k✝ + 1 + 1) p✝ (n✝ / p✝) else k✝ + 1) =
    (if 1 < p✝ ∧ 0 < n✝ ∧ n✝ % p✝ = 0 then go (k✝ + 1) p✝ (n✝ / p✝) else k✝) + 1

Proof state:
k✝ p✝ n✝ : ℕ
h : ¬(1 < p✝ ∧ 0 < n✝ ∧ n✝ % p✝ = 0)
⊢ (if 1 < p✝ ∧ 0 < n✝ ∧ n✝ % p✝ = 0 then go (k✝ + 1 + 1) p✝ (n✝ / p✝) else k✝ + 1) =
    (if 1 < p✝ ∧ 0 < n✝ ∧ n✝ % p✝ = 0 then go (k✝ + 1) p✝ (n✝ / p✝) else k✝) + 1

Tactic:
simp only [if_neg h]

Result:
no goals

Proof state:
case case2
k✝ p✝ n✝ : ℕ
h✝ : ¬(1 < p✝ ∧ 0 < n✝ ∧ n✝ % p✝ = 0)
⊢ go (k✝ + 1) p✝ n✝ = go k✝ p✝ n✝ + 1

Tactic:
case case2 h =>
  unfold go
  simp only [if_neg h]

Result:
no goals

Proof state:
case case1
k✝ p✝ n✝ : ℕ
h✝ : 1 < p✝ ∧ 0 < n✝ ∧ n✝ % p✝ = 0
ih1✝ : go (k✝ + 1 + 1) p✝ (n✝ / p✝) = go (k✝ + 1) p✝ (n✝ / p✝) + 1
⊢ go (k✝ + 1) p✝ n✝ = go k✝ p✝ n✝ + 1

case case2
k✝ p✝ n✝ : ℕ
h✝ : ¬(1 < p✝ ∧ 0 < n✝ ∧ n✝ % p✝ = 0)
⊢ go (k✝ + 1) p✝ n✝ = go k✝ p✝ n✝ + 1

Tactic:
case case1 h ih =>
  unfold go
  simp only [if_pos h]
  exact ih

Result:
case case2
k✝ p✝ n✝ : ℕ
h✝ : ¬(1 < p✝ ∧ 0 < n✝ ∧ n✝ % p✝ = 0)
⊢ go (k✝ + 1) p✝ n✝ = go k✝ p✝ n✝ + 1

Proof state:
k✝ p✝ n✝ : ℕ
h : 1 < p✝ ∧ 0 < n✝ ∧ n✝ % p✝ = 0
ih : go (k✝ + 1 + 1) p✝ (n✝ / p✝) = go (k✝ + 1) p✝ (n✝ / p✝) + 1
⊢ (if 1 < p✝ ∧ 0 < n✝ ∧ n✝ % p✝ = 0 then go (k✝ + 1 + 1) p✝ (n✝ / p✝) else k✝ + 1) =
    (if 1 < p✝ ∧ 0 < n✝ ∧ n✝ % p✝ = 0 then go (k✝ + 1) p✝ (n✝ / p✝) else k✝) + 1

Tactic:
simp only [if_pos h]

Result:
k✝ p✝ n✝ : ℕ
h : 1 < p✝ ∧ 0 < n✝ ∧ n✝ % p✝ = 0
ih : go (k✝ + 1 + 1) p✝ (n✝ / p✝) = go (k✝ + 1) p✝ (n✝ / p✝) + 1
⊢ go (k✝ + 1 + 1) p✝ (n✝ / p✝) = go (k✝ + 1) p✝ (n✝ / p✝) + 1

Proof state:
k p n : ℕ
⊢ go (k + 1) p n = go k p n + 1

Tactic:
induction k, p, n using go.induct

Result:
case case1
k✝ p✝ n✝ : ℕ
h✝ : 1 < p✝ ∧ 0 < n✝ ∧ n✝ % p✝ = 0
ih1✝ : go (k✝ + 1 + 1) p✝ (n✝ / p✝) = go (k✝ + 1) p✝ (n✝ / p✝) + 1
⊢ go (k✝ + 1) p✝ n✝ = go k✝ p✝ n✝ + 1

case case2
k✝ p✝ n✝ : ℕ
h✝ : ¬(1 < p✝ ∧ 0 < n✝ ∧ n✝ % p✝ = 0)
⊢ go (k✝ + 1) p✝ n✝ = go k✝ p✝ n✝ + 1

Proof state:
k✝ p✝ n✝ : ℕ
h : 1 < p✝ ∧ 0 < n✝ ∧ n✝ % p✝ = 0
ih : go (k✝ + 1 + 1) p✝ (n✝ / p✝) = go (k✝ + 1) p✝ (n✝ / p✝) + 1
⊢ go (k✝ + 1 + 1) p✝ (n✝ / p✝) = go (k✝ + 1) p✝ (n✝ / p✝) + 1

Tactic:
exact ih

Result:
no goals

Proof state:
k✝ p✝ n✝ : ℕ
h : ¬(1 < p✝ ∧ 0 < n✝ ∧ n✝ % p✝ = 0)
⊢ go (k✝ + 1) p✝ n✝ = go k✝ p✝ n✝ + 1

Tactic:
unfold go

Result:
k✝ p✝ n✝ : ℕ
h : ¬(1 < p✝ ∧ 0 < n✝ ∧ n✝ % p✝ = 0)
⊢ (if 1 < p✝ ∧ 0 < n✝ ∧ n✝ % p✝ = 0 then go (k✝ + 1 + 1) p✝ (n✝ / p✝) else k✝ + 1) =
    (if 1 < p✝ ∧ 0 < n✝ ∧ n✝ % p✝ = 0 then go (k✝ + 1) p✝ (n✝ / p✝) else k✝) + 1
-- Mathlib/LinearAlgebra/BilinearForm/Properties.lean
theorem isAdjointPair_unique_of_nondegenerate (B : BilinForm R₁ M₁) (b : B.Nondegenerate)
    (φ ψ₁ ψ₂ : M₁ →ₗ[R₁] M₁) (hψ₁ : IsAdjointPair B B ψ₁ φ) (hψ₂ : IsAdjointPair B B ψ₂ φ) :
    ψ₁ = ψ₂ :=
  B.compLeft_injective b <| ext fun v w => by rw [compLeft_apply, compLeft_apply, hψ₁, hψ₂]

Proof state:
R₁ : Type u_3
M₁ : Type u_4
inst✝² : CommRing R₁
inst✝¹ : AddCommGroup M₁
inst✝ : Module R₁ M₁
B : BilinForm R₁ M₁
b : B.Nondegenerate
φ ψ₁ ψ₂ : M₁ →ₗ[R₁] M₁
hψ₁ : IsAdjointPair B B ⇑ψ₁ ⇑φ
hψ₂ : IsAdjointPair B B ⇑ψ₂ ⇑φ
v w : M₁
⊢ ((B.compLeft ψ₁) v) w = ((B.compLeft ψ₂) v) w

Tactic:
rw [compLeft_apply, compLeft_apply, hψ₁, hψ₂]

Result:
no goals
-- Mathlib/Data/List/OfFn.lean
theorem ofFn_mul {m n} (f : Fin (m * n) → α) :
    List.ofFn f = List.flatten (List.ofFn fun i : Fin m => List.ofFn fun j : Fin n => f ⟨i * n + j,
    calc
      ↑i * n + j < (i + 1) * n :=
        (Nat.add_lt_add_left j.prop _).trans_eq (by rw [Nat.add_mul, Nat.one_mul])
      _ ≤ _ := Nat.mul_le_mul_right _ i.prop⟩)

Proof state:
case succ
α : Type u
n m : ℕ
IH : ∀ (f : Fin (m * n) → α), ofFn f = (ofFn fun i => ofFn fun j => f ⟨↑i * n + ↑j, ⋯⟩).flatten
f : Fin ((m + 1) * n) → α
⊢ ofFn f = (ofFn fun i => ofFn fun j => f ⟨↑i * n + ↑j, ⋯⟩).flatten

Tactic:
simp_rw [ofFn_succ', succ_mul]

Result:
case succ
α : Type u
n m : ℕ
IH : ∀ (f : Fin (m * n) → α), ofFn f = (ofFn fun i => ofFn fun j => f ⟨↑i * n + ↑j, ⋯⟩).flatten
f : Fin ((m + 1) * n) → α
⊢ (ofFn fun i => f (Fin.cast ⋯ i)) =
    ((ofFn fun i => ofFn fun j => f ⟨↑i.castSucc * n + ↑j, ⋯⟩).concat
        (ofFn fun j => f ⟨↑(Fin.last m) * n + ↑j, ⋯⟩)).flatten

Proof state:
case succ
α : Type u
n m : ℕ
IH : ∀ (f : Fin (m * n) → α), ofFn f = (ofFn fun i => ofFn fun j => f ⟨↑i * n + ↑j, ⋯⟩).flatten
f : Fin ((m + 1) * n) → α
⊢ (ofFn fun i => f (Fin.cast ⋯ i)) =
    ((ofFn fun i => ofFn fun j => f ⟨↑i.castSucc * n + ↑j, ⋯⟩).concat
        (ofFn fun j => f ⟨↑(Fin.last m) * n + ↑j, ⋯⟩)).flatten

Tactic:
simp [flatten_concat, ofFn_add, IH]

Result:
case succ
α : Type u
n m : ℕ
IH : ∀ (f : Fin (m * n) → α), ofFn f = (ofFn fun i => ofFn fun j => f ⟨↑i * n + ↑j, ⋯⟩).flatten
f : Fin ((m + 1) * n) → α
⊢ (ofFn fun j => f (Fin.cast ⋯ (Fin.natAdd (m * n) j))) = ofFn fun j => f ⟨m * n + ↑j, ⋯⟩

Proof state:
case zero
α : Type u
n : ℕ
f : Fin (0 * n) → α
⊢ ofFn f = (ofFn fun i => ofFn fun j => f ⟨↑i * n + ↑j, ⋯⟩).flatten

Tactic:
simp [ofFn_zero, Nat.zero_mul, ofFn_zero, flatten]

Result:
no goals

Proof state:
case succ
α : Type u
n m : ℕ
IH : ∀ (f : Fin (m * n) → α), ofFn f = (ofFn fun i => ofFn fun j => f ⟨↑i * n + ↑j, ⋯⟩).flatten
f : Fin ((m + 1) * n) → α
⊢ (ofFn fun j => f (Fin.cast ⋯ (Fin.natAdd (m * n) j))) = ofFn fun j => f ⟨m * n + ↑j, ⋯⟩

Tactic:
rfl

Result:
no goals

Proof state:
α : Type u
m n : ℕ
f : Fin (m * n) → α
i : Fin m
j : Fin n
⊢ ↑i * n + n = (↑i + 1) * n

Tactic:
rw [Nat.add_mul, Nat.one_mul]

Result:
no goals

Proof state:
α : Type u
m n : ℕ
f : Fin (m * n) → α
⊢ ofFn f = (ofFn fun i => ofFn fun j => f ⟨↑i * n + ↑j, ⋯⟩).flatten

Tactic:
induction' m with m IH

Result:
case zero
α : Type u
n : ℕ
f : Fin (0 * n) → α
⊢ ofFn f = (ofFn fun i => ofFn fun j => f ⟨↑i * n + ↑j, ⋯⟩).flatten

case succ
α : Type u
n m : ℕ
IH : ∀ (f : Fin (m * n) → α), ofFn f = (ofFn fun i => ofFn fun j => f ⟨↑i * n + ↑j, ⋯⟩).flatten
f : Fin ((m + 1) * n) → α
⊢ ofFn f = (ofFn fun i => ofFn fun j => f ⟨↑i * n + ↑j, ⋯⟩).flatten
-- Mathlib/Data/Multiset/Pi.lean
theorem cons_swap {a a' : α} {b : δ a} {b' : δ a'} {m : Multiset α} {f : ∀ a ∈ m, δ a}
    (h : a ≠ a') : HEq (Pi.cons (a' ::ₘ m) a b (Pi.cons m a' b' f))
      (Pi.cons (a ::ₘ m) a' b' (Pi.cons m a b f))

Proof state:
α : Type u_1
inst✝ : DecidableEq α
δ : α → Sort u_2
a a' : α
b : δ a
b' : δ a'
m : Multiset α
f : (a : α) → a ∈ m → δ a
h : a ≠ a'
a'' : α
⊢ (a'' ∈ a ::ₘ a' ::ₘ m) = (a'' ∈ a' ::ₘ a ::ₘ m)

Tactic:
rw [Multiset.cons_swap]

Result:
no goals
-- Mathlib/Data/Multiset/Fold.lean
theorem fold_add (b₁ b₂ : α) (s₁ s₂ : Multiset α) :
    (s₁ + s₂).fold op (b₁ * b₂) = s₁.fold op b₁ * s₂.fold op b₂ :=
  Multiset.induction_on s₂
    (by rw [Multiset.add_zero, fold_zero, ← fold_cons'_right, ← fold_cons_right op])
    (fun a b h => by rw [fold_cons_left, add_cons, fold_cons_left, h, ← ha.assoc, hc.comm a,
      ha.assoc])

Proof state:
α : Type u_1
op : α → α → α
hc : Std.Commutative op
ha : Std.Associative op
b₁ b₂ : α
s₁ s₂ : Multiset α
⊢ fold op (op b₁ b₂) (s₁ + 0) = op (fold op b₁ s₁) (fold op b₂ 0)

Tactic:
rw [Multiset.add_zero, fold_zero, ← fold_cons'_right, ← fold_cons_right op]

Result:
no goals

Proof state:
α : Type u_1
op : α → α → α
hc : Std.Commutative op
ha : Std.Associative op
b₁ b₂ : α
s₁ s₂ : Multiset α
a : α
b : Multiset α
h : fold op (op b₁ b₂) (s₁ + b) = op (fold op b₁ s₁) (fold op b₂ b)
⊢ fold op (op b₁ b₂) (s₁ + a ::ₘ b) = op (fold op b₁ s₁) (fold op b₂ (a ::ₘ b))

Tactic:
rw [fold_cons_left, add_cons, fold_cons_left, h, ← ha.assoc, hc.comm a,
ha.assoc]

Result:
no goals
-- Mathlib/Algebra/Homology/HomotopyCategory/HomComplex.lean
@[reassoc]
lemma v_comp_XIsoOfEq_hom
    (γ : Cochain F G n) (p q q' : ℤ) (hpq : p + n = q) (hq' : q = q') :
    γ.v p q hpq ≫ (HomologicalComplex.XIsoOfEq G hq').hom = γ.v p q' (by rw [← hq', hpq])

Proof state:
C : Type u
inst✝³ : Category.{v, u} C
inst✝² : Preadditive C
R : Type u_1
inst✝¹ : Ring R
inst✝ : Linear R C
F G K L : CochainComplex C ℤ
n m : ℤ
γ : Cochain F G n
p q q' : ℤ
hpq : p + n = q
hq' : q = q'
⊢ p + n = q'

Tactic:
rw [← hq', hpq]

Result:
no goals

Proof state:
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Preadditive C
F G : CochainComplex C ℤ
n : ℤ
γ : Cochain F G n
p q : ℤ
hpq : p + n = q
⊢ γ.v p q hpq ≫ (HomologicalComplex.XIsoOfEq G ⋯).hom = γ.v p q ⋯

Tactic:
simp only [HomologicalComplex.XIsoOfEq, eqToIso_refl, Iso.refl_hom, comp_id]

Result:
no goals

Proof state:
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Preadditive C
F G : CochainComplex C ℤ
n : ℤ
γ : Cochain F G n
p q q' : ℤ
hpq : p + n = q
hq' : q = q'
⊢ γ.v p q hpq ≫ (HomologicalComplex.XIsoOfEq G hq').hom = γ.v p q' ⋯

Tactic:
subst hq'

Result:
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Preadditive C
F G : CochainComplex C ℤ
n : ℤ
γ : Cochain F G n
p q : ℤ
hpq : p + n = q
⊢ γ.v p q hpq ≫ (HomologicalComplex.XIsoOfEq G ⋯).hom = γ.v p q ⋯
-- Mathlib/MeasureTheory/Integral/Bochner.lean
theorem integral_trim (hm : m ≤ m0) {f : β → G} (hf : StronglyMeasurable[m] f) :
    ∫ x, f x ∂μ = ∫ x, f x ∂μ.trim hm

Proof state:
case pos
G : Type u_5
inst✝¹ : NormedAddCommGroup G
inst✝ : NormedSpace ℝ G
β : Type u_6
m m0 : MeasurableSpace β
μ : Measure β
hm : m ≤ m0
f : β → G
hf : StronglyMeasurable f
hG : CompleteSpace G
this✝¹ : MeasurableSpace G := borel G
this✝ : BorelSpace G
hf_int : Integrable f μ
this : SeparableSpace ↑(range f ∪ {0})
f_seq : ℕ → β →ₛ G := SimpleFunc.approxOn f ⋯ (range f ∪ {0}) 0 ⋯
hf_seq_meas : ∀ (n : ℕ), StronglyMeasurable ⇑(f_seq n)
hf_seq_int : ∀ (n : ℕ), Integrable (⇑(f_seq n)) μ
hf_seq_int_m : ∀ (n : ℕ), Integrable (⇑(f_seq n)) (μ.trim hm)
hf_seq_eq : ∀ (n : ℕ), ∫ (x : β), (f_seq n) x ∂μ = ∫ (x : β), (f_seq n) x ∂μ.trim hm
h_lim_1 : Tendsto (fun n => ∫ (x : β), (f_seq n) x ∂μ) atTop (𝓝 (∫ (x : β), f x ∂μ))
⊢ ∫ (x : β), f x ∂μ = ∫ (x : β), f x ∂μ.trim hm

Tactic:
have h_lim_2 : atTop.Tendsto (fun n => ∫ x, f_seq n x ∂μ) (𝓝 (∫ x, f x ∂μ.trim hm)) := by
  simp_rw [hf_seq_eq]
  refine @tendsto_integral_of_L1 β G _ _ m (μ.trim hm) _ f (hf_int.trim hm hf) _ _
    (Eventually.of_forall hf_seq_int_m) ?_
  exact @SimpleFunc.tendsto_approxOn_range_L1_enorm β G m _ _ _ f _ _ hf.measurable
    (hf_int.trim hm hf)

Result:
case pos
G : Type u_5
inst✝¹ : NormedAddCommGroup G
inst✝ : NormedSpace ℝ G
β : Type u_6
m m0 : MeasurableSpace β
μ : Measure β
hm : m ≤ m0
f : β → G
hf : StronglyMeasurable f
hG : CompleteSpace G
this✝¹ : MeasurableSpace G := borel G
this✝ : BorelSpace G
hf_int : Integrable f μ
this : SeparableSpace ↑(range f ∪ {0})
f_seq : ℕ → β →ₛ G := SimpleFunc.approxOn f ⋯ (range f ∪ {0}) 0 ⋯
hf_seq_meas : ∀ (n : ℕ), StronglyMeasurable ⇑(f_seq n)
hf_seq_int : ∀ (n : ℕ), Integrable (⇑(f_seq n)) μ
hf_seq_int_m : ∀ (n : ℕ), Integrable (⇑(f_seq n)) (μ.trim hm)
hf_seq_eq : ∀ (n : ℕ), ∫ (x : β), (f_seq n) x ∂μ = ∫ (x : β), (f_seq n) x ∂μ.trim hm
h_lim_1 : Tendsto (fun n => ∫ (x : β), (f_seq n) x ∂μ) atTop (𝓝 (∫ (x : β), f x ∂μ))
h_lim_2 : Tendsto (fun n => ∫ (x : β), (f_seq n) x ∂μ) atTop (𝓝 (∫ (x : β), f x ∂μ.trim hm))
⊢ ∫ (x : β), f x ∂μ = ∫ (x : β), f x ∂μ.trim hm
-- Mathlib/Topology/Instances/ENNReal/Lemmas.lean
/-- If `xs : ι → ℝ≥0∞` is bounded, then we have `liminf (toReal ∘ xs) = toReal (liminf xs)`. -/
lemma liminf_toReal_eq {ι : Type*} {F : Filter ι} [NeBot F] {b : ℝ≥0∞} (b_ne_top : b ≠ ∞)
    {xs : ι → ℝ≥0∞} (le_b : ∀ᶠ i in F, xs i ≤ b) :
    F.liminf (fun i ↦ (xs i).toReal) = (F.liminf xs).toReal

Proof state:
ι : Type u_5
F : Filter ι
inst✝ : F.NeBot
b : ℝ≥0∞
b_ne_top : b ≠ ⊤
xs : ι → ℝ≥0∞
le_b : ∀ᶠ (i : ι) in F, xs i ≤ b
liminf_le : liminf xs F ≤ b
aux : ∀ᶠ (i : ι) in F, (xs i).toReal = b.truncateToReal (xs i)
⊢ liminf (fun i => (xs i).toReal) F = (liminf xs F).toReal

Tactic:
have aux' : (F.liminf xs).toReal = ENNReal.truncateToReal b (F.liminf xs) := by
  rw [truncateToReal_eq_toReal b_ne_top liminf_le]

Result:
ι : Type u_5
F : Filter ι
inst✝ : F.NeBot
b : ℝ≥0∞
b_ne_top : b ≠ ⊤
xs : ι → ℝ≥0∞
le_b : ∀ᶠ (i : ι) in F, xs i ≤ b
liminf_le : liminf xs F ≤ b
aux : ∀ᶠ (i : ι) in F, (xs i).toReal = b.truncateToReal (xs i)
aux' : (liminf xs F).toReal = b.truncateToReal (liminf xs F)
⊢ liminf (fun i => (xs i).toReal) F = (liminf xs F).toReal

Proof state:
ι : Type u_5
F : Filter ι
inst✝ : F.NeBot
b : ℝ≥0∞
b_ne_top : b ≠ ⊤
xs : ι → ℝ≥0∞
le_b : ∀ᶠ (i : ι) in F, xs i ≤ b
⊢ liminf (fun i => (xs i).toReal) F = (liminf xs F).toReal

Tactic:
have liminf_le : F.liminf xs ≤ b := by
  apply liminf_le_of_le ⟨0, by simp⟩
  intro y h
  obtain ⟨i, hi⟩ := (Eventually.and h le_b).exists
  exact hi.1.trans hi.2

Result:
ι : Type u_5
F : Filter ι
inst✝ : F.NeBot
b : ℝ≥0∞
b_ne_top : b ≠ ⊤
xs : ι → ℝ≥0∞
le_b : ∀ᶠ (i : ι) in F, xs i ≤ b
liminf_le : liminf xs F ≤ b
⊢ liminf (fun i => (xs i).toReal) F = (liminf xs F).toReal

Proof state:
case intro
ι : Type u_5
F : Filter ι
inst✝ : F.NeBot
b : ℝ≥0∞
b_ne_top : b ≠ ⊤
xs : ι → ℝ≥0∞
le_b : ∀ᶠ (i : ι) in F, xs i ≤ b
y : ℝ≥0∞
h : ∀ᶠ (n : ι) in F, y ≤ xs n
i : ι
hi : y ≤ xs i ∧ xs i ≤ b
⊢ y ≤ b

Tactic:
exact hi.1.trans hi.2

Result:
no goals
-- Mathlib/ModelTheory/Definability.lean
theorem definable_finset_inf {ι : Type*} {f : ι → Set (α → M)} (hf : ∀ i, A.Definable L (f i))
    (s : Finset ι) : A.Definable L (s.inf f)

Proof state:
M : Type w
A : Set M
L : Language
inst✝ : L.Structure M
α : Type u₁
ι : Type u_2
f : ι → Set (α → M)
hf : ∀ (i : ι), A.Definable L (f i)
s✝ : Finset ι
i : ι
s : Finset ι
x✝ : i ∉ s
h : A.Definable L (s.inf f)
⊢ A.Definable L (f i ⊓ s.inf f)

Tactic:
exact (hf i).inter h

Result:
no goals

Proof state:
M : Type w
A : Set M
L : Language
inst✝ : L.Structure M
α : Type u₁
ι : Type u_2
f : ι → Set (α → M)
hf : ∀ (i : ι), A.Definable L (f i)
s✝ : Finset ι
i : ι
s : Finset ι
x✝ : i ∉ s
h : A.Definable L (s.inf f)
⊢ A.Definable L ((insert i s).inf f)

Tactic:
rw [Finset.inf_insert]

Result:
M : Type w
A : Set M
L : Language
inst✝ : L.Structure M
α : Type u₁
ι : Type u_2
f : ι → Set (α → M)
hf : ∀ (i : ι), A.Definable L (f i)
s✝ : Finset ι
i : ι
s : Finset ι
x✝ : i ∉ s
h : A.Definable L (s.inf f)
⊢ A.Definable L (f i ⊓ s.inf f)

Proof state:
M : Type w
A : Set M
L : Language
inst✝ : L.Structure M
α : Type u₁
ι : Type u_2
f : ι → Set (α → M)
hf : ∀ (i : ι), A.Definable L (f i)
s : Finset ι
⊢ A.Definable L (s.inf f)

Tactic:
refine Finset.induction definable_univ (fun i s _ h => ?_) s

Result:
M : Type w
A : Set M
L : Language
inst✝ : L.Structure M
α : Type u₁
ι : Type u_2
f : ι → Set (α → M)
hf : ∀ (i : ι), A.Definable L (f i)
s✝ : Finset ι
i : ι
s : Finset ι
x✝ : i ∉ s
h : A.Definable L (s.inf f)
⊢ A.Definable L ((insert i s).inf f)

Proof state:
M : Type w
A : Set M
L : Language
inst✝ : L.Structure M
α : Type u₁
ι : Type u_2
f : ι → Set (α → M)
hf : ∀ (i : ι), A.Definable L (f i)
s : Finset ι
⊢ A.Definable L (s.inf f)

Tactic:
classical
  refine Finset.induction definable_univ (fun i s _ h => ?_) s
  rw [Finset.inf_insert]
  exact (hf i).inter h

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/BitVec/Bitblast.lean
theorem msb_add {w : Nat} {x y: BitVec w} :
    (x + y).msb =
      Bool.xor x.msb (Bool.xor y.msb (carry (w - 1) x y false))

Proof state:
case neg.i_lt
w : Nat
x y : BitVec w
h : ¬w ≤ 0
⊢ w - 1 - 0 < w

Tactic:
omega

Result:
no goals

Proof state:
case neg
w : Nat
x y : BitVec w
h : ¬w ≤ 0
⊢ (decide (0 < w) && (x.getLsbD (w - 1 - 0) ^^ (y.getLsbD (w - 1 - 0) ^^ carry (w - 1 - 0) x y false))) =
    (decide (0 < w) && x.getLsbD (w - 1 - 0) ^^ (decide (0 < w) && y.getLsbD (w - 1 - 0) ^^ carry (w - 1) x y false))

case neg.i_lt
w : Nat
x y : BitVec w
h : ¬w ≤ 0
⊢ w - 1 - 0 < w

Tactic:
simp [show w > 0 by omega]

Result:
case neg.i_lt
w : Nat
x y : BitVec w
h : ¬w ≤ 0
⊢ w - 1 - 0 < w

Proof state:
w : Nat
x y : BitVec w
h : w ≤ 0
⊢ w = 0

Tactic:
omega

Result:
no goals

Proof state:
w : Nat
x y : BitVec w
h : ¬w ≤ 0
⊢ w > 0

Tactic:
omega

Result:
no goals

Proof state:
case neg
w : Nat
x y : BitVec w
h : ¬w ≤ 0
⊢ (decide (0 < w) && (x + y).getLsbD (w - 1 - 0)) =
    (decide (0 < w) && x.getLsbD (w - 1 - 0) ^^ (decide (0 < w) && y.getLsbD (w - 1 - 0) ^^ carry (w - 1) x y false))

Tactic:
rw [getLsbD_add (x := x)]

Result:
case neg
w : Nat
x y : BitVec w
h : ¬w ≤ 0
⊢ (decide (0 < w) && (x.getLsbD (w - 1 - 0) ^^ (y.getLsbD (w - 1 - 0) ^^ carry (w - 1 - 0) x y false))) =
    (decide (0 < w) && x.getLsbD (w - 1 - 0) ^^ (decide (0 < w) && y.getLsbD (w - 1 - 0) ^^ carry (w - 1) x y false))

case neg.i_lt
w : Nat
x y : BitVec w
h : ¬w ≤ 0
⊢ w - 1 - 0 < w

Proof state:
w : Nat
x y : BitVec w
⊢ (decide (0 < w) && (x + y).getLsbD (w - 1 - 0)) =
    (decide (0 < w) && x.getLsbD (w - 1 - 0) ^^ (decide (0 < w) && y.getLsbD (w - 1 - 0) ^^ carry (w - 1) x y false))

Tactic:
by_cases h : w ≤ 0

Result:
case pos
w : Nat
x y : BitVec w
h : w ≤ 0
⊢ (decide (0 < w) && (x + y).getLsbD (w - 1 - 0)) =
    (decide (0 < w) && x.getLsbD (w - 1 - 0) ^^ (decide (0 < w) && y.getLsbD (w - 1 - 0) ^^ carry (w - 1) x y false))

case neg
w : Nat
x y : BitVec w
h : ¬w ≤ 0
⊢ (decide (0 < w) && (x + y).getLsbD (w - 1 - 0)) =
    (decide (0 < w) && x.getLsbD (w - 1 - 0) ^^ (decide (0 < w) && y.getLsbD (w - 1 - 0) ^^ carry (w - 1) x y false))

Proof state:
w : Nat
x y : BitVec w
⊢ (x + y).msb = (x.msb ^^ (y.msb ^^ carry (w - 1) x y false))

Tactic:
simp only [BitVec.msb, BitVec.getMsbD]

Result:
w : Nat
x y : BitVec w
⊢ (decide (0 < w) && (x + y).getLsbD (w - 1 - 0)) =
    (decide (0 < w) && x.getLsbD (w - 1 - 0) ^^ (decide (0 < w) && y.getLsbD (w - 1 - 0) ^^ carry (w - 1) x y false))

Proof state:
case pos
w : Nat
x y : BitVec w
h : w ≤ 0
⊢ (decide (0 < w) && (x + y).getLsbD (w - 1 - 0)) =
    (decide (0 < w) && x.getLsbD (w - 1 - 0) ^^ (decide (0 < w) && y.getLsbD (w - 1 - 0) ^^ carry (w - 1) x y false))

Tactic:
simp [h, show w = 0 by omega]

Result:
no goals
-- Mathlib/Topology/DerivedSet.lean
lemma derivedSet_union (A B : Set X) : derivedSet (A ∪ B) = derivedSet A ∪ derivedSet B

Proof state:
X : Type u_1
inst✝ : TopologicalSpace X
A B : Set X
⊢ derivedSet (A ∪ B) = derivedSet A ∪ derivedSet B

Tactic:
ext x

Result:
case h
X : Type u_1
inst✝ : TopologicalSpace X
A B : Set X
x : X
⊢ x ∈ derivedSet (A ∪ B) ↔ x ∈ derivedSet A ∪ derivedSet B

Proof state:
case h
X : Type u_1
inst✝ : TopologicalSpace X
A B : Set X
x : X
⊢ x ∈ derivedSet (A ∪ B) ↔ x ∈ derivedSet A ∪ derivedSet B

Tactic:
simp [derivedSet, ← sup_principal, accPt_sup]

Result:
no goals
-- Mathlib/Probability/Kernel/Composition/MeasureComp.lean
lemma map_comp (μ : Measure α) (κ : Kernel α β) {f : β → γ} (hf : Measurable f) :
    (κ ∘ₘ μ).map f = (κ.map f) ∘ₘ μ

Proof state:
case h
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
μ : Measure α
κ : Kernel α β
f : β → γ
hf : Measurable f
s : Set γ
hs : MeasurableSet s
⊢ ∫⁻ (a : α), (κ a) (f ⁻¹' s) ∂μ = ∫⁻ (a : α), ((κ.map f) a) s ∂μ

Tactic:
simp_rw [Kernel.map_apply' _ hf _ hs]

Result:
no goals

Proof state:
case h
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
μ : Measure α
κ : Kernel α β
f : β → γ
hf : Measurable f
s : Set γ
hs : MeasurableSet s
⊢ (map f (⇑κ ∘ₘ μ)) s = (⇑(κ.map f) ∘ₘ μ) s

Tactic:
rw [Measure.map_apply hf hs, Measure.bind_apply (hf hs) κ.measurable,
  Measure.bind_apply hs (Kernel.measurable _)]

Result:
case h
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
μ : Measure α
κ : Kernel α β
f : β → γ
hf : Measurable f
s : Set γ
hs : MeasurableSet s
⊢ ∫⁻ (a : α), (κ a) (f ⁻¹' s) ∂μ = ∫⁻ (a : α), ((κ.map f) a) s ∂μ

Proof state:
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
μ : Measure α
κ : Kernel α β
f : β → γ
hf : Measurable f
⊢ map f (⇑κ ∘ₘ μ) = ⇑(κ.map f) ∘ₘ μ

Tactic:
ext s hs

Result:
case h
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
μ : Measure α
κ : Kernel α β
f : β → γ
hf : Measurable f
s : Set γ
hs : MeasurableSet s
⊢ (map f (⇑κ ∘ₘ μ)) s = (⇑(κ.map f) ∘ₘ μ) s
-- Mathlib/Topology/Instances/ENNReal/Lemmas.lean
theorem le_of_forall_lt_one_mul_le {x y : ℝ≥0∞} (h : ∀ a < 1, a * x ≤ y) : x ≤ y

Proof state:
x y : ℝ≥0∞
h : ∀ a < 1, a * x ≤ y
this : Tendsto (fun x_1 => x_1 * x) (𝓝[<] 1) (𝓝 x)
⊢ x ≤ y

Tactic:
exact le_of_tendsto this (eventually_nhdsWithin_iff.2 <| Eventually.of_forall h)

Result:
no goals

Proof state:
x y : ℝ≥0∞
h : ∀ a < 1, a * x ≤ y
this : Tendsto (fun x_1 => x_1 * x) (𝓝[<] 1) (𝓝 (1 * x))
⊢ x ≤ y

Tactic:
rw [one_mul] at this

Result:
x y : ℝ≥0∞
h : ∀ a < 1, a * x ≤ y
this : Tendsto (fun x_1 => x_1 * x) (𝓝[<] 1) (𝓝 x)
⊢ x ≤ y
-- Mathlib/Geometry/Euclidean/Angle/Oriented/Basic.lean
theorem oangle_add_cyc3_neg_left {x y z : V} (hx : x ≠ 0) (hy : y ≠ 0) (hz : z ≠ 0) :
    o.oangle (-x) y + o.oangle (-y) z + o.oangle (-z) x = π

Proof state:
V : Type u_1
inst✝² : NormedAddCommGroup V
inst✝¹ : InnerProductSpace ℝ V
inst✝ : Fact (finrank ℝ V = 2)
o : Orientation ℝ V (Fin 2)
x y z : V
hx : x ≠ 0
hy : y ≠ 0
hz : z ≠ 0
⊢ o.oangle x y + ↑π + (o.oangle y z + ↑π) + (o.oangle z x + ↑π) =
    o.oangle x y + o.oangle y z + o.oangle z x + (↑π + ↑π + ↑π)

Tactic:
abel

Result:
no goals

Proof state:
V : Type u_1
inst✝² : NormedAddCommGroup V
inst✝¹ : InnerProductSpace ℝ V
inst✝ : Fact (finrank ℝ V = 2)
o : Orientation ℝ V (Fin 2)
x y z : V
hx : x ≠ 0
hy : y ≠ 0
hz : z ≠ 0
⊢ o.oangle (-x) y + o.oangle (-y) z + o.oangle (-z) x = ↑π

Tactic:
rw [o.oangle_neg_left hx hy, o.oangle_neg_left hy hz, o.oangle_neg_left hz hx,
  show o.oangle x y + π + (o.oangle y z + π) + (o.oangle z x + π) =
    o.oangle x y + o.oangle y z + o.oangle z x + (π + π + π : Real.Angle) by abel,
  o.oangle_add_cyc3 hx hy hz, Real.Angle.coe_pi_add_coe_pi, zero_add, zero_add]

Result:
no goals
-- Mathlib/Algebra/TrivSqZeroExt.lean
theorem inv_zero : (0 : tsze R M)⁻¹ = (0 : tsze R M)

Proof state:
R : Type u
M : Type v
inst✝³ : DivisionSemiring R
inst✝² : AddCommGroup M
inst✝¹ : Module Rᵐᵒᵖ M
inst✝ : Module R M
⊢ 0⁻¹ = 0

Tactic:
rw [← inl_zero, TrivSqZeroExt.inv_inl, inv_zero]

Result:
no goals
-- Mathlib/Data/Finset/Insert.lean
theorem cons_induction {α : Type*} {p : Finset α → Prop} (empty : p ∅)
    (cons : ∀ (a : α) (s : Finset α) (h : a ∉ s), p s → p (cons a s h)) : ∀ s, p s
  | ⟨s, nd⟩ => by
    induction s using Multiset.induction with
    | empty => exact empty
    | cons a s IH =>
      rw [mk_cons nd]
      exact cons a _ _ (IH _)

Proof state:
α : Type u_3
p : Finset α → Prop
empty : p ∅
cons : ∀ (a : α) (s : Finset α) (h : a ∉ s), p s → p (Finset.cons a s h)
s : Multiset α
nd : s.Nodup
⊢ p { val := s, nodup := nd }

Tactic:
induction s using Multiset.induction with
| empty => exact empty
| cons a s IH =>
  rw [mk_cons nd]
  exact cons a _ _ (IH _)

Result:
no goals

Proof state:
case empty
α : Type u_3
p : Finset α → Prop
empty : p ∅
cons : ∀ (a : α) (s : Finset α) (h : a ∉ s), p s → p (Finset.cons a s h)
nd : Nodup 0
⊢ p { val := 0, nodup := nd }

Tactic:
exact empty

Result:
no goals

Proof state:
case cons
α : Type u_3
p : Finset α → Prop
empty : p ∅
cons : ∀ (a : α) (s : Finset α) (h : a ∉ s), p s → p (Finset.cons a s h)
a : α
s : Multiset α
IH : ∀ (nd : s.Nodup), p { val := s, nodup := nd }
nd : (a ::ₘ s).Nodup
⊢ p (Finset.cons a { val := s, nodup := ⋯ } ⋯)

Tactic:
exact cons a _ _ (IH _)

Result:
no goals

Proof state:
case cons
α : Type u_3
p : Finset α → Prop
empty : p ∅
cons : ∀ (a : α) (s : Finset α) (h : a ∉ s), p s → p (Finset.cons a s h)
a : α
s : Multiset α
IH : ∀ (nd : s.Nodup), p { val := s, nodup := nd }
nd : (a ::ₘ s).Nodup
⊢ p { val := a ::ₘ s, nodup := nd }

Tactic:
rw [mk_cons nd]

Result:
case cons
α : Type u_3
p : Finset α → Prop
empty : p ∅
cons : ∀ (a : α) (s : Finset α) (h : a ∉ s), p s → p (Finset.cons a s h)
a : α
s : Multiset α
IH : ∀ (nd : s.Nodup), p { val := s, nodup := nd }
nd : (a ::ₘ s).Nodup
⊢ p (Finset.cons a { val := s, nodup := ⋯ } ⋯)