harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/GroupTheory/Sylow.lean
/-- A special case of **Sylow's first theorem**. If `G` is a `p`-group and `H` a subgroup of size at
least `p ^ n` then there is a subgroup of `H` of cardinality `p ^ n`. -/
lemma exists_subgroup_le_card_pow_prime_of_le_card {n p : ℕ} (hp : p.Prime) (h : IsPGroup p G)
    {H : Subgroup G} (hn : p ^ n ≤ Nat.card H) : ∃ H' ≤ H, Nat.card H' = p ^ n

Proof state:
G : Type u
inst✝ : Group G
n p : ℕ
hp : Nat.Prime p
h : IsPGroup p G
H : Subgroup G
hn : p ^ n ≤ Nat.card ↥H
⊢ ∃ H' ≤ H, Nat.card ↥H' = p ^ n

Tactic:
obtain ⟨H', H'card⟩ := exists_subgroup_card_pow_prime_of_le_card hp (h.to_subgroup H) hn

Result:
case intro
G : Type u
inst✝ : Group G
n p : ℕ
hp : Nat.Prime p
h : IsPGroup p G
H : Subgroup G
hn : p ^ n ≤ Nat.card ↥H
H' : Subgroup ↥H
H'card : Nat.card ↥H' = p ^ n
⊢ ∃ H' ≤ H, Nat.card ↥H' = p ^ n

