harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/RingTheory/MvPowerSeries/Inverse.lean
theorem invOfUnit_mul (φ : MvPowerSeries σ R) (u : Rˣ) (h : constantCoeff σ R φ = u) :
    invOfUnit φ u * φ = 1

Proof state:
case hφ
σ : Type u_1
R : Type u_2
inst✝ : Ring R
φ : MvPowerSeries σ R
u : Rˣ
h : (constantCoeff σ R) φ = ↑u
⊢ (constantCoeff σ R) (φ.invOfUnit u) ∈ nonZeroDivisors R

Tactic:
simp only [constantCoeff_invOfUnit, IsUnit.mem_nonZeroDivisors (Units.isUnit u⁻¹)]

Result:
no goals

Proof state:
σ : Type u_1
R : Type u_2
inst✝ : Ring R
φ : MvPowerSeries σ R
u : Rˣ
h : (constantCoeff σ R) φ = ↑u
⊢ φ.invOfUnit u * φ = 1

Tactic:
rw [← mul_cancel_right_mem_nonZeroDivisors (r := φ.invOfUnit u), mul_assoc, one_mul,
  mul_invOfUnit _ _ h, mul_one]

Result:
σ : Type u_1
R : Type u_2
inst✝ : Ring R
φ : MvPowerSeries σ R
u : Rˣ
h : (constantCoeff σ R) φ = ↑u
⊢ φ.invOfUnit u ∈ nonZeroDivisors (MvPowerSeries σ R)

Proof state:
σ : Type u_1
R : Type u_2
inst✝ : Ring R
φ : MvPowerSeries σ R
u : Rˣ
h : (constantCoeff σ R) φ = ↑u
⊢ φ.invOfUnit u ∈ nonZeroDivisors (MvPowerSeries σ R)

Tactic:
apply mem_nonZeroDivisors_of_constantCoeff

Result:
case hφ
σ : Type u_1
R : Type u_2
inst✝ : Ring R
φ : MvPowerSeries σ R
u : Rˣ
h : (constantCoeff σ R) φ = ↑u
⊢ (constantCoeff σ R) (φ.invOfUnit u) ∈ nonZeroDivisors R
-- Mathlib/MeasureTheory/Constructions/Pi.lean
theorem pi_pi_le (m : ∀ i, OuterMeasure (α i)) (s : ∀ i, Set (α i)) :
    OuterMeasure.pi m (pi univ s) ≤ ∏ i, m i (s i)

Proof state:
ι : Type u_1
α : ι → Type u_3
inst✝ : Fintype ι
m : (i : ι) → OuterMeasure (α i)
s : (i : ι) → Set (α i)
⊢ (OuterMeasure.pi m) (univ.pi s) ≤ ∏ i : ι, (m i) (s i)

Tactic:
rcases (pi univ s).eq_empty_or_nonempty with h | h

Result:
case inl
ι : Type u_1
α : ι → Type u_3
inst✝ : Fintype ι
m : (i : ι) → OuterMeasure (α i)
s : (i : ι) → Set (α i)
h : univ.pi s = ∅
⊢ (OuterMeasure.pi m) (univ.pi s) ≤ ∏ i : ι, (m i) (s i)

case inr
ι : Type u_1
α : ι → Type u_3
inst✝ : Fintype ι
m : (i : ι) → OuterMeasure (α i)
s : (i : ι) → Set (α i)
h : (univ.pi s).Nonempty
⊢ (OuterMeasure.pi m) (univ.pi s) ≤ ∏ i : ι, (m i) (s i)

Proof state:
case inr
ι : Type u_1
α : ι → Type u_3
inst✝ : Fintype ι
m : (i : ι) → OuterMeasure (α i)
s : (i : ι) → Set (α i)
h : (univ.pi s).Nonempty
⊢ (OuterMeasure.pi m) (univ.pi s) ≤ ∏ i : ι, (m i) (s i)

Tactic:
exact (boundedBy_le _).trans_eq (piPremeasure_pi h)

Result:
no goals

Proof state:
case inl
ι : Type u_1
α : ι → Type u_3
inst✝ : Fintype ι
m : (i : ι) → OuterMeasure (α i)
s : (i : ι) → Set (α i)
h : univ.pi s = ∅
⊢ (OuterMeasure.pi m) (univ.pi s) ≤ ∏ i : ι, (m i) (s i)

Tactic:
simp [h]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Nat/Simproc.lean
theorem add_sub_add_le (a c : Nat) {b d : Nat} (h : b ≤ d) : a + b - (c + d) = a - (c + (d-b))

Proof state:
b : Nat
ind : ∀ (a c : Nat) {d : Nat}, b ≤ d → a + b - (c + d) = a - (c + (d - b))
a c d✝ d : Nat
h : b + 1 ≤ d + 1
g : b ≤ d
⊢ a + (b + 1) - (c + (d + 1)) = a - (c + (d + 1 - (b + 1)))

