harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/MeasureTheory/Function/LpSpace/Basic.lean
theorem completeSpace_lp_of_cauchy_complete_eLpNorm [hp : Fact (1 ≤ p)]
    (H :
      ∀ (f : ℕ → α → E) (_ : ∀ n, MemLp (f n) p μ) (B : ℕ → ℝ≥0∞) (_ : ∑' i, B i < ∞)
        (_ : ∀ N n m : ℕ, N ≤ n → N ≤ m → eLpNorm (f n - f m) p μ < B N),
        ∃ (f_lim : α → E), MemLp f_lim p μ ∧
          atTop.Tendsto (fun n => eLpNorm (f n - f_lim) p μ) (𝓝 0)) :
    CompleteSpace (Lp E p μ)

Proof state:
case intro
α : Type u_1
E : Type u_4
m0 : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
inst✝ : NormedAddCommGroup E
hp : Fact (1 ≤ p)
H :
  ∀ (f : ℕ → α → E),
    (∀ (n : ℕ), MemLp (f n) p μ) →
      ∀ (B : ℕ → ℝ≥0∞),
        ∑' (i : ℕ), B i < ⊤ →
          (∀ (N n m : ℕ), N ≤ n → N ≤ m → eLpNorm (f n - f m) p μ < B N) →
            ∃ f_lim, MemLp f_lim p μ ∧ Tendsto (fun n => eLpNorm (f n - f_lim) p μ) atTop (𝓝 0)
B : ℕ → ℝ := fun n => (1 / 2) ^ n
hB_pos : ∀ (n : ℕ), 0 < B n
f : ℕ → ↥(Lp E p μ)
hf : ∀ (N n m : ℕ), N ≤ n → N ≤ m → dist (f n) (f m) < B N
M : ℝ
hB : HasSum B M
⊢ ∃ f_lim, MemLp f_lim p μ ∧ Tendsto (fun n => eLpNorm (↑↑(f n) - f_lim) p μ) atTop (𝓝 0)

Tactic:
let B1 n := ENNReal.ofReal (B n)

Result:
case intro
α : Type u_1
E : Type u_4
m0 : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
inst✝ : NormedAddCommGroup E
hp : Fact (1 ≤ p)
H :
  ∀ (f : ℕ → α → E),
    (∀ (n : ℕ), MemLp (f n) p μ) →
      ∀ (B : ℕ → ℝ≥0∞),
        ∑' (i : ℕ), B i < ⊤ →
          (∀ (N n m : ℕ), N ≤ n → N ≤ m → eLpNorm (f n - f m) p μ < B N) →
            ∃ f_lim, MemLp f_lim p μ ∧ Tendsto (fun n => eLpNorm (f n - f_lim) p μ) atTop (𝓝 0)
B : ℕ → ℝ := fun n => (1 / 2) ^ n
hB_pos : ∀ (n : ℕ), 0 < B n
f : ℕ → ↥(Lp E p μ)
hf : ∀ (N n m : ℕ), N ≤ n → N ≤ m → dist (f n) (f m) < B N
M : ℝ
hB : HasSum B M
B1 : ℕ → ℝ≥0∞ := fun n => ENNReal.ofReal (B n)
⊢ ∃ f_lim, MemLp f_lim p μ ∧ Tendsto (fun n => eLpNorm (↑↑(f n) - f_lim) p μ) atTop (𝓝 0)
-- Mathlib/LinearAlgebra/Reflection.lean
lemma eq_of_mapsTo_reflection_of_mem [NoZeroSMulDivisors ℤ M] {Φ : Set M} (hΦ : Φ.Finite)
    (hfx : f x = 2) (hgy : g y = 2) (hgx : g x = 2) (hfy : f y = 2)
    (hxfΦ : MapsTo (preReflection x f) Φ Φ)
    (hygΦ : MapsTo (preReflection y g) Φ Φ)
    (hyΦ : y ∈ Φ) :
    x = y

Proof state:
R : Type u_1
M : Type u_2
inst✝³ : CommRing R
inst✝² : AddCommGroup M
inst✝¹ : Module R M
x : M
f : Dual R M
y : M
g : Dual R M
inst✝ : NoZeroSMulDivisors ℤ M
Φ : Set M
hfx : f x = 2
hgy : g y = 2
hgx : g x = 2
hfy : f y = 2
hxfΦ : MapsTo (⇑(preReflection x f)) Φ Φ
hygΦ : MapsTo (⇑(preReflection y g)) Φ Φ
hyΦ : y ∈ Φ
hΦ : f y • x ≠ 2 • y
n : ℕ
⊢ (⇑(reflection hgy ≪≫ₗ reflection hfx))^[n] y ∈ (⇑(reflection hfx) ∘ ⇑(reflection hgy))^[n] '' Φ

Tactic:
exact mem_image_of_mem _ hyΦ

Result:
no goals

Proof state:
R : Type u_1
M : Type u_2
inst✝³ : CommRing R
inst✝² : AddCommGroup M
inst✝¹ : Module R M
x : M
f : Dual R M
y : M
g : Dual R M
inst✝ : NoZeroSMulDivisors ℤ M
Φ : Set M
hfx : f x = 2
hgy : g y = 2
hgx : g x = 2
hfy : f y = 2
hxfΦ : MapsTo (⇑(preReflection x f)) Φ Φ
hygΦ : MapsTo (⇑(preReflection y g)) Φ Φ
hyΦ : y ∈ Φ
hΦ : f y • x ≠ 2 • y
⊢ Φ.Infinite

Tactic:
apply ((infinite_range_reflection_reflection_iterate_iff hfx hgy
  (by rw [hfy, hgx]; norm_cast)).mpr hΦ).mono

Result:
R : Type u_1
M : Type u_2
inst✝³ : CommRing R
inst✝² : AddCommGroup M
inst✝¹ : Module R M
x : M
f : Dual R M
y : M
g : Dual R M
inst✝ : NoZeroSMulDivisors ℤ M
Φ : Set M
hfx : f x = 2
hgy : g y = 2
hgx : g x = 2
hfy : f y = 2
hxfΦ : MapsTo (⇑(preReflection x f)) Φ Φ
hygΦ : MapsTo (⇑(preReflection y g)) Φ Φ
hyΦ : y ∈ Φ
hΦ : f y • x ≠ 2 • y
⊢ (range fun n => (⇑(reflection hgy ≪≫ₗ reflection hfx))^[n] y) ⊆ Φ
-- Mathlib/CategoryTheory/SmallObject/Construction.lean
lemma functorMap_comm :
    functorObjLeft f πX ≫ functorMapTgt f τ =
      functorMapSrc f τ ≫ functorObjLeft f πY

Proof state:
case h.mk
C : Type u
inst✝² : Category.{v, u} C
I : Type w
A B : I → C
f : (i : I) → A i ⟶ B i
S T X Y : C
πX : X ⟶ S
πY : Y ⟶ T
τ : Arrow.mk πX ⟶ Arrow.mk πY
inst✝¹ : HasColimitsOfShape (Discrete (FunctorObjIndex f πX)) C
inst✝ : HasColimitsOfShape (Discrete (FunctorObjIndex f πY)) C
i : I
t : A i ⟶ X
b : B i ⟶ S
w : t ≫ πX = f i ≫ b
⊢ Sigma.ι (functorObjSrcFamily f πX) { i := i, t := t, b := b, w := w } ≫ functorObjLeft f πX ≫ functorMapTgt f τ =
    Sigma.ι (functorObjSrcFamily f πX) { i := i, t := t, b := b, w := w } ≫ functorMapSrc f τ ≫ functorObjLeft f πY

Tactic:
simp only [ι_colimMap_assoc, Discrete.natTrans_app, ι_colimMap,
  ι_functorMapTgt f τ i t b w _ rfl,
  ι_functorMapSrc_assoc f τ i t b w _ rfl]

Result:
no goals

Proof state:
C : Type u
inst✝² : Category.{v, u} C
I : Type w
A B : I → C
f : (i : I) → A i ⟶ B i
S T X Y : C
πX : X ⟶ S
πY : Y ⟶ T
τ : Arrow.mk πX ⟶ Arrow.mk πY
inst✝¹ : HasColimitsOfShape (Discrete (FunctorObjIndex f πX)) C
inst✝ : HasColimitsOfShape (Discrete (FunctorObjIndex f πY)) C
⊢ functorObjLeft f πX ≫ functorMapTgt f τ = functorMapSrc f τ ≫ functorObjLeft f πY

Tactic:
ext ⟨i, t, b, w⟩

Result:
case h.mk
C : Type u
inst✝² : Category.{v, u} C
I : Type w
A B : I → C
f : (i : I) → A i ⟶ B i
S T X Y : C
πX : X ⟶ S
πY : Y ⟶ T
τ : Arrow.mk πX ⟶ Arrow.mk πY
inst✝¹ : HasColimitsOfShape (Discrete (FunctorObjIndex f πX)) C
inst✝ : HasColimitsOfShape (Discrete (FunctorObjIndex f πY)) C
i : I
t : A i ⟶ X
b : B i ⟶ S
w : t ≫ πX = f i ≫ b
⊢ Sigma.ι (functorObjSrcFamily f πX) { i := i, t := t, b := b, w := w } ≫ functorObjLeft f πX ≫ functorMapTgt f τ =
    Sigma.ι (functorObjSrcFamily f πX) { i := i, t := t, b := b, w := w } ≫ functorMapSrc f τ ≫ functorObjLeft f πY
-- Mathlib/Data/Num/Lemmas.lean
theorem ofNat'_succ : ∀ {n}, ofNat' (n + 1) = ofNat' n + 1 :=
  @(Nat.binaryRec (by simp [zero_add]) fun b n ih => by
    cases b
    · erw [ofNat'_bit true n, ofNat'_bit]
      simp only [← bit1_of_bit1, ← bit0_of_bit0, cond]
    · rw [show n.bit true + 1 = (n + 1).bit false by simp [Nat.bit, mul_add],
        ofNat'_bit, ofNat'_bit, ih]
      simp only [cond, add_one, bit1_succ])

Proof state:
⊢ ofNat' (0 + 1) = ofNat' 0 + 1

Tactic:
simp [zero_add]

Result:
no goals

Proof state:
n : ℕ
ih : ofNat' (n + 1) = ofNat' n + 1
⊢ Nat.bit true n + 1 = Nat.bit false (n + 1)

Tactic:
simp [Nat.bit, mul_add]

Result:
no goals

Proof state:
b : Bool
n : ℕ
ih : ofNat' (n + 1) = ofNat' n + 1
⊢ ofNat' (Nat.bit b n + 1) = ofNat' (Nat.bit b n) + 1

Tactic:
cases b

Result:
case false
n : ℕ
ih : ofNat' (n + 1) = ofNat' n + 1
⊢ ofNat' (Nat.bit false n + 1) = ofNat' (Nat.bit false n) + 1

case true
n : ℕ
ih : ofNat' (n + 1) = ofNat' n + 1
⊢ ofNat' (Nat.bit true n + 1) = ofNat' (Nat.bit true n) + 1

Proof state:
case true
n : ℕ
ih : ofNat' (n + 1) = ofNat' n + 1
⊢ (bif false then Num.bit1 else Num.bit0) (ofNat' n + 1) = (bif true then Num.bit1 else Num.bit0) (ofNat' n) + 1

Tactic:
simp only [cond, add_one, bit1_succ]

Result:
no goals

Proof state:
case false
n : ℕ
ih : ofNat' (n + 1) = ofNat' n + 1
⊢ ofNat' (Nat.bit false n + 1) = ofNat' (Nat.bit false n) + 1

Tactic:
erw [ofNat'_bit true n, ofNat'_bit]

Result:
case false
n : ℕ
ih : ofNat' (n + 1) = ofNat' n + 1
⊢ (bif true then Num.bit1 else Num.bit0) (ofNat' n) = (bif false then Num.bit1 else Num.bit0) (ofNat' n) + 1

Proof state:
case false
n : ℕ
ih : ofNat' (n + 1) = ofNat' n + 1
⊢ (bif true then Num.bit1 else Num.bit0) (ofNat' n) = (bif false then Num.bit1 else Num.bit0) (ofNat' n) + 1

Tactic:
simp only [← bit1_of_bit1, ← bit0_of_bit0, cond]

Result:
no goals

Proof state:
case true
n : ℕ
ih : ofNat' (n + 1) = ofNat' n + 1
⊢ ofNat' (Nat.bit true n + 1) = ofNat' (Nat.bit true n) + 1

Tactic:
rw [show n.bit true + 1 = (n + 1).bit false by simp [Nat.bit, mul_add],
  ofNat'_bit, ofNat'_bit, ih]

Result:
case true
n : ℕ
ih : ofNat' (n + 1) = ofNat' n + 1
⊢ (bif false then Num.bit1 else Num.bit0) (ofNat' n + 1) = (bif true then Num.bit1 else Num.bit0) (ofNat' n) + 1
-- Mathlib/Algebra/Group/Basic.lean
@[to_additive] lemma zpow_mul_comm (a : G) (m n : ℤ) : a ^ m * a ^ n = a ^ n * a ^ m

Proof state:
G : Type u_3
inst✝ : Group G
a : G
m n : ℤ
⊢ a ^ m * a ^ n = a ^ n * a ^ m

Tactic:
rw [← zpow_add, Int.add_comm, zpow_add]

Result:
no goals
-- Mathlib/RingTheory/PowerSeries/WellKnown.lean
theorem one_sub_pow_add_mul_invOneSubPow_val_eq_one_sub_pow (e : ℕ) :
    (1 - X) ^ (d + e) * (invOneSubPow S e).val = (1 - X) ^ d

Proof state:
S : Type u_1
inst✝ : CommRing S
d e : ℕ
⊢ (1 - X) ^ (d + e) * ↑(invOneSubPow S e) = (1 - X) ^ d

Tactic:
simp [pow_add, mul_assoc, ← invOneSubPow_inv_eq_one_sub_pow S e]

Result:
no goals
-- Mathlib/MeasureTheory/Measure/FiniteMeasure.lean
theorem testAgainstNN_add (μ : FiniteMeasure Ω) (f₁ f₂ : Ω →ᵇ ℝ≥0) :
    μ.testAgainstNN (f₁ + f₂) = μ.testAgainstNN f₁ + μ.testAgainstNN f₂

Proof state:
Ω : Type u_1
inst✝² : MeasurableSpace Ω
inst✝¹ : TopologicalSpace Ω
inst✝ : OpensMeasurableSpace Ω
μ : FiniteMeasure Ω
f₁ f₂ : Ω →ᵇ ℝ≥0
⊢ μ.testAgainstNN (f₁ + f₂) = μ.testAgainstNN f₁ + μ.testAgainstNN f₂

Tactic:
simp only [← ENNReal.coe_inj, BoundedContinuousFunction.coe_add, ENNReal.coe_add, Pi.add_apply,
  testAgainstNN_coe_eq]

Result:
Ω : Type u_1
inst✝² : MeasurableSpace Ω
inst✝¹ : TopologicalSpace Ω
inst✝ : OpensMeasurableSpace Ω
μ : FiniteMeasure Ω
f₁ f₂ : Ω →ᵇ ℝ≥0
⊢ ∫⁻ (ω : Ω), ↑(f₁ ω) + ↑(f₂ ω) ∂↑μ = ∫⁻ (ω : Ω), ↑(f₁ ω) ∂↑μ + ∫⁻ (ω : Ω), ↑(f₂ ω) ∂↑μ

Proof state:
Ω : Type u_1
inst✝² : MeasurableSpace Ω
inst✝¹ : TopologicalSpace Ω
inst✝ : OpensMeasurableSpace Ω
μ : FiniteMeasure Ω
f₁ f₂ : Ω →ᵇ ℝ≥0
⊢ ∫⁻ (ω : Ω), ↑(f₁ ω) + ↑(f₂ ω) ∂↑μ = ∫⁻ (ω : Ω), ↑(f₁ ω) ∂↑μ + ∫⁻ (ω : Ω), ↑(f₂ ω) ∂↑μ

Tactic:
exact lintegral_add_left (BoundedContinuousFunction.measurable_coe_ennreal_comp _) _

Result:
no goals
-- Mathlib/RingTheory/PowerSeries/Derivative.lean
theorem derivativeFun_mul (f g : R⟦X⟧) :
    derivativeFun (f * g) = f • g.derivativeFun + g • f.derivativeFun

Proof state:
R : Type u_1
inst✝ : CommSemiring R
f g : R⟦X⟧
⊢ (f * g).derivativeFun = f • g.derivativeFun + g • f.derivativeFun

Tactic:
ext n

Result:
case h
R : Type u_1
inst✝ : CommSemiring R
f g : R⟦X⟧
n : ℕ
⊢ (coeff R n) (f * g).derivativeFun = (coeff R n) (f • g.derivativeFun + g • f.derivativeFun)

Proof state:
case h
R : Type u_1
inst✝ : CommSemiring R
f g : R⟦X⟧
n : ℕ
h₁ : n < n + 1
⊢ (coeff R n) (f * g).derivativeFun = (coeff R n) (f • g.derivativeFun + g • f.derivativeFun)

Tactic:
have h₂ : n < n + 1 + 1 := Nat.lt_add_right _ h₁

Result:
case h
R : Type u_1
inst✝ : CommSemiring R
f g : R⟦X⟧
n : ℕ
h₁ : n < n + 1
h₂ : n < n + 1 + 1
⊢ (coeff R n) (f * g).derivativeFun = (coeff R n) (f • g.derivativeFun + g • f.derivativeFun)

Proof state:
case h
R : Type u_1
inst✝ : CommSemiring R
f g : R⟦X⟧
n : ℕ
h₁ : n < n + 1
h₂ : n < n + 1 + 1
⊢ (coeff R n) (f * g).derivativeFun = (coeff R n) (f • g.derivativeFun + g • f.derivativeFun)

Tactic:
rw [coeff_derivativeFun, map_add, coeff_mul_eq_coeff_trunc_mul_trunc _ _ (lt_succ_self _),
  smul_eq_mul, smul_eq_mul, coeff_mul_eq_coeff_trunc_mul_trunc₂ g f.derivativeFun h₂ h₁,
  coeff_mul_eq_coeff_trunc_mul_trunc₂ f g.derivativeFun h₂ h₁, trunc_derivativeFun,
  trunc_derivativeFun, ← map_add, ← derivativeFun_coe_mul_coe, coeff_derivativeFun]

Result:
no goals

Proof state:
case h
R : Type u_1
inst✝ : CommSemiring R
f g : R⟦X⟧
n : ℕ
⊢ (coeff R n) (f * g).derivativeFun = (coeff R n) (f • g.derivativeFun + g • f.derivativeFun)

Tactic:
have h₁ : n < n + 1 := lt_succ_self n

Result:
case h
R : Type u_1
inst✝ : CommSemiring R
f g : R⟦X⟧
n : ℕ
h₁ : n < n + 1
⊢ (coeff R n) (f * g).derivativeFun = (coeff R n) (f • g.derivativeFun + g • f.derivativeFun)
-- Mathlib/Algebra/SkewMonoidAlgebra/Basic.lean
theorem sum_add_index {S : Type*} [DecidableEq G] [AddCommMonoid S]
    {f g : SkewMonoidAlgebra k G} {h : G → k → S} (h_zero : ∀ a ∈ f.support ∪ g.support, h a 0 = 0)
    (h_add : ∀ a ∈ f.support ∪ g.support, ∀ b₁ b₂, h a (b₁ + b₂) = h a b₁ + h a b₂) :
    (f + g).sum h = f.sum h + g.sum h

Proof state:
k : Type u_1
G : Type u_2
inst✝² : AddCommMonoid k
S : Type u_3
inst✝¹ : DecidableEq G
inst✝ : AddCommMonoid S
f g : SkewMonoidAlgebra k G
h : G → k → S
h_zero : ∀ a ∈ f.support ∪ g.support, h a 0 = 0
h_add : ∀ a ∈ f.support ∪ g.support, ∀ (b₁ b₂ : k), h a (b₁ + b₂) = h a b₁ + h a b₂
⊢ (f + g).sum h = f.sum h + g.sum h

Tactic:
rw [show f + g = ⟨f.toFinsupp + g.toFinsupp⟩ by rw [ofFinsupp_add, eta]]

Result:
k : Type u_1
G : Type u_2
inst✝² : AddCommMonoid k
S : Type u_3
inst✝¹ : DecidableEq G
inst✝ : AddCommMonoid S
f g : SkewMonoidAlgebra k G
h : G → k → S
h_zero : ∀ a ∈ f.support ∪ g.support, h a 0 = 0
h_add : ∀ a ∈ f.support ∪ g.support, ∀ (b₁ b₂ : k), h a (b₁ + b₂) = h a b₁ + h a b₂
⊢ { toFinsupp := f.toFinsupp + g.toFinsupp }.sum h = f.sum h + g.sum h

Proof state:
k : Type u_1
G : Type u_2
inst✝² : AddCommMonoid k
S : Type u_3
inst✝¹ : DecidableEq G
inst✝ : AddCommMonoid S
f g : SkewMonoidAlgebra k G
h : G → k → S
h_zero : ∀ a ∈ f.support ∪ g.support, h a 0 = 0
h_add : ∀ a ∈ f.support ∪ g.support, ∀ (b₁ b₂ : k), h a (b₁ + b₂) = h a b₁ + h a b₂
⊢ f + g = { toFinsupp := f.toFinsupp + g.toFinsupp }

Tactic:
rw [ofFinsupp_add, eta]

Result:
no goals

Proof state:
k : Type u_1
G : Type u_2
inst✝² : AddCommMonoid k
S : Type u_3
inst✝¹ : DecidableEq G
inst✝ : AddCommMonoid S
f g : SkewMonoidAlgebra k G
h : G → k → S
h_zero : ∀ a ∈ f.support ∪ g.support, h a 0 = 0
h_add : ∀ a ∈ f.support ∪ g.support, ∀ (b₁ b₂ : k), h a (b₁ + b₂) = h a b₁ + h a b₂
⊢ { toFinsupp := f.toFinsupp + g.toFinsupp }.sum h = f.sum h + g.sum h

Tactic:
exact Finsupp.sum_add_index h_zero h_add

Result:
no goals
-- Mathlib/LinearAlgebra/AffineSpace/AffineSubspace/Defs.lean
theorem mem_mk'_iff_vsub_mem {p₁ p₂ : P} {direction : Submodule k V} :
    p₂ ∈ mk' p₁ direction ↔ p₂ -ᵥ p₁ ∈ direction

Proof state:
case refine_2
k : Type u_1
V : Type u_2
P : Type u_3
inst✝³ : Ring k
inst✝² : AddCommGroup V
inst✝¹ : Module k V
inst✝ : AffineSpace V P
p₁ p₂ : P
direction : Submodule k V
h : p₂ -ᵥ p₁ ∈ direction
⊢ p₂ ∈ mk' p₁ direction

Tactic:
rw [← vsub_vadd p₂ p₁]

Result:
case refine_2
k : Type u_1
V : Type u_2
P : Type u_3
inst✝³ : Ring k
inst✝² : AddCommGroup V
inst✝¹ : Module k V
inst✝ : AffineSpace V P
p₁ p₂ : P
direction : Submodule k V
h : p₂ -ᵥ p₁ ∈ direction
⊢ (p₂ -ᵥ p₁) +ᵥ p₁ ∈ mk' p₁ direction

Proof state:
case refine_1
k : Type u_1
V : Type u_2
P : Type u_3
inst✝³ : Ring k
inst✝² : AddCommGroup V
inst✝¹ : Module k V
inst✝ : AffineSpace V P
p₁ p₂ : P
direction : Submodule k V
h : p₂ ∈ mk' p₁ direction
⊢ p₂ -ᵥ p₁ ∈ (mk' p₁ direction).direction

Tactic:
exact vsub_mem_direction h (self_mem_mk' _ _)

Result:
no goals

Proof state:
case refine_1
k : Type u_1
V : Type u_2
P : Type u_3
inst✝³ : Ring k
inst✝² : AddCommGroup V
inst✝¹ : Module k V
inst✝ : AffineSpace V P
p₁ p₂ : P
direction : Submodule k V
h : p₂ ∈ mk' p₁ direction
⊢ p₂ -ᵥ p₁ ∈ direction

Tactic:
rw [← direction_mk' p₁ direction]

Result:
case refine_1
k : Type u_1
V : Type u_2
P : Type u_3
inst✝³ : Ring k
inst✝² : AddCommGroup V
inst✝¹ : Module k V
inst✝ : AffineSpace V P
p₁ p₂ : P
direction : Submodule k V
h : p₂ ∈ mk' p₁ direction
⊢ p₂ -ᵥ p₁ ∈ (mk' p₁ direction).direction

Proof state:
k : Type u_1
V : Type u_2
P : Type u_3
inst✝³ : Ring k
inst✝² : AddCommGroup V
inst✝¹ : Module k V
inst✝ : AffineSpace V P
p₁ p₂ : P
direction : Submodule k V
⊢ p₂ ∈ mk' p₁ direction ↔ p₂ -ᵥ p₁ ∈ direction

Tactic:
refine ⟨fun h => ?_, fun h => ?_⟩

Result:
case refine_1
k : Type u_1
V : Type u_2
P : Type u_3
inst✝³ : Ring k
inst✝² : AddCommGroup V
inst✝¹ : Module k V
inst✝ : AffineSpace V P
p₁ p₂ : P
direction : Submodule k V
h : p₂ ∈ mk' p₁ direction
⊢ p₂ -ᵥ p₁ ∈ direction

case refine_2
k : Type u_1
V : Type u_2
P : Type u_3
inst✝³ : Ring k
inst✝² : AddCommGroup V
inst✝¹ : Module k V
inst✝ : AffineSpace V P
p₁ p₂ : P
direction : Submodule k V
h : p₂ -ᵥ p₁ ∈ direction
⊢ p₂ ∈ mk' p₁ direction

Proof state:
case refine_2
k : Type u_1
V : Type u_2
P : Type u_3
inst✝³ : Ring k
inst✝² : AddCommGroup V
inst✝¹ : Module k V
inst✝ : AffineSpace V P
p₁ p₂ : P
direction : Submodule k V
h : p₂ -ᵥ p₁ ∈ direction
⊢ (p₂ -ᵥ p₁) +ᵥ p₁ ∈ mk' p₁ direction

Tactic:
exact vadd_mem_mk' p₁ h

Result:
no goals
-- Mathlib/Data/Nat/Bitwise.lean
@[simp]
lemma bitwise_zero_left (m : Nat) : bitwise f 0 m = if f false true then m else 0

Proof state:
f : Bool → Bool → Bool
m : ℕ
⊢ bitwise f 0 m = if f false true = true then m else 0

Tactic:
simp [bitwise]

Result:
no goals
-- Mathlib/Algebra/Ring/Subsemiring/Basic.lean
theorem top_prod (s : Subsemiring S) : (⊤ : Subsemiring R).prod s = s.comap (RingHom.snd R S) :=
  ext fun x => by simp [mem_prod, MonoidHom.coe_snd]

Proof state:
R : Type u
S : Type v
inst✝¹ : NonAssocSemiring R
inst✝ : NonAssocSemiring S
s : Subsemiring S
x : R × S
⊢ x ∈ ⊤.prod s ↔ x ∈ comap (RingHom.snd R S) s

Tactic:
simp [mem_prod, MonoidHom.coe_snd]

Result:
no goals
-- Mathlib/Algebra/Order/Monovary.lean
/-- Two functions antivary iff the rearrangement inequality holds. -/
lemma antivaryOn_iff_mul_rearrangement :
    AntivaryOn f g s ↔
      ∀ ⦃i⦄, i ∈ s → ∀ ⦃j⦄, j ∈ s → f i * g i + f j * g j ≤ f i * g j + f j * g i

Proof state:
ι : Type u_1
α : Type u_2
inst✝ : LinearOrderedRing α
f g : ι → α
s : Set ι
⊢ AntivaryOn f g s ↔ ∀ ⦃i : ι⦄, i ∈ s → ∀ ⦃j : ι⦄, j ∈ s → f i * g i + f j * g j ≤ f i * g j + f j * g i

Tactic:
simp only [smul_eq_mul, antivaryOn_iff_smul_rearrangement]

Result:
no goals
-- Mathlib/Data/Stream/Init.lean
theorem length_take (n : ℕ) (s : Stream' α) : (take n s).length = n

Proof state:
α : Type u
n : ℕ
s : Stream' α
⊢ (take n s).length = n

Tactic:
induction n generalizing s <;> simp [*, take_succ]

Result:
no goals
-- Mathlib/Algebra/GroupWithZero/Basic.lean
theorem ne_zero_of_one_div_ne_zero {a : G₀} (h : 1 / a ≠ 0) : a ≠ 0 := fun ha : a = 0 => by
  rw [ha, div_zero] at h
  contradiction

Proof state:
G₀ : Type u_2
inst✝ : GroupWithZero G₀
a : G₀
h : 1 / a ≠ 0
ha : a = 0
⊢ False

Tactic:
rw [ha, div_zero] at h

Result:
G₀ : Type u_2
inst✝ : GroupWithZero G₀
a : G₀
h : 0 ≠ 0
ha : a = 0
⊢ False

Proof state:
G₀ : Type u_2
inst✝ : GroupWithZero G₀
a : G₀
h : 0 ≠ 0
ha : a = 0
⊢ False

Tactic:
contradiction

Result:
no goals
-- Mathlib/SetTheory/Ordinal/Arithmetic.lean
theorem lt_omega0 {o : Ordinal} : o < ω ↔ ∃ n : ℕ, o = n

Proof state:
o : Ordinal.{u_1}
⊢ o < ω ↔ ∃ n, o = ↑n

Tactic:
simp_rw [← Cardinal.ord_aleph0, Cardinal.lt_ord, lt_aleph0, card_eq_nat]

Result:
no goals
-- Mathlib/Analysis/InnerProductSpace/PiL2.lean
theorem repr_reindex (b : OrthonormalBasis ι 𝕜 E) (e : ι ≃ ι') (x : E) (i' : ι') :
    (b.reindex e).repr x i' = b.repr x (e.symm i')

Proof state:
ι : Type u_1
ι' : Type u_2
𝕜 : Type u_3
inst✝⁴ : RCLike 𝕜
E : Type u_4
inst✝³ : NormedAddCommGroup E
inst✝² : InnerProductSpace 𝕜 E
inst✝¹ : Fintype ι
inst✝ : Fintype ι'
b : OrthonormalBasis ι 𝕜 E
e : ι ≃ ι'
x : E
i' : ι'
⊢ (b.reindex e).repr x i' = b.repr x (e.symm i')

Tactic:
classical
rw [OrthonormalBasis.repr_apply_apply, b.repr_apply_apply, OrthonormalBasis.coe_reindex,
  comp_apply]

Result:
no goals

Proof state:
ι : Type u_1
ι' : Type u_2
𝕜 : Type u_3
inst✝⁴ : RCLike 𝕜
E : Type u_4
inst✝³ : NormedAddCommGroup E
inst✝² : InnerProductSpace 𝕜 E
inst✝¹ : Fintype ι
inst✝ : Fintype ι'
b : OrthonormalBasis ι 𝕜 E
e : ι ≃ ι'
x : E
i' : ι'
⊢ (b.reindex e).repr x i' = b.repr x (e.symm i')

Tactic:
rw [OrthonormalBasis.repr_apply_apply, b.repr_apply_apply, OrthonormalBasis.coe_reindex,
  comp_apply]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Std/Data/DHashMap/Internal/List/Associative.lean
theorem insertListIfNewUnit_perm_of_perm_first [BEq α] [EquivBEq α] {l1 l2 : List ((_ : α) × Unit)}
    {toInsert : List α } (h : Perm l1 l2) (distinct : DistinctKeys l1) :
    Perm (insertListIfNewUnit l1 toInsert) (insertListIfNewUnit l2 toInsert)

Proof state:
case cons
α : Type u
inst✝¹ : BEq α
inst✝ : EquivBEq α
hd : α
tl : List α
ih :
  ∀ {l1 l2 : List ((_ : α) × Unit)},
    l1.Perm l2 → DistinctKeys l1 → (insertListIfNewUnit l1 tl).Perm (insertListIfNewUnit l2 tl)
l1 l2 : List ((_ : α) × Unit)
h : l1.Perm l2
distinct : DistinctKeys l1
⊢ (insertListIfNewUnit (insertEntryIfNew hd () l1) tl).Perm (insertListIfNewUnit (insertEntryIfNew hd () l2) tl)

Tactic:
apply ih

Result:
case cons.h
α : Type u
inst✝¹ : BEq α
inst✝ : EquivBEq α
hd : α
tl : List α
ih :
  ∀ {l1 l2 : List ((_ : α) × Unit)},
    l1.Perm l2 → DistinctKeys l1 → (insertListIfNewUnit l1 tl).Perm (insertListIfNewUnit l2 tl)
l1 l2 : List ((_ : α) × Unit)
h : l1.Perm l2
distinct : DistinctKeys l1
⊢ (insertEntryIfNew hd () l1).Perm (insertEntryIfNew hd () l2)

case cons.distinct
α : Type u
inst✝¹ : BEq α
inst✝ : EquivBEq α
hd : α
tl : List α
ih :
  ∀ {l1 l2 : List ((_ : α) × Unit)},
    l1.Perm l2 → DistinctKeys l1 → (insertListIfNewUnit l1 tl).Perm (insertListIfNewUnit l2 tl)
l1 l2 : List ((_ : α) × Unit)
h : l1.Perm l2
distinct : DistinctKeys l1
⊢ DistinctKeys (insertEntryIfNew hd () l1)

Proof state:
case neg
α : Type u
inst✝¹ : BEq α
inst✝ : EquivBEq α
hd : α
tl : List α
ih :
  ∀ {l1 l2 : List ((_ : α) × Unit)},
    l1.Perm l2 → DistinctKeys l1 → (insertListIfNewUnit l1 tl).Perm (insertListIfNewUnit l2 tl)
l1 l2 : List ((_ : α) × Unit)
h : l1.Perm l2
distinct : DistinctKeys l1
contains_eq : containsKey hd l1 = containsKey hd l2
contains_hd : ¬containsKey hd l2 = true
⊢ (if containsKey hd l2 = true then l1 else ⟨hd, ()⟩ :: l1).Perm
    (if containsKey hd l2 = true then l2 else ⟨hd, ()⟩ :: l2)

Tactic:
simp only [contains_hd, Bool.false_eq_true, ↓reduceIte, List.perm_cons]

Result:
case neg
α : Type u
inst✝¹ : BEq α
inst✝ : EquivBEq α
hd : α
tl : List α
ih :
  ∀ {l1 l2 : List ((_ : α) × Unit)},
    l1.Perm l2 → DistinctKeys l1 → (insertListIfNewUnit l1 tl).Perm (insertListIfNewUnit l2 tl)
l1 l2 : List ((_ : α) × Unit)
h : l1.Perm l2
distinct : DistinctKeys l1
contains_eq : containsKey hd l1 = containsKey hd l2
contains_hd : ¬containsKey hd l2 = true
⊢ l1.Perm l2

Proof state:
case cons.distinct
α : Type u
inst✝¹ : BEq α
inst✝ : EquivBEq α
hd : α
tl : List α
ih :
  ∀ {l1 l2 : List ((_ : α) × Unit)},
    l1.Perm l2 → DistinctKeys l1 → (insertListIfNewUnit l1 tl).Perm (insertListIfNewUnit l2 tl)
l1 l2 : List ((_ : α) × Unit)
h : l1.Perm l2
distinct : DistinctKeys l1
⊢ DistinctKeys (insertEntryIfNew hd () l1)

Tactic:
apply DistinctKeys.insertEntryIfNew distinct

Result:
no goals
-- Mathlib/MeasureTheory/OuterMeasure/Induced.lean
theorem le_extend {s : α} (h : P s) : m s h ≤ extend m s

Proof state:
α : Type u_1
P : α → Prop
m : (s : α) → P s → ℝ≥0∞
s : α
h i✝ : P s
⊢ m s h ≤ m s i✝

Tactic:
rfl

Result:
no goals

Proof state:
α : Type u_1
P : α → Prop
m : (s : α) → P s → ℝ≥0∞
s : α
h : P s
⊢ ∀ (i : P s), m s h ≤ m s i

Tactic:
intro

Result:
α : Type u_1
P : α → Prop
m : (s : α) → P s → ℝ≥0∞
s : α
h i✝ : P s
⊢ m s h ≤ m s i✝

Proof state:
α : Type u_1
P : α → Prop
m : (s : α) → P s → ℝ≥0∞
s : α
h : P s
⊢ m s h ≤ extend m s

Tactic:
simp only [extend, le_iInf_iff]

Result:
α : Type u_1
P : α → Prop
m : (s : α) → P s → ℝ≥0∞
s : α
h : P s
⊢ ∀ (i : P s), m s h ≤ m s i