Proof state:
case intro
G : Type u
inst✝ : Group G
n p : ℕ
hp : Nat.Prime p
h : IsPGroup p G
H : Subgroup G
hn : p ^ n ≤ Nat.card ↥H
H' : Subgroup ↥H
H'card : Nat.card ↥H' = p ^ n
⊢ Nat.card ↥(Subgroup.map H.subtype H') = Nat.card ↥H'

Tactic:
let e : H' ≃* H'.map H.subtype := H'.equivMapOfInjective (Subgroup.subtype H) H.subtype_injective

Result:
case intro
G : Type u
inst✝ : Group G
n p : ℕ
hp : Nat.Prime p
h : IsPGroup p G
H : Subgroup G
hn : p ^ n ≤ Nat.card ↥H
H' : Subgroup ↥H
H'card : Nat.card ↥H' = p ^ n
e : ↥H' ≃* ↥(Subgroup.map H.subtype H') := H'.equivMapOfInjective H.subtype ⋯
⊢ Nat.card ↥(Subgroup.map H.subtype H') = Nat.card ↥H'

Proof state:
case intro
G : Type u
inst✝ : Group G
n p : ℕ
hp : Nat.Prime p
h : IsPGroup p G
H : Subgroup G
hn : p ^ n ≤ Nat.card ↥H
H' : Subgroup ↥H
H'card : Nat.card ↥H' = p ^ n
⊢ Nat.card ↥(Subgroup.map H.subtype H') = p ^ n

Tactic:
rw [← H'card]

Result:
case intro
G : Type u
inst✝ : Group G
n p : ℕ
hp : Nat.Prime p
h : IsPGroup p G
H : Subgroup G
hn : p ^ n ≤ Nat.card ↥H
H' : Subgroup ↥H
H'card : Nat.card ↥H' = p ^ n
⊢ Nat.card ↥(Subgroup.map H.subtype H') = Nat.card ↥H'

Proof state:
case intro
G : Type u
inst✝ : Group G
n p : ℕ
hp : Nat.Prime p
h : IsPGroup p G
H : Subgroup G
hn : p ^ n ≤ Nat.card ↥H
H' : Subgroup ↥H
H'card : Nat.card ↥H' = p ^ n
⊢ ∃ H' ≤ H, Nat.card ↥H' = p ^ n

Tactic:
refine ⟨H'.map H.subtype, map_subtype_le _, ?_⟩

Result:
case intro
G : Type u
inst✝ : Group G
n p : ℕ
hp : Nat.Prime p
h : IsPGroup p G
H : Subgroup G
hn : p ^ n ≤ Nat.card ↥H
H' : Subgroup ↥H
H'card : Nat.card ↥H' = p ^ n
⊢ Nat.card ↥(Subgroup.map H.subtype H') = p ^ n

Proof state:
case intro
G : Type u
inst✝ : Group G
n p : ℕ
hp : Nat.Prime p
h : IsPGroup p G
H : Subgroup G
hn : p ^ n ≤ Nat.card ↥H
H' : Subgroup ↥H
H'card : Nat.card ↥H' = p ^ n
e : ↥H' ≃* ↥(Subgroup.map H.subtype H') := H'.equivMapOfInjective H.subtype ⋯
⊢ Nat.card ↥(Subgroup.map H.subtype H') = Nat.card ↥H'

Tactic:
exact Nat.card_congr e.symm.toEquiv

Result:
no goals
-- Mathlib/Data/Nat/Factorial/Basic.lean
theorem descFactorial_lt_pow {n : ℕ} (hn : 1 ≤ n) : ∀ {k : ℕ}, 2 ≤ k → n.descFactorial k < n ^ k
  | 0 => by rintro ⟨⟩
  | 1 => by intro; contradiction
  | k + 2 => fun _ => by
    rw [descFactorial_succ, pow_succ', Nat.mul_comm, Nat.mul_comm n]
    exact Nat.mul_lt_mul_of_le_of_lt (descFactorial_le_pow _ _) (Nat.sub_lt hn k.zero_lt_succ)
      (Nat.pow_pos (Nat.lt_of_succ_le hn))

Proof state:
n : ℕ
hn : 1 ≤ n
k : ℕ
x✝ : 2 ≤ k + 2
⊢ n.descFactorial (k + 1) * (n - (k + 1)) < n ^ (k + 1) * n

Tactic:
exact Nat.mul_lt_mul_of_le_of_lt (descFactorial_le_pow _ _) (Nat.sub_lt hn k.zero_lt_succ)
  (Nat.pow_pos (Nat.lt_of_succ_le hn))

Result:
no goals

Proof state:
n : ℕ
hn : 1 ≤ n
k : ℕ
x✝ : 2 ≤ k + 2
⊢ n.descFactorial (k + 2) < n ^ (k + 2)

Tactic:
rw [descFactorial_succ, pow_succ', Nat.mul_comm, Nat.mul_comm n]

Result:
n : ℕ
hn : 1 ≤ n
k : ℕ
x✝ : 2 ≤ k + 2
⊢ n.descFactorial (k + 1) * (n - (k + 1)) < n ^ (k + 1) * n

Proof state:
n : ℕ
hn : 1 ≤ n
a✝ : 2 ≤ 1
⊢ n.descFactorial 1 < n ^ 1

Tactic:
contradiction

Result:
no goals

Proof state:
n : ℕ
hn : 1 ≤ n
⊢ 2 ≤ 0 → n.descFactorial 0 < n ^ 0

Tactic:
rintro ⟨⟩

Result:
no goals

Proof state:
n : ℕ
hn : 1 ≤ n
⊢ 2 ≤ 1 → n.descFactorial 1 < n ^ 1

Tactic:
intro

Result:
n : ℕ
hn : 1 ≤ n
a✝ : 2 ≤ 1
⊢ n.descFactorial 1 < n ^ 1
-- Mathlib/Probability/Moments/IntegrableExpMul.lean
/-- If `ω ↦ exp (t * X ω)` is integrable at `t` and `-t` for `t ≠ 0`, then `ω ↦ X ω ^ n` is
integrable for all `n : ℕ`. -/
lemma integrable_pow_of_integrable_exp_mul (ht : t ≠ 0)
    (ht_int_pos : Integrable (fun ω ↦ exp (t * X ω)) μ)
    (ht_int_neg : Integrable (fun ω ↦ exp (- t * X ω)) μ) (n : ℕ) :
    Integrable (fun ω ↦ X ω ^ n) μ

Proof state:
Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
t : ℝ
ht : t ≠ 0
ht_int_pos : Integrable (fun ω => rexp (t * X ω)) μ
ht_int_neg : Integrable (fun ω => rexp (-t * X ω)) μ
n : ℕ
⊢ Integrable (fun ω => X ω ^ n) μ

Tactic:
convert integrable_rpow_of_integrable_exp_mul ht ht_int_pos ht_int_neg
  (by positivity : 0 ≤ (n : ℝ)) with ω

Result:
case h.e'_6.h
Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
t : ℝ
ht : t ≠ 0
ht_int_pos : Integrable (fun ω => rexp (t * X ω)) μ
ht_int_neg : Integrable (fun ω => rexp (-t * X ω)) μ
n : ℕ
ω : Ω
⊢ X ω ^ n = X ω ^ ↑n

Proof state:
case h.e'_6.h
Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
t : ℝ
ht : t ≠ 0
ht_int_pos : Integrable (fun ω => rexp (t * X ω)) μ
ht_int_neg : Integrable (fun ω => rexp (-t * X ω)) μ
n : ℕ
ω : Ω
⊢ X ω ^ n = X ω ^ ↑n

Tactic:
simp

Result:
no goals

Proof state:
Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
t : ℝ
ht : t ≠ 0
ht_int_pos : Integrable (fun ω => rexp (t * X ω)) μ
ht_int_neg : Integrable (fun ω => rexp (-t * X ω)) μ
n : ℕ
⊢ 0 ≤ ↑n

Tactic:
positivity

Result:
no goals
-- Mathlib/GroupTheory/Perm/Cycle/Type.lean
theorem isThreeCycle_sq {g : Perm α} (ht : IsThreeCycle g) : IsThreeCycle (g * g)

Proof state:
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
g : Perm α
ht : g.IsThreeCycle
⊢ (g * g).IsThreeCycle

Tactic:
rw [← pow_two, ← card_support_eq_three_iff, support_pow_coprime, ht.card_support]

Result:
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
g : Perm α
ht : g.IsThreeCycle
⊢ Nat.Coprime 2 (_root_.orderOf g)

Proof state:
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
g : Perm α
ht : g.IsThreeCycle
⊢ Nat.Coprime 2 (_root_.orderOf g)

Tactic:
rw [ht.orderOf]

Result:
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
g : Perm α
ht : g.IsThreeCycle
⊢ Nat.Coprime 2 3

Proof state:
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
g : Perm α
ht : g.IsThreeCycle
⊢ Nat.Coprime 2 3

Tactic:
norm_num

Result:
no goals
-- Mathlib/Topology/MetricSpace/Infsep.lean
theorem einfsep_ne_top :
    s.einfsep ≠ ∞ ↔ ∃ x ∈ s, ∃ y ∈ s, x ≠ y ∧ edist x y ≠ ∞

Proof state:
α : Type u_1
inst✝ : EDist α
s : Set α
⊢ s.einfsep ≠ ⊤ ↔ ∃ x ∈ s, ∃ y ∈ s, x ≠ y ∧ edist x y ≠ ⊤

Tactic:
simp_rw [← lt_top_iff_ne_top, einfsep_lt_top]

Result:
no goals
-- Mathlib/Data/Complex/Exponential.lean
theorem add_one_lt_exp {x : ℝ} (hx : x ≠ 0) : x + 1 < Real.exp x

Proof state:
x : ℝ
hx✝ : x ≠ 0
hx : x < 0
h' : -x < 1
⊢ 0 < x + 1

Tactic:
linarith

Result:
no goals

Proof state:
x : ℝ
hx : x ≠ 0
⊢ x + 1 < rexp x

Tactic:
obtain hx | hx := hx.symm.lt_or_lt

Result:
case inl
x : ℝ
hx✝ : x ≠ 0
hx : 0 < x
⊢ x + 1 < rexp x

case inr
x : ℝ
hx✝ : x ≠ 0
hx : x < 0
⊢ x + 1 < rexp x

Proof state:
case inr
x : ℝ
hx✝ : x ≠ 0
hx : x < 0
⊢ x + 1 < rexp x

Tactic:
obtain h' | h' := le_or_lt 1 (-x)

Result:
case inr.inl
x : ℝ
hx✝ : x ≠ 0
hx : x < 0
h' : 1 ≤ -x
⊢ x + 1 < rexp x

case inr.inr
x : ℝ
hx✝ : x ≠ 0
hx : x < 0
h' : -x < 1
⊢ x + 1 < rexp x

Proof state:
case inr.inl
x : ℝ
hx✝ : x ≠ 0
hx : x < 0
h' : 1 ≤ -x
⊢ x + 1 < rexp x

Tactic:
linarith [x.exp_pos]

Result:
no goals

Proof state:
case inl
x : ℝ
hx✝ : x ≠ 0
hx : 0 < x
⊢ x + 1 < rexp x

Tactic:
exact add_one_lt_exp_of_pos hx

Result:
no goals

Proof state:
case inr.inr
x : ℝ
hx✝ : x ≠ 0
hx : x < 0
h' : -x < 1
hx' : 0 < x + 1
⊢ x + 1 < rexp x

Tactic:
simpa [add_comm, exp_neg, inv_lt_inv₀ (exp_pos _) hx']
  using exp_bound_div_one_sub_of_interval' (neg_pos.2 hx) h'

Result:
no goals

Proof state:
case inr.inr
x : ℝ
hx✝ : x ≠ 0
hx : x < 0
h' : -x < 1
⊢ x + 1 < rexp x

Tactic:
have hx' : 0 < x + 1 := by linarith

Result:
case inr.inr
x : ℝ
hx✝ : x ≠ 0
hx : x < 0
h' : -x < 1
hx' : 0 < x + 1
⊢ x + 1 < rexp x
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Int/Lemmas.lean
theorem add_left_inj {i j : Int} (k : Int) : (i + k = j + k) ↔ i = j

Proof state:
case mp
i j k : Int
⊢ i + k = j + k → i = j

Tactic:
intro p

Result:
case mp
i j k : Int
p : i + k = j + k
⊢ i = j

Proof state:
case mp
i j k : Int
p : i + k = j + k
⊢ i = j

Tactic:
rw [←Int.add_sub_cancel i k, ←Int.add_sub_cancel j k, p]

Result:
no goals

Proof state:
i j k : Int
⊢ i + k = j + k ↔ i = j

Tactic:
apply Iff.intro

Result:
case mp
i j k : Int
⊢ i + k = j + k → i = j

case mpr
i j k : Int
⊢ i = j → i + k = j + k
-- Mathlib/Data/Complex/Exponential.lean
theorem exp_add : exp (x + y) = exp x * exp y

Proof state:
x y : ℂ
j m : ℕ
x✝ : m ∈ range j
I : ℕ
hi : I ∈ range (m + 1)
h₁ : ↑(m.choose I) ≠ 0
h₂ : m.choose I * I.factorial * (m - I).factorial = m.factorial
⊢ x ^ I * (y ^ (m - I) * ((↑I.factorial)⁻¹ * ((↑(m - I).factorial)⁻¹ * ((↑(m.choose I))⁻¹ * ↑(m.choose I))))) =
    x ^ I / ↑I.factorial * (y ^ (m - I) / ↑(m - I).factorial)

Tactic:
rw [inv_mul_cancel₀ h₁]

Result:
x y : ℂ
j m : ℕ
x✝ : m ∈ range j
I : ℕ
hi : I ∈ range (m + 1)
h₁ : ↑(m.choose I) ≠ 0
h₂ : m.choose I * I.factorial * (m - I).factorial = m.factorial
⊢ x ^ I * (y ^ (m - I) * ((↑I.factorial)⁻¹ * ((↑(m - I).factorial)⁻¹ * 1))) =
    x ^ I / ↑I.factorial * (y ^ (m - I) / ↑(m - I).factorial)

Proof state:
x y : ℂ
hj :
  ∀ (j : ℕ),
    ∑ m ∈ range j, (x + y) ^ m / ↑m.factorial =
      ∑ i ∈ range j, ∑ k ∈ range (i + 1), x ^ k / ↑k.factorial * (y ^ (i - k) / ↑(i - k).factorial)
⊢ ⟨fun n => ∑ m ∈ range n, x ^ m / ↑m.factorial, ⋯⟩ * ⟨fun n => ∑ m ∈ range n, y ^ m / ↑m.factorial, ⋯⟩ ≈
    ⟨fun n => ∑ i ∈ range n, ∑ k ∈ range (i + 1), x ^ k / ↑k.factorial * (y ^ (i - k) / ↑(i - k).factorial), ⋯⟩

Tactic:
exact cauchy_product (isCauSeq_norm_exp x) (isCauSeq_exp y)

Result:
no goals
-- Mathlib/GroupTheory/CoprodI.lean
theorem lift_word_ping_pong {i j k} (w : NeWord H i j) (hk : j ≠ k) :
    lift f w.prod • X k ⊆ X i

Proof state:
ι : Type u_1
G : Type u_4
inst✝² : Group G
H : ι → Type u_5
inst✝¹ : (i : ι) → Group (H i)
f : (i : ι) → H i →* G
α : Type u_6
inst✝ : MulAction G α
X : ι → Set α
hpp : Pairwise fun i j => ∀ (h : H i), h ≠ 1 → (f i) h • X j ⊆ X i
i✝ j✝ i j k✝ l : ι
w₁ : NeWord H i j
hne : j ≠ k✝
w₂ : NeWord H k✝ l
hIw₁ : ∀ {k : ι}, j ≠ k → (lift f) w₁.prod • X k ⊆ X i
hIw₂ : ∀ {k : ι}, l ≠ k → (lift f) w₂.prod • X k ⊆ X k✝
k : ι
hk : l ≠ k
⊢ (lift f) (w₁.append hne w₂).prod • X k = (lift f) w₁.prod • (lift f) w₂.prod • X k

Tactic:
simp [MulAction.mul_smul]

Result:
no goals

Proof state:
ι : Type u_1
G : Type u_4
inst✝² : Group G
H : ι → Type u_5
inst✝¹ : (i : ι) → Group (H i)
f : (i : ι) → H i →* G
α : Type u_6
inst✝ : MulAction G α
X : ι → Set α
hpp : Pairwise fun i j => ∀ (h : H i), h ≠ 1 → (f i) h • X j ⊆ X i
i j k : ι
w : NeWord H i j
hk : j ≠ k
⊢ (lift f) w.prod • X k ⊆ X i

Tactic:
induction' w with i x hne_one i j k l w₁ hne w₂ hIw₁ hIw₂ generalizing k

Result:
case singleton
ι : Type u_1
G : Type u_4
inst✝² : Group G
H : ι → Type u_5
inst✝¹ : (i : ι) → Group (H i)
f : (i : ι) → H i →* G
α : Type u_6
inst✝ : MulAction G α
X : ι → Set α
hpp : Pairwise fun i j => ∀ (h : H i), h ≠ 1 → (f i) h • X j ⊆ X i
i✝ j i : ι
x : H i
hne_one : x ≠ 1
k : ι
hk : i ≠ k
⊢ (lift f) (NeWord.singleton x hne_one).prod • X k ⊆ X i

case append
ι : Type u_1
G : Type u_4
inst✝² : Group G
H : ι → Type u_5
inst✝¹ : (i : ι) → Group (H i)
f : (i : ι) → H i →* G
α : Type u_6
inst✝ : MulAction G α
X : ι → Set α
hpp : Pairwise fun i j => ∀ (h : H i), h ≠ 1 → (f i) h • X j ⊆ X i
i✝ j✝ i j k✝ l : ι
w₁ : NeWord H i j
hne : j ≠ k✝
w₂ : NeWord H k✝ l
hIw₁ : ∀ {k : ι}, j ≠ k → (lift f) w₁.prod • X k ⊆ X i
hIw₂ : ∀ {k : ι}, l ≠ k → (lift f) w₂.prod • X k ⊆ X k✝
k : ι
hk : l ≠ k
⊢ (lift f) (w₁.append hne w₂).prod • X k ⊆ X i

Proof state:
case singleton
ι : Type u_1
G : Type u_4
inst✝² : Group G
H : ι → Type u_5
inst✝¹ : (i : ι) → Group (H i)
f : (i : ι) → H i →* G
α : Type u_6
inst✝ : MulAction G α
X : ι → Set α
hpp : Pairwise fun i j => ∀ (h : H i), h ≠ 1 → (f i) h • X j ⊆ X i
i✝ j i : ι
x : H i
hne_one : x ≠ 1
k : ι
hk : i ≠ k
⊢ (lift f) (NeWord.singleton x hne_one).prod • X k ⊆ X i

Tactic:
simpa using hpp hk _ hne_one

Result:
no goals

Proof state:
case append
ι : Type u_1
G : Type u_4
inst✝² : Group G
H : ι → Type u_5
inst✝¹ : (i : ι) → Group (H i)
f : (i : ι) → H i →* G
α : Type u_6
inst✝ : MulAction G α
X : ι → Set α
hpp : Pairwise fun i j => ∀ (h : H i), h ≠ 1 → (f i) h • X j ⊆ X i
i✝ j✝ i j k✝ l : ι
w₁ : NeWord H i j
hne : j ≠ k✝
w₂ : NeWord H k✝ l
hIw₁ : ∀ {k : ι}, j ≠ k → (lift f) w₁.prod • X k ⊆ X i
hIw₂ : ∀ {k : ι}, l ≠ k → (lift f) w₂.prod • X k ⊆ X k✝
k : ι
hk : l ≠ k
⊢ (lift f) (w₁.append hne w₂).prod • X k ⊆ X i

Tactic:
calc
  lift f (NeWord.append w₁ hne w₂).prod • X k = lift f w₁.prod • lift f w₂.prod • X k := by
    simp [MulAction.mul_smul]
  _ ⊆ lift f w₁.prod • X _ := smul_set_subset_smul_set_iff.mpr (hIw₂ hk)
  _ ⊆ X i := hIw₁ hne

Result:
no goals
-- Mathlib/MeasureTheory/Integral/BochnerL1.lean
theorem continuous_integral : Continuous fun f : α →₁[μ] E => integral f

Proof state:
α : Type u_1
E : Type u_2
inst✝² : NormedAddCommGroup E
m : MeasurableSpace α
μ : Measure α
inst✝¹ : NormedSpace ℝ E
inst✝ : CompleteSpace E
⊢ Continuous fun f => integralCLM f

Tactic:
exact L1.integralCLM.continuous

Result:
no goals

Proof state:
α : Type u_1
E : Type u_2
inst✝² : NormedAddCommGroup E
m : MeasurableSpace α
μ : Measure α
inst✝¹ : NormedSpace ℝ E
inst✝ : CompleteSpace E
⊢ Continuous fun f => integral f

Tactic:
simp only [integral]

Result:
α : Type u_1
E : Type u_2
inst✝² : NormedAddCommGroup E
m : MeasurableSpace α
μ : Measure α
inst✝¹ : NormedSpace ℝ E
inst✝ : CompleteSpace E
⊢ Continuous fun f => integralCLM f
-- Mathlib/Topology/Compactness/Lindelof.lean
theorem Set.Finite.isLindelof_sUnion {S : Set (Set X)} (hf : S.Finite)
    (hc : ∀ s ∈ S, IsLindelof s) : IsLindelof (⋃₀ S)

Proof state:
X : Type u
inst✝ : TopologicalSpace X
S : Set (Set X)
hf : S.Finite
hc : ∀ s ∈ S, IsLindelof s
⊢ IsLindelof (⋃₀ S)

Tactic:
rw [sUnion_eq_biUnion]

Result:
X : Type u
inst✝ : TopologicalSpace X
S : Set (Set X)
hf : S.Finite
hc : ∀ s ∈ S, IsLindelof s
⊢ IsLindelof (⋃ i ∈ S, i)

Proof state:
X : Type u
inst✝ : TopologicalSpace X
S : Set (Set X)
hf : S.Finite
hc : ∀ s ∈ S, IsLindelof s
⊢ IsLindelof (⋃ i ∈ S, i)

Tactic:
exact hf.isLindelof_biUnion hc

Result:
no goals
-- Mathlib/Topology/Algebra/Group/Basic.lean
theorem Specializes.zpow {G : Type*} [DivInvMonoid G] [TopologicalSpace G]
    [ContinuousMul G] [ContinuousInv G] {x y : G} (h : x ⤳ y) : ∀ m : ℤ, (x ^ m) ⤳ (y ^ m)
  | .ofNat n => by simpa using h.pow n
  | .negSucc n => by simpa using (h.pow (n + 1)).inv

Proof state:
G : Type u_1
inst✝³ : DivInvMonoid G
inst✝² : TopologicalSpace G
inst✝¹ : ContinuousMul G
inst✝ : ContinuousInv G
x y : G
h : x ⤳ y
n : ℕ
⊢ (x ^ Int.negSucc n) ⤳ (y ^ Int.negSucc n)

Tactic:
simpa using (h.pow (n + 1)).inv

Result:
no goals

Proof state:
G : Type u_1
inst✝³ : DivInvMonoid G
inst✝² : TopologicalSpace G
inst✝¹ : ContinuousMul G
inst✝ : ContinuousInv G
x y : G
h : x ⤳ y
n : ℕ
⊢ (x ^ Int.ofNat n) ⤳ (y ^ Int.ofNat n)

Tactic:
simpa using h.pow n

Result:
no goals
-- Mathlib/Topology/MetricSpace/Completion.lean
theorem uniformity_dist' :
    𝓤 (Completion α) = ⨅ ε : { ε : ℝ // 0 < ε }, 𝓟 { p | dist p.1 p.2 < ε.val }

Proof state:
case h
α : Type u
inst✝ : PseudoMetricSpace α
s : Set (Completion α × Completion α)
⊢ s ∈ 𝓤 (Completion α) ↔ s ∈ ⨅ ε, 𝓟 {p | dist p.1 p.2 < ↑ε}

Tactic:
rw [mem_iInf_of_directed]

Result:
case h
α : Type u
inst✝ : PseudoMetricSpace α
s : Set (Completion α × Completion α)
⊢ s ∈ 𝓤 (Completion α) ↔ ∃ i, s ∈ 𝓟 {p | dist p.1 p.2 < ↑i}

case h.h
α : Type u
inst✝ : PseudoMetricSpace α
s : Set (Completion α × Completion α)
⊢ Directed (fun x1 x2 => x1 ≥ x2) fun ε => 𝓟 {p | dist p.1 p.2 < ↑ε}

Proof state:
case h.h.mk.mk
α : Type u
inst✝ : PseudoMetricSpace α
s : Set (Completion α × Completion α)
r : ℝ
hr : 0 < r
p : ℝ
hp : 0 < p
⊢ ∃ z,
    (fun x1 x2 => x1 ≥ x2) ((fun ε => 𝓟 {p | dist p.1 p.2 < ↑ε}) ⟨r, hr⟩) ((fun ε => 𝓟 {p | dist p.1 p.2 < ↑ε}) z) ∧
      (fun x1 x2 => x1 ≥ x2) ((fun ε => 𝓟 {p | dist p.1 p.2 < ↑ε}) ⟨p, hp⟩) ((fun ε => 𝓟 {p | dist p.1 p.2 < ↑ε}) z)

Tactic:
use ⟨min r p, lt_min hr hp⟩

Result:
case h
α : Type u
inst✝ : PseudoMetricSpace α
s : Set (Completion α × Completion α)
r : ℝ
hr : 0 < r
p : ℝ
hp : 0 < p
⊢ (fun x1 x2 => x1 ≥ x2) ((fun ε => 𝓟 {p | dist p.1 p.2 < ↑ε}) ⟨r, hr⟩)
      ((fun ε => 𝓟 {p | dist p.1 p.2 < ↑ε}) ⟨r ⊓ p, ⋯⟩) ∧
    (fun x1 x2 => x1 ≥ x2) ((fun ε => 𝓟 {p | dist p.1 p.2 < ↑ε}) ⟨p, hp⟩)
      ((fun ε => 𝓟 {p | dist p.1 p.2 < ↑ε}) ⟨r ⊓ p, ⋯⟩)

Proof state:
α : Type u
inst✝ : PseudoMetricSpace α
⊢ 𝓤 (Completion α) = ⨅ ε, 𝓟 {p | dist p.1 p.2 < ↑ε}

Tactic:
ext s

Result:
case h
α : Type u
inst✝ : PseudoMetricSpace α
s : Set (Completion α × Completion α)
⊢ s ∈ 𝓤 (Completion α) ↔ s ∈ ⨅ ε, 𝓟 {p | dist p.1 p.2 < ↑ε}

Proof state:
case h
α : Type u
inst✝ : PseudoMetricSpace α
s : Set (Completion α × Completion α)
⊢ s ∈ 𝓤 (Completion α) ↔ ∃ i, s ∈ 𝓟 {p | dist p.1 p.2 < ↑i}

Tactic:
simp [Completion.mem_uniformity_dist, subset_def]

Result:
no goals

Proof state:
case h
α : Type u
inst✝ : PseudoMetricSpace α
s : Set (Completion α × Completion α)
r : ℝ
hr : 0 < r
p : ℝ
hp : 0 < p
⊢ (fun x1 x2 => x1 ≥ x2) ((fun ε => 𝓟 {p | dist p.1 p.2 < ↑ε}) ⟨r, hr⟩)
      ((fun ε => 𝓟 {p | dist p.1 p.2 < ↑ε}) ⟨r ⊓ p, ⋯⟩) ∧
    (fun x1 x2 => x1 ≥ x2) ((fun ε => 𝓟 {p | dist p.1 p.2 < ↑ε}) ⟨p, hp⟩)
      ((fun ε => 𝓟 {p | dist p.1 p.2 < ↑ε}) ⟨r ⊓ p, ⋯⟩)

Tactic:
simp +contextual [lt_min_iff]

Result:
no goals

Proof state:
case h.h
α : Type u
inst✝ : PseudoMetricSpace α
s : Set (Completion α × Completion α)
⊢ Directed (fun x1 x2 => x1 ≥ x2) fun ε => 𝓟 {p | dist p.1 p.2 < ↑ε}

Tactic:
rintro ⟨r, hr⟩ ⟨p, hp⟩

Result:
case h.h.mk.mk
α : Type u
inst✝ : PseudoMetricSpace α
s : Set (Completion α × Completion α)
r : ℝ
hr : 0 < r
p : ℝ
hp : 0 < p
⊢ ∃ z,
    (fun x1 x2 => x1 ≥ x2) ((fun ε => 𝓟 {p | dist p.1 p.2 < ↑ε}) ⟨r, hr⟩) ((fun ε => 𝓟 {p | dist p.1 p.2 < ↑ε}) z) ∧
      (fun x1 x2 => x1 ≥ x2) ((fun ε => 𝓟 {p | dist p.1 p.2 < ↑ε}) ⟨p, hp⟩) ((fun ε => 𝓟 {p | dist p.1 p.2 < ↑ε}) z)
-- Mathlib/Data/Fin/VecNotation.lean
theorem cons_vecAlt1 (h : m + 1 + 1 = n + 1 + (n + 1)) (x y : α) (u : Fin m → α) :
    vecAlt1 h (vecCons x (vecCons y u)) = vecCons y (vecAlt1 (by omega) u)

Proof state:
case h
α : Type u
m n : ℕ
h : m + 1 + 1 = n + 1 + (n + 1)
x y : α
u : Fin m → α
i : Fin (n + 1)
⊢ vecAlt1 h (vecCons x (vecCons y u)) i = vecCons y (vecAlt1 ⋯ u) i

Tactic:
simp_rw [vecAlt1]

Result:
case h
α : Type u
m n : ℕ
h : m + 1 + 1 = n + 1 + (n + 1)
x y : α
u : Fin m → α
i : Fin (n + 1)
⊢ vecCons x (vecCons y u) ⟨↑i + ↑i + 1, ⋯⟩ = vecCons y (vecAlt1 ⋯ u) i

Proof state:
α : Type u
m n o : ℕ
h : m + 1 + 1 = n + 1 + (n + 1)
x y : α
u : Fin m → α
⊢ m = n + n

Tactic:
omega

Result:
no goals

Proof state:
case h
α : Type u
m n : ℕ
h : m + 1 + 1 = n + 1 + (n + 1)
x y : α
u : Fin m → α
i : Fin (n + 1)
⊢ vecCons x (vecCons y u) ⟨↑i + ↑i + 1, ⋯⟩ = vecCons y (vecAlt1 ⋯ u) i

Tactic:
rcases i with ⟨⟨⟩ | i, hi⟩

Result:
case h.mk.zero
α : Type u
m n : ℕ
h : m + 1 + 1 = n + 1 + (n + 1)
x y : α
u : Fin m → α
hi : 0 < n + 1
⊢ vecCons x (vecCons y u) ⟨↑⟨0, hi⟩ + ↑⟨0, hi⟩ + 1, ⋯⟩ = vecCons y (vecAlt1 ⋯ u) ⟨0, hi⟩

case h.mk.succ
α : Type u
m n : ℕ
h : m + 1 + 1 = n + 1 + (n + 1)
x y : α
u : Fin m → α
i : ℕ
hi : i + 1 < n + 1
⊢ vecCons x (vecCons y u) ⟨↑⟨i + 1, hi⟩ + ↑⟨i + 1, hi⟩ + 1, ⋯⟩ = vecCons y (vecAlt1 ⋯ u) ⟨i + 1, hi⟩

Proof state:
case h.mk.succ
α : Type u
m n : ℕ
h : m + 1 + 1 = n + 1 + (n + 1)
x y : α
u : Fin m → α
i : ℕ
hi : i + 1 < n + 1
⊢ vecCons x (vecCons y u) ⟨↑⟨i + 1, hi⟩ + ↑⟨i + 1, hi⟩ + 1, ⋯⟩ = vecCons y (vecAlt1 ⋯ u) ⟨i + 1, hi⟩

Tactic:
simp [vecAlt1, Nat.add_right_comm, ← Nat.add_assoc]

Result:
no goals

Proof state:
case h.mk.zero
α : Type u
m n : ℕ
h : m + 1 + 1 = n + 1 + (n + 1)
x y : α
u : Fin m → α
hi : 0 < n + 1
⊢ vecCons x (vecCons y u) ⟨↑⟨0, hi⟩ + ↑⟨0, hi⟩ + 1, ⋯⟩ = vecCons y (vecAlt1 ⋯ u) ⟨0, hi⟩

Tactic:
rfl

Result:
no goals

Proof state:
α : Type u
m n : ℕ
h : m + 1 + 1 = n + 1 + (n + 1)
x y : α
u : Fin m → α
⊢ vecAlt1 h (vecCons x (vecCons y u)) = vecCons y (vecAlt1 ⋯ u)

Tactic:
ext i

Result:
case h
α : Type u
m n : ℕ
h : m + 1 + 1 = n + 1 + (n + 1)
x y : α
u : Fin m → α
i : Fin (n + 1)
⊢ vecAlt1 h (vecCons x (vecCons y u)) i = vecCons y (vecAlt1 ⋯ u) i
-- Mathlib/Algebra/GeomSum.lean
theorem Commute.geom_sum₂_mul_add {x y : α} (h : Commute x y) (n : ℕ) :
    (∑ i ∈ range n, (x + y) ^ i * y ^ (n - 1 - i)) * x + y ^ n = (x + y) ^ n

Proof state:
α : Type u
inst✝ : Semiring α
x y : α
h : Commute x y
f : ℕ → ℕ → α := fun m i => (x + y) ^ i * y ^ (m - 1 - i)
n : ℕ
ih : (∑ i ∈ range n, f n i) * x + y ^ n = (x + y) ^ n
f_last : f (n + 1) n = (x + y) ^ n
i : ℕ
hi : i ∈ range n
this✝ : Commute y ((x + y) ^ i)
this : i + 1 + (n - (i + 1)) = n
⊢ (x + y) ^ i * y ^ (n - i) = (x + y) ^ i * y ^ (n - (i + 1) + 1)

Tactic:
rw [add_comm (i + 1)] at this

Result:
α : Type u
inst✝ : Semiring α
x y : α
h : Commute x y
f : ℕ → ℕ → α := fun m i => (x + y) ^ i * y ^ (m - 1 - i)
n : ℕ
ih : (∑ i ∈ range n, f n i) * x + y ^ n = (x + y) ^ n
f_last : f (n + 1) n = (x + y) ^ n
i : ℕ
hi : i ∈ range n
this✝ : Commute y ((x + y) ^ i)
this : n - (i + 1) + (i + 1) = n
⊢ (x + y) ^ i * y ^ (n - i) = (x + y) ^ i * y ^ (n - (i + 1) + 1)

Proof state:
case zero
α : Type u
inst✝ : Semiring α
x y : α
h : Commute x y
f : ℕ → ℕ → α := fun m i => (x + y) ^ i * y ^ (m - 1 - i)
⊢ (∑ i ∈ range 0, f 0 i) * x + y ^ 0 = (x + y) ^ 0

Tactic:
rw [range_zero, sum_empty, zero_mul, zero_add, pow_zero, pow_zero]

Result:
no goals

Proof state:
α : Type u
inst✝ : Semiring α
x y : α
h : Commute x y
f : ℕ → ℕ → α := fun m i => (x + y) ^ i * y ^ (m - 1 - i)
n : ℕ
ih : (∑ i ∈ range n, f n i) * x + y ^ n = (x + y) ^ n
f_last : f (n + 1) n = (x + y) ^ n
i : ℕ
hi : i ∈ range n
this✝ : Commute y ((x + y) ^ i)
this : n - (i + 1) + (i + 1) = n
⊢ (x + y) ^ i * y ^ (n - i) = (x + y) ^ i * y ^ (n - (i + 1) + 1)

Tactic:
rw [← this, add_tsub_cancel_right, add_comm i 1, ← add_assoc, add_tsub_cancel_right]

Result:
no goals

Proof state:
case succ
α : Type u
inst✝ : Semiring α
x y : α
h : Commute x y
f : ℕ → ℕ → α := fun m i => (x + y) ^ i * y ^ (m - 1 - i)
n : ℕ
ih : (∑ i ∈ range n, f n i) * x + y ^ n = (x + y) ^ n
f_last : f (n + 1) n = (x + y) ^ n
f_succ : ∀ i ∈ range n, f (n + 1) i = y * f n i
⊢ (∑ i ∈ range (n + 1), f (n + 1) i) * x + y ^ (n + 1) = (x + y) ^ (n + 1)

Tactic:
rw [pow_succ' (x + y), add_mul, sum_range_succ_comm, add_mul, f_last, add_assoc,
  (((Commute.refl x).add_right h).pow_right n).eq, sum_congr rfl f_succ, ← mul_sum,
  pow_succ' y, mul_assoc, ← mul_add y, ih]

Result:
no goals
-- Mathlib/MeasureTheory/Measure/MeasureSpace.lean
theorem measure_eq_right_of_subset_of_measure_add_eq {s t : Set α} (h : (μ + ν) t ≠ ∞) (h' : s ⊆ t)
    (h'' : (μ + ν) s = (μ + ν) t) : ν s = ν t

Proof state:
α : Type u_1
m0 : MeasurableSpace α
μ ν : Measure α
s t : Set α
h : (μ + ν) t ≠ ⊤
h' : s ⊆ t
h'' : (μ + ν) s = (μ + ν) t
⊢ ν s = ν t

Tactic:
rw [add_comm] at h'' h

Result:
α : Type u_1
m0 : MeasurableSpace α
μ ν : Measure α
s t : Set α
h : (ν + μ) t ≠ ⊤
h' : s ⊆ t
h'' : (ν + μ) s = (ν + μ) t
⊢ ν s = ν t

Proof state:
α : Type u_1
m0 : MeasurableSpace α
μ ν : Measure α
s t : Set α
h : (ν + μ) t ≠ ⊤
h' : s ⊆ t
h'' : (ν + μ) s = (ν + μ) t
⊢ ν s = ν t

Tactic:
exact measure_eq_left_of_subset_of_measure_add_eq h h' h''

Result:
no goals