Tactic:
rw [Nat.add_succ a, Nat.add_succ c, Nat.succ_sub_succ, Nat.succ_sub_succ,
    ind _ _ g]

Result:
no goals

Proof state:
b : Nat
ind : ∀ (a c : Nat) {d : Nat}, b ≤ d → a + b - (c + d) = a - (c + (d - b))
a c d : Nat
h : b + 1 ≤ 0
⊢ a + (b + 1) - (c + 0) = a - (c + (0 - (b + 1)))

Tactic:
contradiction

Result:
no goals

Proof state:
case succ
b : Nat
ind : ∀ (a c : Nat) {d : Nat}, b ≤ d → a + b - (c + d) = a - (c + (d - b))
a c d : Nat
h : b + 1 ≤ d
⊢ a + (b + 1) - (c + d) = a - (c + (d - (b + 1)))

Tactic:
match d with
| 0 =>
  contradiction
| d + 1 =>
  have g := Nat.le_of_succ_le_succ h
  rw [Nat.add_succ a, Nat.add_succ c, Nat.succ_sub_succ, Nat.succ_sub_succ,
      ind _ _ g]

Result:
no goals

Proof state:
a c b d : Nat
h : b ≤ d
⊢ a + b - (c + d) = a - (c + (d - b))

Tactic:
induction b generalizing a c d with
| zero =>
  simp
| succ b ind =>
  match d with
  | 0 =>
    contradiction
  | d + 1 =>
    have g := Nat.le_of_succ_le_succ h
    rw [Nat.add_succ a, Nat.add_succ c, Nat.succ_sub_succ, Nat.succ_sub_succ,
        ind _ _ g]

Result:
no goals

Proof state:
case zero
a c d : Nat
h : 0 ≤ d
⊢ a + 0 - (c + d) = a - (c + (d - 0))

Tactic:
simp

Result:
no goals

Proof state:
b : Nat
ind : ∀ (a c : Nat) {d : Nat}, b ≤ d → a + b - (c + d) = a - (c + (d - b))
a c d✝ d : Nat
h : b + 1 ≤ d + 1
⊢ a + (b + 1) - (c + (d + 1)) = a - (c + (d + 1 - (b + 1)))

Tactic:
have g := Nat.le_of_succ_le_succ h

Result:
b : Nat
ind : ∀ (a c : Nat) {d : Nat}, b ≤ d → a + b - (c + d) = a - (c + (d - b))
a c d✝ d : Nat
h : b + 1 ≤ d + 1
g : b ≤ d
⊢ a + (b + 1) - (c + (d + 1)) = a - (c + (d + 1 - (b + 1)))
-- Mathlib/Analysis/Calculus/BumpFunction/FiniteDimension.lean
theorem y_pos_of_mem_ball {D : ℝ} {x : E} (Dpos : 0 < D) (D_lt_one : D < 1)
    (hx : x ∈ ball (0 : E) (1 + D)) : 0 < y D x

Proof state:
case refine_1
E : Type u_1
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace ℝ E
inst✝² : FiniteDimensional ℝ E
inst✝¹ : MeasurableSpace E
inst✝ : BorelSpace E
D : ℝ
x : E
Dpos : 0 < D
D_lt_one : D < 1
hx : ‖x‖ < 1 + D
F_comp : HasCompactSupport (w D)
B : LocallyIntegrable φ μ
C : Continuous (w D)
⊢ Integrable (fun i => w D i * φ (x - i)) μ

Tactic:
exact (F_comp.convolutionExists_left (lsmul ℝ ℝ : ℝ →L[ℝ] ℝ →L[ℝ] ℝ) C B x).integrable

Result:
no goals

Proof state:
E : Type u_1
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace ℝ E
inst✝² : FiniteDimensional ℝ E
inst✝¹ : MeasurableSpace E
inst✝ : BorelSpace E
D : ℝ
x : E
Dpos : 0 < D
D_lt_one : D < 1
hx : ‖x‖ < 1 + D
z : E := (D / (1 + D)) • x
hz : z = (D / (1 + D)) • x
B : 0 < 1 + D
y : E
hy : y ∈ ball z (D * (1 + D - ‖x‖) / (1 + D))
⊢ (D - (1 + D)) / (1 + D) ≤ 0

Tactic:
apply div_nonpos_of_nonpos_of_nonneg _ B.le

Result:
E : Type u_1
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace ℝ E
inst✝² : FiniteDimensional ℝ E
inst✝¹ : MeasurableSpace E
inst✝ : BorelSpace E
D : ℝ
x : E
Dpos : 0 < D
D_lt_one : D < 1
hx : ‖x‖ < 1 + D
z : E := (D / (1 + D)) • x
hz : z = (D / (1 + D)) • x
B : 0 < 1 + D
y : E
hy : y ∈ ball z (D * (1 + D - ‖x‖) / (1 + D))
⊢ D - (1 + D) ≤ 0
-- Mathlib/Data/List/Permutation.lean
theorem length_foldr_permutationsAux2' (t : α) (ts : List α) (r L : List (List α)) (n)
    (H : ∀ l ∈ L, length l = n) :
    length (foldr (fun y r => (permutationsAux2 t ts r y id).2) r L) = n * length L + length r

Proof state:
α : Type u_1
t : α
ts : List α
r L : List (List α)
n : ℕ
H : ∀ l ∈ L, l.length = n
⊢ (map length L).sum = n * L.length

Tactic:
induction' L with l L ih

Result:
case nil
α : Type u_1
t : α
ts : List α
r : List (List α)
n : ℕ
H : ∀ l ∈ [], l.length = n
⊢ (map length []).sum = n * [].length

case cons
α : Type u_1
t : α
ts : List α
r : List (List α)
n : ℕ
l : List α
L : List (List α)
ih : (∀ l ∈ L, l.length = n) → (map length L).sum = n * L.length
H : ∀ l_1 ∈ l :: L, l_1.length = n
⊢ (map length (l :: L)).sum = n * (l :: L).length

Proof state:
case nil
α : Type u_1
t : α
ts : List α
r : List (List α)
n : ℕ
H : ∀ l ∈ [], l.length = n
⊢ (map length []).sum = n * [].length

Tactic:
simp

Result:
no goals

Proof state:
case cons
α : Type u_1
t : α
ts : List α
r : List (List α)
n : ℕ
l : List α
L : List (List α)
ih : (∀ l ∈ L, l.length = n) → (map length L).sum = n * L.length
H : ∀ l_1 ∈ l :: L, l_1.length = n
sum_map : (map length L).sum = n * L.length
⊢ (map length (l :: L)).sum = n * (l :: L).length

Tactic:
have length_l : length l = n := H _ (mem_cons_self _ _)

Result:
case cons
α : Type u_1
t : α
ts : List α
r : List (List α)
n : ℕ
l : List α
L : List (List α)
ih : (∀ l ∈ L, l.length = n) → (map length L).sum = n * L.length
H : ∀ l_1 ∈ l :: L, l_1.length = n
sum_map : (map length L).sum = n * L.length
length_l : l.length = n
⊢ (map length (l :: L)).sum = n * (l :: L).length

Proof state:
case cons
α : Type u_1
t : α
ts : List α
r : List (List α)
n : ℕ
l : List α
L : List (List α)
ih : (∀ l ∈ L, l.length = n) → (map length L).sum = n * L.length
H : ∀ l_1 ∈ l :: L, l_1.length = n
sum_map : (map length L).sum = n * L.length
length_l : l.length = n
⊢ (map length (l :: L)).sum = n * (l :: L).length

Tactic:
simp [sum_map, length_l, Nat.mul_add, Nat.add_comm, mul_succ]

Result:
no goals

Proof state:
α : Type u_1
t : α
ts : List α
r L : List (List α)
n : ℕ
H : ∀ l ∈ L, l.length = n
⊢ (foldr (fun y r => (permutationsAux2 t ts r y id).2) r L).length = n * L.length + r.length

Tactic:
rw [length_foldr_permutationsAux2, (_ : (map length L).sum = n * length L)]

Result:
α : Type u_1
t : α
ts : List α
r L : List (List α)
n : ℕ
H : ∀ l ∈ L, l.length = n
⊢ (map length L).sum = n * L.length

Proof state:
case cons
α : Type u_1
t : α
ts : List α
r : List (List α)
n : ℕ
l : List α
L : List (List α)
ih : (∀ l ∈ L, l.length = n) → (map length L).sum = n * L.length
H : ∀ l_1 ∈ l :: L, l_1.length = n
⊢ (map length (l :: L)).sum = n * (l :: L).length

Tactic:
have sum_map : (map length L).sum = n * length L := ih fun l m => H l (mem_cons_of_mem _ m)

Result:
case cons
α : Type u_1
t : α
ts : List α
r : List (List α)
n : ℕ
l : List α
L : List (List α)
ih : (∀ l ∈ L, l.length = n) → (map length L).sum = n * L.length
H : ∀ l_1 ∈ l :: L, l_1.length = n
sum_map : (map length L).sum = n * L.length
⊢ (map length (l :: L)).sum = n * (l :: L).length
-- Mathlib/MeasureTheory/Integral/IntegrableOn.lean
theorem integrableOn_Lp_of_measure_ne_top {E} [NormedAddCommGroup E] {p : ℝ≥0∞} {s : Set α}
    (f : Lp E p μ) (hp : 1 ≤ p) (hμs : μ s ≠ ∞) : IntegrableOn f s μ

Proof state:
α : Type u_1
inst✝¹ : MeasurableSpace α
μ : Measure α
E : Type u_6
inst✝ : NormedAddCommGroup E
p : ℝ≥0∞
s : Set α
f : ↥(Lp E p μ)
hp : 1 ≤ p
hμs : μ s ≠ ⊤
⊢ MemLp (↑↑f) 1 (μ.restrict s)

Tactic:
have hμ_restrict_univ : (μ.restrict s) Set.univ < ∞ := by
  simpa only [Set.univ_inter, MeasurableSet.univ, Measure.restrict_apply, lt_top_iff_ne_top]

Result:
α : Type u_1
inst✝¹ : MeasurableSpace α
μ : Measure α
E : Type u_6
inst✝ : NormedAddCommGroup E
p : ℝ≥0∞
s : Set α
f : ↥(Lp E p μ)
hp : 1 ≤ p
hμs : μ s ≠ ⊤
hμ_restrict_univ : (μ.restrict s) univ < ⊤
⊢ MemLp (↑↑f) 1 (μ.restrict s)

Proof state:
α : Type u_1
inst✝¹ : MeasurableSpace α
μ : Measure α
E : Type u_6
inst✝ : NormedAddCommGroup E
p : ℝ≥0∞
s : Set α
f : ↥(Lp E p μ)
hp : 1 ≤ p
hμs : μ s ≠ ⊤
hμ_restrict_univ : (μ.restrict s) univ < ⊤
⊢ MemLp (↑↑f) 1 (μ.restrict s)

Tactic:
haveI hμ_finite : IsFiniteMeasure (μ.restrict s) := ⟨hμ_restrict_univ⟩

Result:
α : Type u_1
inst✝¹ : MeasurableSpace α
μ : Measure α
E : Type u_6
inst✝ : NormedAddCommGroup E
p : ℝ≥0∞
s : Set α
f : ↥(Lp E p μ)
hp : 1 ≤ p
hμs : μ s ≠ ⊤
hμ_restrict_univ : (μ.restrict s) univ < ⊤
hμ_finite : IsFiniteMeasure (μ.restrict s)
⊢ MemLp (↑↑f) 1 (μ.restrict s)

Proof state:
α : Type u_1
inst✝¹ : MeasurableSpace α
μ : Measure α
E : Type u_6
inst✝ : NormedAddCommGroup E
p : ℝ≥0∞
s : Set α
f : ↥(Lp E p μ)
hp : 1 ≤ p
hμs : μ s ≠ ⊤
⊢ IntegrableOn (↑↑f) s μ

Tactic:
refine memLp_one_iff_integrable.mp ?_

Result:
α : Type u_1
inst✝¹ : MeasurableSpace α
μ : Measure α
E : Type u_6
inst✝ : NormedAddCommGroup E
p : ℝ≥0∞
s : Set α
f : ↥(Lp E p μ)
hp : 1 ≤ p
hμs : μ s ≠ ⊤
⊢ MemLp (↑↑f) 1 (μ.restrict s)

Proof state:
α : Type u_1
inst✝¹ : MeasurableSpace α
μ : Measure α
E : Type u_6
inst✝ : NormedAddCommGroup E
p : ℝ≥0∞
s : Set α
f : ↥(Lp E p μ)
hp : 1 ≤ p
hμs : μ s ≠ ⊤
hμ_restrict_univ : (μ.restrict s) univ < ⊤
hμ_finite : IsFiniteMeasure (μ.restrict s)
⊢ MemLp (↑↑f) 1 (μ.restrict s)

Tactic:
exact ((Lp.memLp _).restrict s).mono_exponent hp

Result:
no goals

Proof state:
α : Type u_1
inst✝¹ : MeasurableSpace α
μ : Measure α
E : Type u_6
inst✝ : NormedAddCommGroup E
p : ℝ≥0∞
s : Set α
f : ↥(Lp E p μ)
hp : 1 ≤ p
hμs : μ s ≠ ⊤
⊢ (μ.restrict s) univ < ⊤

Tactic:
simpa only [Set.univ_inter, MeasurableSet.univ, Measure.restrict_apply, lt_top_iff_ne_top]

Result:
no goals
-- Mathlib/RingTheory/NonUnitalSubsemiring/Basic.lean
theorem mem_iSup_of_directed {ι} [hι : Nonempty ι] {S : ι → NonUnitalSubsemiring R}
    (hS : Directed (· ≤ ·) S) {x : R} : (x ∈ ⨆ i, S i) ↔ ∃ i, x ∈ S i

Proof state:
R : Type u
inst✝ : NonUnitalNonAssocSemiring R
ι : Sort u_2
hι : Nonempty ι
S : ι → NonUnitalSubsemiring R
hS : Directed (fun x1 x2 => x1 ≤ x2) S
x : R
U : NonUnitalSubsemiring R :=
  NonUnitalSubsemiring.mk' (⋃ i, ↑(S i)) (⨆ i, (S i).toSubsemigroup) ⋯ (⨆ i, (S i).toAddSubmonoid) ⋯
⊢ x ∈ ⨆ i, S i → ∃ i, x ∈ S i

Tactic:
suffices H : ⨆ i, S i ≤ U by simpa [U] using @H x

Result:
R : Type u
inst✝ : NonUnitalNonAssocSemiring R
ι : Sort u_2
hι : Nonempty ι
S : ι → NonUnitalSubsemiring R
hS : Directed (fun x1 x2 => x1 ≤ x2) S
x : R
U : NonUnitalSubsemiring R :=
  NonUnitalSubsemiring.mk' (⋃ i, ↑(S i)) (⨆ i, (S i).toSubsemigroup) ⋯ (⨆ i, (S i).toAddSubmonoid) ⋯
⊢ ⨆ i, S i ≤ U

Proof state:
R : Type u
inst✝ : NonUnitalNonAssocSemiring R
ι : Sort u_2
hι : Nonempty ι
S : ι → NonUnitalSubsemiring R
hS : Directed (fun x1 x2 => x1 ≤ x2) S
x : R
U : NonUnitalSubsemiring R :=
  NonUnitalSubsemiring.mk' (⋃ i, ↑(S i)) (⨆ i, (S i).toSubsemigroup) ⋯ (⨆ i, (S i).toAddSubmonoid) ⋯
H : ⨆ i, S i ≤ U
⊢ x ∈ ⨆ i, S i → ∃ i, x ∈ S i

Tactic:
simpa [U] using @H x

Result:
no goals

Proof state:
R : Type u
inst✝ : NonUnitalNonAssocSemiring R
ι : Sort u_2
hι : Nonempty ι
S : ι → NonUnitalSubsemiring R
hS : Directed (fun x1 x2 => x1 ≤ x2) S
x : R
U : NonUnitalSubsemiring R :=
  NonUnitalSubsemiring.mk' (⋃ i, ↑(S i)) (⨆ i, (S i).toSubsemigroup) ⋯ (⨆ i, (S i).toAddSubmonoid) ⋯
⊢ ⨆ i, S i ≤ U

Tactic:
exact iSup_le fun i x hx => Set.mem_iUnion.2 ⟨i, hx⟩

Result:
no goals

Proof state:
R : Type u
inst✝ : NonUnitalNonAssocSemiring R
ι : Sort u_2
hι : Nonempty ι
S : ι → NonUnitalSubsemiring R
hS : Directed (fun x1 x2 => x1 ≤ x2) S
x : R
⊢ x ∈ ⨆ i, S i ↔ ∃ i, x ∈ S i

Tactic:
refine ⟨?_, fun ⟨i, hi⟩ ↦ le_iSup S i hi⟩

Result:
R : Type u
inst✝ : NonUnitalNonAssocSemiring R
ι : Sort u_2
hι : Nonempty ι
S : ι → NonUnitalSubsemiring R
hS : Directed (fun x1 x2 => x1 ≤ x2) S
x : R
⊢ x ∈ ⨆ i, S i → ∃ i, x ∈ S i

Proof state:
R : Type u
inst✝ : NonUnitalNonAssocSemiring R
ι : Sort u_2
hι : Nonempty ι
S : ι → NonUnitalSubsemiring R
hS : Directed (fun x1 x2 => x1 ≤ x2) S
x : R
⊢ x ∈ ⨆ i, S i → ∃ i, x ∈ S i

Tactic:
let U : NonUnitalSubsemiring R :=
  NonUnitalSubsemiring.mk' (⋃ i, (S i : Set R))
    (⨆ i, (S i).toSubsemigroup) (Subsemigroup.coe_iSup_of_directed hS)
    (⨆ i, (S i).toAddSubmonoid) (AddSubmonoid.coe_iSup_of_directed hS)

Result:
R : Type u
inst✝ : NonUnitalNonAssocSemiring R
ι : Sort u_2
hι : Nonempty ι
S : ι → NonUnitalSubsemiring R
hS : Directed (fun x1 x2 => x1 ≤ x2) S
x : R
U : NonUnitalSubsemiring R :=
  NonUnitalSubsemiring.mk' (⋃ i, ↑(S i)) (⨆ i, (S i).toSubsemigroup) ⋯ (⨆ i, (S i).toAddSubmonoid) ⋯
⊢ x ∈ ⨆ i, S i → ∃ i, x ∈ S i
-- Mathlib/Analysis/Normed/Affine/Simplex.lean
lemma equilateral_iff_dist_eq_and_dist_eq {t : Triangle R P} {i₁ i₂ i₃ : Fin 3} (h₁₂ : i₁ ≠ i₂)
    (h₁₃ : i₁ ≠ i₃) (h₂₃ : i₂ ≠ i₃) :
    t.Equilateral ↔ dist (t.points i₁) (t.points i₂) = dist (t.points i₁) (t.points i₃) ∧
      dist (t.points i₁) (t.points i₂) = dist (t.points i₂) (t.points i₃)

Proof state:
R : Type u_1
V : Type u_2
P : Type u_3
inst✝⁴ : Ring R
inst✝³ : SeminormedAddCommGroup V
inst✝² : PseudoMetricSpace P
inst✝¹ : Module R V
inst✝ : NormedAddTorsor V P
t : Triangle R P
i₁ i₂ i₃ : Fin 3
h₁₂ : i₁ ≠ i₂
h₁₃ : i₁ ≠ i₃
h₂₃ : i₂ ≠ i₃
⊢ Simplex.Equilateral t ↔
    dist (t.points i₁) (t.points i₂) = dist (t.points i₁) (t.points i₃) ∧
      dist (t.points i₁) (t.points i₂) = dist (t.points i₂) (t.points i₃)

Tactic:
refine ⟨fun ⟨r, hr⟩ ↦ ?_, fun h ↦ ?_⟩

Result:
case refine_1
R : Type u_1
V : Type u_2
P : Type u_3
inst✝⁴ : Ring R
inst✝³ : SeminormedAddCommGroup V
inst✝² : PseudoMetricSpace P
inst✝¹ : Module R V
inst✝ : NormedAddTorsor V P
t : Triangle R P
i₁ i₂ i₃ : Fin 3
h₁₂ : i₁ ≠ i₂
h₁₃ : i₁ ≠ i₃
h₂₃ : i₂ ≠ i₃
x✝ : Simplex.Equilateral t
r : ℝ
hr : ∀ (i j : Fin (2 + 1)), i ≠ j → dist (t.points i) (t.points j) = r
⊢ dist (t.points i₁) (t.points i₂) = dist (t.points i₁) (t.points i₃) ∧
    dist (t.points i₁) (t.points i₂) = dist (t.points i₂) (t.points i₃)

case refine_2
R : Type u_1
V : Type u_2
P : Type u_3
inst✝⁴ : Ring R
inst✝³ : SeminormedAddCommGroup V
inst✝² : PseudoMetricSpace P
inst✝¹ : Module R V
inst✝ : NormedAddTorsor V P
t : Triangle R P
i₁ i₂ i₃ : Fin 3
h₁₂ : i₁ ≠ i₂
h₁₃ : i₁ ≠ i₃
h₂₃ : i₂ ≠ i₃
h :
  dist (t.points i₁) (t.points i₂) = dist (t.points i₁) (t.points i₃) ∧
    dist (t.points i₁) (t.points i₂) = dist (t.points i₂) (t.points i₃)
⊢ Simplex.Equilateral t

Proof state:
case refine_2.intro.inr.inl.intro
R : Type u_1
V : Type u_2
P : Type u_3
inst✝⁴ : Ring R
inst✝³ : SeminormedAddCommGroup V
inst✝² : PseudoMetricSpace P
inst✝¹ : Module R V
inst✝ : NormedAddTorsor V P
t : Triangle R P
i₃ : Fin 3
i j : Fin (2 + 1)
hij : i ≠ j
h₂₃ : i ≠ i₃
h₁₃ : j ≠ i₃
h₁₂ : j ≠ i
h₁ : dist (t.points j) (t.points i) = dist (t.points j) (t.points i₃)
h₂ : dist (t.points j) (t.points i) = dist (t.points i) (t.points i₃)
⊢ dist (t.points i) (t.points j) = dist (t.points j) (t.points i)

Tactic:
exact dist_comm _ _

Result:
no goals

Proof state:
case refine_2.intro.inl.intro
R : Type u_1
V : Type u_2
P : Type u_3
inst✝⁴ : Ring R
inst✝³ : SeminormedAddCommGroup V
inst✝² : PseudoMetricSpace P
inst✝¹ : Module R V
inst✝ : NormedAddTorsor V P
t : Triangle R P
i₃ : Fin 3
i j : Fin (2 + 1)
hij : i ≠ j
h₁₃ : i ≠ i₃
h₂₃ : j ≠ i₃
h₁₂ : i ≠ j
h₁ : dist (t.points i) (t.points j) = dist (t.points i) (t.points i₃)
h₂ : dist (t.points i) (t.points j) = dist (t.points j) (t.points i₃)
⊢ dist (t.points i) (t.points j) = dist (t.points i) (t.points j)

Tactic:
rfl

Result:
no goals
-- Mathlib/Algebra/BigOperators/Group/List/Lemmas.lean
lemma length_sigma {σ : α → Type*} (l₁ : List α) (l₂ : ∀ a, List (σ a)) :
    length (l₁.sigma l₂) = (l₁.map fun a ↦ length (l₂ a)).sum

Proof state:
case cons
α : Type u_2
σ : α → Type u_8
l₂ : (a : α) → List (σ a)
x : α
l₁ : List α
IH : (l₁.sigma l₂).length = (map (fun a => (l₂ a).length) l₁).sum
⊢ ((x :: l₁).sigma l₂).length = (map (fun a => (l₂ a).length) (x :: l₁)).sum

Tactic:
simp only [sigma_cons, length_append, length_map, IH, map, sum_cons]

Result:
no goals

Proof state:
α : Type u_2
σ : α → Type u_8
l₁ : List α
l₂ : (a : α) → List (σ a)
⊢ (l₁.sigma l₂).length = (map (fun a => (l₂ a).length) l₁).sum

Tactic:
induction' l₁ with x l₁ IH

Result:
case nil
α : Type u_2
σ : α → Type u_8
l₂ : (a : α) → List (σ a)
⊢ ([].sigma l₂).length = (map (fun a => (l₂ a).length) []).sum

case cons
α : Type u_2
σ : α → Type u_8
l₂ : (a : α) → List (σ a)
x : α
l₁ : List α
IH : (l₁.sigma l₂).length = (map (fun a => (l₂ a).length) l₁).sum
⊢ ((x :: l₁).sigma l₂).length = (map (fun a => (l₂ a).length) (x :: l₁)).sum

Proof state:
case nil
α : Type u_2
σ : α → Type u_8
l₂ : (a : α) → List (σ a)
⊢ ([].sigma l₂).length = (map (fun a => (l₂ a).length) []).sum

Tactic:
rfl

Result:
no goals
-- Mathlib/Computability/AkraBazzi/AkraBazzi.lean
lemma tendsto_atTop_r (i : α) : Tendsto (r i) atTop atTop

Proof state:
α : Type u_1
inst✝¹ : Fintype α
T : ℕ → ℝ
g : ℝ → ℝ
a b✝ : α → ℝ
r : α → ℕ → ℕ
inst✝ : Nonempty α
R : AkraBazziRecurrence T g a b✝ r
i : α
b : ℕ
⊢ ∀ᶠ (a : ℕ) in atTop, b ≤ r i a

Tactic:
have := R.eventually_r_ge b

Result:
α : Type u_1
inst✝¹ : Fintype α
T : ℕ → ℝ
g : ℝ → ℝ
a b✝ : α → ℝ
r : α → ℕ → ℕ
inst✝ : Nonempty α
R : AkraBazziRecurrence T g a b✝ r
i : α
b : ℕ
this : ∀ᶠ (n : ℕ) in atTop, ∀ (i : α), ↑b ≤ ↑(r i n)
⊢ ∀ᶠ (a : ℕ) in atTop, b ≤ r i a

Proof state:
α : Type u_1
inst✝¹ : Fintype α
T : ℕ → ℝ
g : ℝ → ℝ
a b : α → ℝ
r : α → ℕ → ℕ
inst✝ : Nonempty α
R : AkraBazziRecurrence T g a b r
i : α
⊢ ∀ (b : ℕ), ∀ᶠ (a : ℕ) in atTop, b ≤ r i a

Tactic:
intro b

Result:
α : Type u_1
inst✝¹ : Fintype α
T : ℕ → ℝ
g : ℝ → ℝ
a b✝ : α → ℝ
r : α → ℕ → ℕ
inst✝ : Nonempty α
R : AkraBazziRecurrence T g a b✝ r
i : α
b : ℕ
⊢ ∀ᶠ (a : ℕ) in atTop, b ≤ r i a

Proof state:
α : Type u_1
inst✝¹ : Fintype α
T : ℕ → ℝ
g : ℝ → ℝ
a b : α → ℝ
r : α → ℕ → ℕ
inst✝ : Nonempty α
R : AkraBazziRecurrence T g a b r
i : α
⊢ Tendsto (r i) atTop atTop

Tactic:
rw [tendsto_atTop]

Result:
α : Type u_1
inst✝¹ : Fintype α
T : ℕ → ℝ
g : ℝ → ℝ
a b : α → ℝ
r : α → ℕ → ℕ
inst✝ : Nonempty α
R : AkraBazziRecurrence T g a b r
i : α
⊢ ∀ (b : ℕ), ∀ᶠ (a : ℕ) in atTop, b ≤ r i a

Proof state:
α : Type u_1
inst✝¹ : Fintype α
T : ℕ → ℝ
g : ℝ → ℝ
a b✝ : α → ℝ
r : α → ℕ → ℕ
inst✝ : Nonempty α
R : AkraBazziRecurrence T g a b✝ r
i : α
b : ℕ
this : ∀ (i : α), ∀ᶠ (x : ℕ) in atTop, ↑b ≤ ↑(r i x)
⊢ ∀ᶠ (a : ℕ) in atTop, b ≤ r i a

Tactic:
exact_mod_cast this i

Result:
no goals

Proof state:
α : Type u_1
inst✝¹ : Fintype α
T : ℕ → ℝ
g : ℝ → ℝ
a b✝ : α → ℝ
r : α → ℕ → ℕ
inst✝ : Nonempty α
R : AkraBazziRecurrence T g a b✝ r
i : α
b : ℕ
this : ∀ᶠ (n : ℕ) in atTop, ∀ (i : α), ↑b ≤ ↑(r i n)
⊢ ∀ᶠ (a : ℕ) in atTop, b ≤ r i a

Tactic:
rw [Filter.eventually_all] at this

Result:
α : Type u_1
inst✝¹ : Fintype α
T : ℕ → ℝ
g : ℝ → ℝ
a b✝ : α → ℝ
r : α → ℕ → ℕ
inst✝ : Nonempty α
R : AkraBazziRecurrence T g a b✝ r
i : α
b : ℕ
this : ∀ (i : α), ∀ᶠ (x : ℕ) in atTop, ↑b ≤ ↑(r i x)
⊢ ∀ᶠ (a : ℕ) in atTop, b ≤ r i a
-- Mathlib/LinearAlgebra/StdBasis.lean
theorem linearIndependent_single [Ring R] [∀ i, AddCommGroup (Ms i)] [∀ i, Module R (Ms i)]
    [DecidableEq η] (v : ∀ j, ιs j → Ms j) (hs : ∀ i, LinearIndependent R (v i)) :
    LinearIndependent R fun ji : Σj, ιs j ↦ Pi.single ji.1 (v ji.1 ji.2)

Proof state:
R : Type u_1
η : Type u_2
ιs : η → Type u_3
Ms : η → Type u_4
inst✝³ : Ring R
inst✝² : (i : η) → AddCommGroup (Ms i)
inst✝¹ : (i : η) → Module R (Ms i)
inst✝ : DecidableEq η
v : (j : η) → ιs j → Ms j
hs : ∀ (i : η), LinearIndependent R (v i)
hs' : ∀ (j : η), LinearIndependent R fun i => (LinearMap.single R Ms j) (v j i)
j✝ : η
J : Set η
a✝ : J.Finite
hiJ : j✝ ∉ J
j : η
⊢ (Set.range fun i => (LinearMap.single R Ms j) (v j i)) ⊆ Set.range ⇑(LinearMap.single R Ms j)

Tactic:
apply range_comp_subset_range

Result:
no goals

Proof state:
R : Type u_1
η : Type u_2
ιs : η → Type u_3
Ms : η → Type u_4
inst✝³ : Ring R
inst✝² : (i : η) → AddCommGroup (Ms i)
inst✝¹ : (i : η) → Module R (Ms i)
inst✝ : DecidableEq η
v : (j : η) → ιs j → Ms j
hs : ∀ (i : η), LinearIndependent R (v i)
hs' : ∀ (j : η), LinearIndependent R fun i => (LinearMap.single R Ms j) (v j i)
j✝ : η
J : Set η
a✝ : J.Finite
hiJ : j✝ ∉ J
j : η
⊢ span R (Set.range fun i => (LinearMap.single R Ms j) (v j i)) ≤ LinearMap.range (LinearMap.single R Ms j)

Tactic:
rw [span_le, LinearMap.range_coe]

Result:
R : Type u_1
η : Type u_2
ιs : η → Type u_3
Ms : η → Type u_4
inst✝³ : Ring R
inst✝² : (i : η) → AddCommGroup (Ms i)
inst✝¹ : (i : η) → Module R (Ms i)
inst✝ : DecidableEq η
v : (j : η) → ιs j → Ms j
hs : ∀ (i : η), LinearIndependent R (v i)
hs' : ∀ (j : η), LinearIndependent R fun i => (LinearMap.single R Ms j) (v j i)
j✝ : η
J : Set η
a✝ : J.Finite
hiJ : j✝ ∉ J
j : η
⊢ (Set.range fun i => (LinearMap.single R Ms j) (v j i)) ⊆ Set.range ⇑(LinearMap.single R Ms j)

Proof state:
R : Type u_1
η : Type u_2
ιs : η → Type u_3
Ms : η → Type u_4
inst✝³ : Ring R
inst✝² : (i : η) → AddCommGroup (Ms i)
inst✝¹ : (i : η) → Module R (Ms i)
inst✝ : DecidableEq η
v : (j : η) → ιs j → Ms j
hs : ∀ (i : η), LinearIndependent R (v i)
hs' : ∀ (j : η), LinearIndependent R fun i => (LinearMap.single R Ms j) (v j i)
⊢ LinearIndependent R fun ji => single ji.fst (v ji.fst ji.snd)

Tactic:
apply linearIndependent_iUnion_finite hs'

Result:
R : Type u_1
η : Type u_2
ιs : η → Type u_3
Ms : η → Type u_4
inst✝³ : Ring R
inst✝² : (i : η) → AddCommGroup (Ms i)
inst✝¹ : (i : η) → Module R (Ms i)
inst✝ : DecidableEq η
v : (j : η) → ιs j → Ms j
hs : ∀ (i : η), LinearIndependent R (v i)
hs' : ∀ (j : η), LinearIndependent R fun i => (LinearMap.single R Ms j) (v j i)
⊢ ∀ (i : η) (t : Set η),
    t.Finite →
      i ∉ t →
        Disjoint (span R (Set.range fun i_1 => (LinearMap.single R Ms i) (v i i_1)))
          (⨆ i ∈ t, span R (Set.range fun i_1 => (LinearMap.single R Ms i) (v i i_1)))