harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/Combinatorics/SimpleGraph/Path.lean
lemma iUnion_connectedComponentSupp (G : SimpleGraph V) :
    ⋃ c : G.ConnectedComponent, c.supp = Set.univ

Proof state:
V : Type u
G : SimpleGraph V
v : V
⊢ (↑(G.connectedComponentMk v) ∈ Set.range fun c => c.supp) ∧ v ∈ ↑(G.connectedComponentMk v)

Tactic:
simp only [Set.mem_range, SetLike.mem_coe]

Result:
V : Type u
G : SimpleGraph V
v : V
⊢ (∃ y, y.supp = ↑(G.connectedComponentMk v)) ∧ v ∈ G.connectedComponentMk v

Proof state:
V : Type u
G : SimpleGraph V
⊢ ⋃ c, c.supp = Set.univ

Tactic:
refine Set.eq_univ_of_forall fun v ↦ ⟨G.connectedComponentMk v, ?_⟩

Result:
V : Type u
G : SimpleGraph V
v : V
⊢ (↑(G.connectedComponentMk v) ∈ Set.range fun c => c.supp) ∧ v ∈ ↑(G.connectedComponentMk v)

Proof state:
case h
V : Type u
G : SimpleGraph V
v : V
⊢ (G.connectedComponentMk v).supp = ↑(G.connectedComponentMk v)

Tactic:
exact rfl

Result:
no goals

Proof state:
V : Type u
G : SimpleGraph V
v : V
⊢ (∃ y, y.supp = ↑(G.connectedComponentMk v)) ∧ v ∈ G.connectedComponentMk v

Tactic:
exact ⟨by use G.connectedComponentMk v; exact rfl, rfl⟩

Result:
no goals

Proof state:
V : Type u
G : SimpleGraph V
v : V
⊢ ∃ y, y.supp = ↑(G.connectedComponentMk v)

Tactic:
use G.connectedComponentMk v

Result:
case h
V : Type u
G : SimpleGraph V
v : V
⊢ (G.connectedComponentMk v).supp = ↑(G.connectedComponentMk v)
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Array/Lemmas.lean
theorem setIfInBounds_setIfInBounds (a b : α) (as : Array α) (i : Nat) :
    (as.setIfInBounds i a).setIfInBounds i b = as.setIfInBounds i b

Proof state:
α : Type u_1
a b : α
as : Array α
i : Nat
⊢ (as.setIfInBounds i a).setIfInBounds i b = as.setIfInBounds i b

Tactic:
cases as

Result:
case mk
α : Type u_1
a b : α
i : Nat
toList✝ : List α
⊢ ({ toList := toList✝ }.setIfInBounds i a).setIfInBounds i b = { toList := toList✝ }.setIfInBounds i b

Proof state:
case mk
α : Type u_1
a b : α
i : Nat
toList✝ : List α
⊢ ({ toList := toList✝ }.setIfInBounds i a).setIfInBounds i b = { toList := toList✝ }.setIfInBounds i b

Tactic:
simp

Result:
no goals
-- Mathlib/Analysis/SpecialFunctions/Trigonometric/Arctan.lean
theorem two_mul_arctan_add_pi {x : ℝ} (h : 1 < x) :
    2 * arctan x = arctan (2 * x / (1 - x ^ 2)) + π

Proof state:
x : ℝ
h : 1 < x
⊢ arctan ((x + x) / (1 - x * x)) + π = arctan (2 * x / (1 - x ^ 2)) + π

Tactic:
congr 2

Result:
case e_a.e_x
x : ℝ
h : 1 < x
⊢ (x + x) / (1 - x * x) = 2 * x / (1 - x ^ 2)

Proof state:
x : ℝ
h : 1 < x
⊢ 2 * arctan x = arctan (2 * x / (1 - x ^ 2)) + π

Tactic:
rw [two_mul, arctan_add_eq_add_pi (by nlinarith) (by linarith)]

Result:
x : ℝ
h : 1 < x
⊢ arctan ((x + x) / (1 - x * x)) + π = arctan (2 * x / (1 - x ^ 2)) + π

Proof state:
x : ℝ
h : 1 < x
⊢ 0 < x

Tactic:
linarith

Result:
no goals

Proof state:
x : ℝ
h : 1 < x
⊢ 1 < x * x

Tactic:
nlinarith

Result:
no goals

Proof state:
case e_a.e_x
x : ℝ
h : 1 < x
⊢ (x + x) / (1 - x * x) = 2 * x / (1 - x ^ 2)

Tactic:
ring

Result:
no goals
-- Mathlib/GroupTheory/ClassEquation.lean
theorem Group.card_center_add_sum_card_noncenter_eq_card (G) [Group G]
    [∀ x : ConjClasses G, Fintype x.carrier] [Fintype G] [Fintype <| Subgroup.center G]
    [Fintype <| noncenter G] : Fintype.card (Subgroup.center G) +
  ∑ x ∈ (noncenter G).toFinset, x.carrier.toFinset.card = Fintype.card G

Proof state:
case h.e'_2.h.e'_6
G : Type u_2
inst✝⁴ : Group G
inst✝³ : (x : ConjClasses G) → Fintype ↑x.carrier
inst✝² : Fintype G
inst✝¹ : Fintype ↥(Subgroup.center G)
inst✝ : Fintype ↑(noncenter G)
⊢ ∑ x ∈ (noncenter G).toFinset, x.carrier.toFinset.card =
    ∑ᶠ (x : ConjClasses G) (_ : x ∈ noncenter G), Nat.card ↑x.carrier

Tactic:
rw [← finsum_set_coe_eq_finsum_mem (noncenter G), finsum_eq_sum_of_fintype,
  ← Finset.sum_set_coe]

Result:
case h.e'_2.h.e'_6
G : Type u_2
inst✝⁴ : Group G
inst✝³ : (x : ConjClasses G) → Fintype ↑x.carrier
inst✝² : Fintype G
inst✝¹ : Fintype ↥(Subgroup.center G)
inst✝ : Fintype ↑(noncenter G)
⊢ ∑ i : ↑(noncenter G), (↑i).carrier.toFinset.card = ∑ i : ↑(noncenter G), Nat.card ↑(↑i).carrier

Proof state:
case h.e'_2.h.e'_5
G : Type u_2
inst✝⁴ : Group G
inst✝³ : (x : ConjClasses G) → Fintype ↑x.carrier
inst✝² : Fintype G
inst✝¹ : Fintype ↥(Subgroup.center G)
inst✝ : Fintype ↑(noncenter G)
⊢ Fintype.card ↥(Subgroup.center G) = Nat.card ↥(Subgroup.center G)

Tactic:
simp

Result:
no goals

Proof state:
case h.e'_2.h.e'_6
G : Type u_2
inst✝⁴ : Group G
inst✝³ : (x : ConjClasses G) → Fintype ↑x.carrier
inst✝² : Fintype G
inst✝¹ : Fintype ↥(Subgroup.center G)
inst✝ : Fintype ↑(noncenter G)
⊢ ∑ i : ↑(noncenter G), (↑i).carrier.toFinset.card = ∑ i : ↑(noncenter G), Nat.card ↑(↑i).carrier

Tactic:
simp

Result:
no goals

Proof state:
G : Type u_2
inst✝⁴ : Group G
inst✝³ : (x : ConjClasses G) → Fintype ↑x.carrier
inst✝² : Fintype G
inst✝¹ : Fintype ↥(Subgroup.center G)
inst✝ : Fintype ↑(noncenter G)
⊢ Fintype.card ↥(Subgroup.center G) + ∑ x ∈ (noncenter G).toFinset, x.carrier.toFinset.card = Fintype.card G

Tactic:
convert Group.nat_card_center_add_sum_card_noncenter_eq_card G using 2

Result:
case h.e'_2.h.e'_5
G : Type u_2
inst✝⁴ : Group G
inst✝³ : (x : ConjClasses G) → Fintype ↑x.carrier
inst✝² : Fintype G
inst✝¹ : Fintype ↥(Subgroup.center G)
inst✝ : Fintype ↑(noncenter G)
⊢ Fintype.card ↥(Subgroup.center G) = Nat.card ↥(Subgroup.center G)

case h.e'_2.h.e'_6
G : Type u_2
inst✝⁴ : Group G
inst✝³ : (x : ConjClasses G) → Fintype ↑x.carrier
inst✝² : Fintype G
inst✝¹ : Fintype ↥(Subgroup.center G)
inst✝ : Fintype ↑(noncenter G)
⊢ ∑ x ∈ (noncenter G).toFinset, x.carrier.toFinset.card =
    ∑ᶠ (x : ConjClasses G) (_ : x ∈ noncenter G), Nat.card ↑x.carrier

case h.e'_3
G : Type u_2
inst✝⁴ : Group G
inst✝³ : (x : ConjClasses G) → Fintype ↑x.carrier
inst✝² : Fintype G
inst✝¹ : Fintype ↥(Subgroup.center G)
inst✝ : Fintype ↑(noncenter G)
⊢ Fintype.card G = Nat.card G

Proof state:
case h.e'_3
G : Type u_2
inst✝⁴ : Group G
inst✝³ : (x : ConjClasses G) → Fintype ↑x.carrier
inst✝² : Fintype G
inst✝¹ : Fintype ↥(Subgroup.center G)
inst✝ : Fintype ↑(noncenter G)
⊢ Fintype.card G = Nat.card G

Tactic:
simp

Result:
no goals
-- Mathlib/Data/Seq/Seq.lean
theorem map_cons (f : α → β) (a) : ∀ s, map f (cons a s) = cons (f a) (map f s)
  | ⟨s, al⟩ => by apply Subtype.eq; dsimp [cons, map]; rw [Stream'.map_cons]; rfl

Proof state:
case a
α : Type u
β : Type v
f : α → β
a : α
s : Stream' (Option α)
al : s.IsSeq
⊢ ↑(map f (cons a ⟨s, al⟩)) = ↑(cons (f a) (map f ⟨s, al⟩))

Tactic:
dsimp [cons, map]

Result:
case a
α : Type u
β : Type v
f : α → β
a : α
s : Stream' (Option α)
al : s.IsSeq
⊢ Stream'.map (Option.map f) (some a :: s) = some (f a) :: Stream'.map (Option.map f) s

Proof state:
α : Type u
β : Type v
f : α → β
a : α
s : Stream' (Option α)
al : s.IsSeq
⊢ map f (cons a ⟨s, al⟩) = cons (f a) (map f ⟨s, al⟩)

Tactic:
apply Subtype.eq

Result:
case a
α : Type u
β : Type v
f : α → β
a : α
s : Stream' (Option α)
al : s.IsSeq
⊢ ↑(map f (cons a ⟨s, al⟩)) = ↑(cons (f a) (map f ⟨s, al⟩))

Proof state:
case a
α : Type u
β : Type v
f : α → β
a : α
s : Stream' (Option α)
al : s.IsSeq
⊢ Stream'.map (Option.map f) (some a :: s) = some (f a) :: Stream'.map (Option.map f) s

Tactic:
rw [Stream'.map_cons]

Result:
case a
α : Type u
β : Type v
f : α → β
a : α
s : Stream' (Option α)
al : s.IsSeq
⊢ Option.map f (some a) :: Stream'.map (Option.map f) s = some (f a) :: Stream'.map (Option.map f) s

Proof state:
case a
α : Type u
β : Type v
f : α → β
a : α
s : Stream' (Option α)
al : s.IsSeq
⊢ Option.map f (some a) :: Stream'.map (Option.map f) s = some (f a) :: Stream'.map (Option.map f) s

Tactic:
rfl

Result:
no goals
-- Mathlib/Data/ENNReal/Real.lean
theorem toReal_eq_toReal (ha : a ≠ ∞) (hb : b ≠ ∞) : a.toReal = b.toReal ↔ a = b

Proof state:
a b : ℝ≥0∞
ha : a ≠ ⊤
hb : b ≠ ⊤
⊢ a.toReal = b.toReal ↔ a = b

Tactic:
lift a to ℝ≥0 using ha

Result:
case intro
b : ℝ≥0∞
hb : b ≠ ⊤
a : ℝ≥0
⊢ (↑a).toReal = b.toReal ↔ ↑a = b

Proof state:
case intro
b : ℝ≥0∞
hb : b ≠ ⊤
a : ℝ≥0
⊢ (↑a).toReal = b.toReal ↔ ↑a = b

Tactic:
lift b to ℝ≥0 using hb

Result:
case intro.intro
a b : ℝ≥0
⊢ (↑a).toReal = (↑b).toReal ↔ ↑a = ↑b

Proof state:
case intro.intro
a b : ℝ≥0
⊢ (↑a).toReal = (↑b).toReal ↔ ↑a = ↑b

Tactic:
simp only [coe_inj, NNReal.coe_inj, coe_toReal]

Result:
no goals
-- Mathlib/Topology/Clopen.lean
theorem isClopen_iff_frontier_eq_empty : IsClopen s ↔ frontier s = ∅

Proof state:
X : Type u
inst✝ : TopologicalSpace X
s : Set X
⊢ IsClopen s ↔ frontier s = ∅

Tactic:
rw [IsClopen, ← closure_eq_iff_isClosed, ← interior_eq_iff_isOpen, frontier, diff_eq_empty]

Result:
X : Type u
inst✝ : TopologicalSpace X
s : Set X
⊢ closure s = s ∧ interior s = s ↔ closure s ⊆ interior s

Proof state:
X : Type u
inst✝ : TopologicalSpace X
s : Set X
⊢ closure s = s ∧ interior s = s ↔ closure s ⊆ interior s

Tactic:
refine ⟨fun h => (h.1.trans h.2.symm).subset, fun h => ?_⟩

Result:
X : Type u
inst✝ : TopologicalSpace X
s : Set X
h : closure s ⊆ interior s
⊢ closure s = s ∧ interior s = s

Proof state:
X : Type u
inst✝ : TopologicalSpace X
s : Set X
h : closure s ⊆ interior s
⊢ closure s = s ∧ interior s = s

Tactic:
exact ⟨(h.trans interior_subset).antisymm subset_closure,
  interior_subset.antisymm (subset_closure.trans h)⟩

Result:
no goals
-- Mathlib/RingTheory/Polynomial/ScaleRoots.lean
/-- Multiplication and `scaleRoots` commute up to a power of `r`. The factor disappears if we
assume that the product of the leading coeffs does not vanish. See `Polynomial.mul_scaleRoots'`. -/
lemma mul_scaleRoots (p q : R[X]) (r : R) :
    r ^ (natDegree p + natDegree q - natDegree (p * q)) • (p * q).scaleRoots r =
      p.scaleRoots r * q.scaleRoots r

Proof state:
case inr
R : Type u_1
inst✝ : CommSemiring R
p q : R[X]
r : R
n a b : ℕ
e : a + b = n
ha : a ≤ p.natDegree
⊢ p.coeff a * q.coeff b * r ^ (p.natDegree + q.natDegree - n) =
    p.coeff a * r ^ (p.natDegree - a) * (q.coeff b * r ^ (q.natDegree - b))

Tactic:
cases lt_or_le (natDegree q) b with
| inl h => simp only [coeff_eq_zero_of_natDegree_lt h, zero_mul, mul_zero]
| inr hb =>
  simp only [← e, mul_assoc, mul_comm (r ^ (_ - a)), ← pow_add]
  rw [add_comm (_ - _), tsub_add_tsub_comm ha hb]

Result:
no goals

Proof state:
case inr.inr
R : Type u_1
inst✝ : CommSemiring R
p q : R[X]
r : R
n a b : ℕ
e : a + b = n
ha : a ≤ p.natDegree
hb : b ≤ q.natDegree
⊢ p.coeff a * q.coeff b * r ^ (p.natDegree + q.natDegree - n) =
    p.coeff a * r ^ (p.natDegree - a) * (q.coeff b * r ^ (q.natDegree - b))

Tactic:
simp only [← e, mul_assoc, mul_comm (r ^ (_ - a)), ← pow_add]

Result:
case inr.inr
R : Type u_1
inst✝ : CommSemiring R
p q : R[X]
r : R
n a b : ℕ
e : a + b = n
ha : a ≤ p.natDegree
hb : b ≤ q.natDegree
⊢ p.coeff a * (q.coeff b * r ^ (p.natDegree + q.natDegree - (a + b))) =
    p.coeff a * (q.coeff b * r ^ (q.natDegree - b + (p.natDegree - a)))
-- Mathlib/.lake/packages/lean4/src/lean/Std/Tactic/BVDecide/Bitblast/BVExpr/Circuit/Lemmas/Pred.lean
theorem denote_bitblast (aig : AIG BVBit) (pred : BVPred) (assign : BVExpr.Assignment) :
    ⟦bitblast aig pred, assign.toAIGAssignment⟧ = pred.eval assign

Proof state:
case bin.ult.hleft
aig : AIG BVBit
assign : BVExpr.Assignment
w✝ : Nat
lhs rhs : BVExpr w✝
⊢ ∀ (idx : Nat) (hidx : idx < w✝),
    ⟦assign.toAIGAssignment,
        { aig := (BVExpr.bitblast (BVExpr.bitblast aig lhs).aig rhs).aig,
          ref :=
            { lhs := (BVExpr.bitblast aig lhs).vec.cast ⋯,
                    rhs := (BVExpr.bitblast (BVExpr.bitblast aig lhs).aig rhs).vec }.lhs.get
              idx hidx }⟧ =
      (BVExpr.eval assign lhs).getLsbD idx

Tactic:
intros

Result:
case bin.ult.hleft
aig : AIG BVBit
assign : BVExpr.Assignment
w✝ : Nat
lhs rhs : BVExpr w✝
idx✝ : Nat
hidx✝ : idx✝ < w✝
⊢ ⟦assign.toAIGAssignment,
      { aig := (BVExpr.bitblast (BVExpr.bitblast aig lhs).aig rhs).aig,
        ref :=
          { lhs := (BVExpr.bitblast aig lhs).vec.cast ⋯,
                  rhs := (BVExpr.bitblast (BVExpr.bitblast aig lhs).aig rhs).vec }.lhs.get
            idx✝ hidx✝ }⟧ =
    (BVExpr.eval assign lhs).getLsbD idx✝

Proof state:
case bin.eq.hleft
aig : AIG BVBit
assign : BVExpr.Assignment
w✝ : Nat
lhs rhs : BVExpr w✝
idx✝ : Nat
hidx✝ : idx✝ < w✝
⊢ ({ lhs := (BVExpr.bitblast aig lhs).vec.cast ⋯,
              rhs := (BVExpr.bitblast (BVExpr.bitblast aig lhs).aig rhs).vec }.lhs.get
        idx✝ hidx✝).gate <
    (BVExpr.bitblast aig lhs).aig.decls.size

Tactic:
simp [Ref.hgate]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Std/Tactic/BVDecide/Normalize/BitVec.lean
theorem BitVec.add_const_right (a b c : BitVec w) : a + (b + c) = (a + c) + b

Proof state:
w : Nat
a b c : BitVec w
⊢ a + (b + c) = a + c + b

Tactic:
ac_rfl

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Nat/Bitwise/Lemmas.lean
theorem testBit_two_pow_add_gt {i j : Nat} (j_lt_i : j < i) (x : Nat) :
    testBit (2^i + x) j = testBit x j

Proof state:
i j : Nat
j_lt_i : j < i
x : Nat
i_def : i = j + (i - j)
d : Nat
i_sub_j_eq : i - j = d.succ
⊢ decide ((2 ^ (d + 1) + x / 2 ^ j) % 2 = 1) = decide (x / 2 ^ j % 2 = 1)

Tactic:
simp [Nat.pow_succ, Nat.mul_comm _ 2, Nat.mul_add_mod]

Result:
no goals

Proof state:
i j : Nat
j_lt_i : j < i
x : Nat
i_def : i = j + (i - j)
⊢ decide ((2 ^ (i - j) + x / 2 ^ j) % 2 = 1) = decide (x / 2 ^ j % 2 = 1)

Tactic:
match i_sub_j_eq : i - j with
| 0 =>
  exfalso
  rw [Nat.sub_eq_zero_iff_le] at i_sub_j_eq
  exact Nat.not_le_of_gt j_lt_i i_sub_j_eq
| d+1 =>
  simp [Nat.pow_succ, Nat.mul_comm _ 2, Nat.mul_add_mod]

Result:
no goals

Proof state:
i j : Nat
j_lt_i : j < i
x : Nat
i_def : i = j + (i - j)
⊢ (2 ^ i + x).testBit j = x.testBit j

Tactic:
rw [i_def]

Result:
i j : Nat
j_lt_i : j < i
x : Nat
i_def : i = j + (i - j)
⊢ (2 ^ (j + (i - j)) + x).testBit j = x.testBit j

Proof state:
i j : Nat
j_lt_i : j < i
x : Nat
i_def : i = j + (i - j)
⊢ (2 ^ (j + (i - j)) + x).testBit j = x.testBit j

Tactic:
simp only [testBit_to_div_mod, Nat.pow_add,
      Nat.add_comm x, Nat.mul_add_div (Nat.two_pow_pos _)]

Result:
i j : Nat
j_lt_i : j < i
x : Nat
i_def : i = j + (i - j)
⊢ decide ((2 ^ (i - j) + x / 2 ^ j) % 2 = 1) = decide (x / 2 ^ j % 2 = 1)

Proof state:
i j : Nat
j_lt_i : j < i
x : Nat
i_def : i = j + (i - j)
i_sub_j_eq : i - j = 0
⊢ False

Tactic:
rw [Nat.sub_eq_zero_iff_le] at i_sub_j_eq

Result:
i j : Nat
j_lt_i : j < i
x : Nat
i_def : i = j + (i - j)
i_sub_j_eq : i ≤ j
⊢ False

Proof state:
i j : Nat
j_lt_i : j < i
x : Nat
⊢ (2 ^ i + x).testBit j = x.testBit j

Tactic:
have i_def : i = j + (i-j) := (Nat.add_sub_cancel' (Nat.le_of_lt j_lt_i)).symm

Result:
i j : Nat
j_lt_i : j < i
x : Nat
i_def : i = j + (i - j)
⊢ (2 ^ i + x).testBit j = x.testBit j

Proof state:
i j : Nat
j_lt_i : j < i
x : Nat
i_def : i = j + (i - j)
i_sub_j_eq : i ≤ j
⊢ False

Tactic:
exact Nat.not_le_of_gt j_lt_i i_sub_j_eq

Result:
no goals

Proof state:
i j : Nat
j_lt_i : j < i
x : Nat
i_def : i = j + (i - j)
i_sub_j_eq : i - j = 0
⊢ decide ((2 ^ 0 + x / 2 ^ j) % 2 = 1) = decide (x / 2 ^ j % 2 = 1)

Tactic:
exfalso

Result:
i j : Nat
j_lt_i : j < i
x : Nat
i_def : i = j + (i - j)
i_sub_j_eq : i - j = 0
⊢ False
-- Mathlib/Algebra/Polynomial/Degree/TrailingDegree.lean
theorem natTrailingDegree_le_natDegree (p : R[X]) : p.natTrailingDegree ≤ p.natDegree

Proof state:
case pos
R : Type u
inst✝ : Semiring R
p : R[X]
hp : p = 0
⊢ p.natTrailingDegree ≤ p.natDegree

Tactic:
rw [hp, natDegree_zero, natTrailingDegree_zero]

Result:
no goals

Proof state:
case neg
R : Type u
inst✝ : Semiring R
p : R[X]
hp : ¬p = 0
⊢ p.natTrailingDegree ≤ p.natDegree

Tactic:
exact le_natDegree_of_ne_zero (mt trailingCoeff_eq_zero.mp hp)

Result:
no goals

Proof state:
R : Type u
inst✝ : Semiring R
p : R[X]
⊢ p.natTrailingDegree ≤ p.natDegree

Tactic:
by_cases hp : p = 0

Result:
case pos
R : Type u
inst✝ : Semiring R
p : R[X]
hp : p = 0
⊢ p.natTrailingDegree ≤ p.natDegree

case neg
R : Type u
inst✝ : Semiring R
p : R[X]
hp : ¬p = 0
⊢ p.natTrailingDegree ≤ p.natDegree
-- Mathlib/Topology/MetricSpace/HausdorffDistance.lean
theorem hausdorffDist_image (h : Isometry Φ) :
    hausdorffDist (Φ '' s) (Φ '' t) = hausdorffDist s t

Proof state:
α : Type u
β : Type v
inst✝¹ : PseudoMetricSpace α
inst✝ : PseudoMetricSpace β
s t : Set α
Φ : α → β
h : Isometry Φ
⊢ hausdorffDist (Φ '' s) (Φ '' t) = hausdorffDist s t

Tactic:
simp [hausdorffDist, hausdorffEdist_image h]

Result:
no goals
-- Mathlib/LinearAlgebra/AffineSpace/Basis.lean
theorem coord_apply_combination_of_mem (hi : i ∈ s) {w : ι → k} (hw : s.sum w = 1) :
    b.coord i (s.affineCombination k b w) = w i

Proof state:
ι : Type u_1
k : Type u_5
V : Type u_6
P : Type u_7
inst✝³ : AddCommGroup V
inst✝² : AffineSpace V P
inst✝¹ : Ring k
inst✝ : Module k V
b : AffineBasis ι k P
s : Finset ι
i : ι
hi : i ∈ s
w : ι → k
hw : s.sum w = 1
⊢ (b.coord i) ((Finset.affineCombination k s ⇑b) w) = w i

Tactic:
classical simp only [coord_apply, hi, Finset.affineCombination_eq_linear_combination, if_true,
    mul_boole, hw, Function.comp_apply, smul_eq_mul, s.sum_ite_eq,
    s.map_affineCombination b w hw]

Result:
no goals

Proof state:
ι : Type u_1
k : Type u_5
V : Type u_6
P : Type u_7
inst✝³ : AddCommGroup V
inst✝² : AffineSpace V P
inst✝¹ : Ring k
inst✝ : Module k V
b : AffineBasis ι k P
s : Finset ι
i : ι
hi : i ∈ s
w : ι → k
hw : s.sum w = 1
⊢ (b.coord i) ((Finset.affineCombination k s ⇑b) w) = w i

Tactic:
simp only [coord_apply, hi, Finset.affineCombination_eq_linear_combination, if_true,
mul_boole, hw, Function.comp_apply, smul_eq_mul, s.sum_ite_eq,
s.map_affineCombination b w hw]

Result:
no goals
-- Mathlib/Data/ZMod/Basic.lean
theorem cast_one (h : m ∣ n) : (cast (1 : ZMod n) : R) = 1

Proof state:
case zero
R : Type u_1
inst✝¹ : Ring R
m : ℕ
inst✝ : CharP R m
h : m ∣ 0
⊢ cast 1 = 1

Tactic:
exact Int.cast_one

Result:
no goals

Proof state:
n : ℕ
R : Type u_1
inst✝¹ : Ring R
m : ℕ
inst✝ : CharP R m
h : m ∣ n
⊢ cast 1 = 1

Tactic:
rcases n with - | n

Result:
case zero
R : Type u_1
inst✝¹ : Ring R
m : ℕ
inst✝ : CharP R m
h : m ∣ 0
⊢ cast 1 = 1

case succ
R : Type u_1
inst✝¹ : Ring R
m : ℕ
inst✝ : CharP R m
n : ℕ
h : m ∣ n + 1
⊢ cast 1 = 1

Proof state:
case succ.succ
R : Type u_1
inst✝¹ : Ring R
m : ℕ
inst✝ : CharP R m
n✝ : ℕ
h : m ∣ n✝ + 1 + 1
⊢ 1 < n✝ + 1 + 1

Tactic:
exact Nat.lt_of_sub_eq_succ rfl

Result:
no goals

Proof state:
case succ.succ
R : Type u_1
inst✝¹ : Ring R
m : ℕ
inst✝ : CharP R m
n✝ : ℕ
h : m ∣ n✝ + 1 + 1
⊢ ↑1 = 1

Tactic:
exact Nat.cast_one

Result:
no goals

Proof state:
case succ.zero
R : Type u_1
inst✝¹ : Ring R
inst✝ : CharP R 1
⊢ ↑(1 % (0 + 1)) = 1

Tactic:
subsingleton [CharP.CharOne.subsingleton]

Result:
no goals

Proof state:
case succ
R : Type u_1
inst✝¹ : Ring R
m : ℕ
inst✝ : CharP R m
n : ℕ
h : m ∣ n + 1
⊢ ↑(1 % (n + 1)) = 1

Tactic:
cases n

Result:
case succ.zero
R : Type u_1
inst✝¹ : Ring R
m : ℕ
inst✝ : CharP R m
h : m ∣ 0 + 1
⊢ ↑(1 % (0 + 1)) = 1

case succ.succ
R : Type u_1
inst✝¹ : Ring R
m : ℕ
inst✝ : CharP R m
n✝ : ℕ
h : m ∣ n✝ + 1 + 1
⊢ ↑(1 % (n✝ + 1 + 1)) = 1

Proof state:
case succ.succ
R : Type u_1
inst✝¹ : Ring R
m : ℕ
inst✝ : CharP R m
n✝ : ℕ
h : m ∣ n✝ + 1 + 1
⊢ ↑(1 % (n✝ + 1 + 1)) = 1

Tactic:
rw [Nat.mod_eq_of_lt]

Result:
case succ.succ
R : Type u_1
inst✝¹ : Ring R
m : ℕ
inst✝ : CharP R m
n✝ : ℕ
h : m ∣ n✝ + 1 + 1
⊢ ↑1 = 1

case succ.succ
R : Type u_1
inst✝¹ : Ring R
m : ℕ
inst✝ : CharP R m
n✝ : ℕ
h : m ∣ n✝ + 1 + 1
⊢ 1 < n✝ + 1 + 1

Proof state:
case succ
R : Type u_1
inst✝¹ : Ring R
m : ℕ
inst✝ : CharP R m
n : ℕ
h : m ∣ n + 1
⊢ cast 1 = 1

Tactic:
show ((1 % (n + 1) : ℕ) : R) = 1

Result:
case succ
R : Type u_1
inst✝¹ : Ring R
m : ℕ
inst✝ : CharP R m
n : ℕ
h : m ∣ n + 1
⊢ ↑(1 % (n + 1)) = 1

Proof state:
case succ.zero
R : Type u_1
inst✝¹ : Ring R
m : ℕ
inst✝ : CharP R m
h : m ∣ 0 + 1
⊢ ↑(1 % (0 + 1)) = 1

Tactic:
rw [Nat.dvd_one] at h

Result:
case succ.zero
R : Type u_1
inst✝¹ : Ring R
m : ℕ
inst✝ : CharP R m
h : m = 1
⊢ ↑(1 % (0 + 1)) = 1

Proof state:
case succ.zero
R : Type u_1
inst✝¹ : Ring R
m : ℕ
inst✝ : CharP R m
h : m = 1
⊢ ↑(1 % (0 + 1)) = 1

Tactic:
subst m

Result:
case succ.zero
R : Type u_1
inst✝¹ : Ring R
inst✝ : CharP R 1
⊢ ↑(1 % (0 + 1)) = 1
-- Mathlib/RingTheory/Ideal/Quotient/Operations.lean
theorem quotQuotEquivComm_symmₐ : (quotQuotEquivCommₐ R I J).symm = quotQuotEquivCommₐ R J I

Proof state:
case h
R : Type u
A : Type u_1
inst✝² : CommSemiring R
inst✝¹ : CommRing A
inst✝ : Algebra R A
I J : Ideal A
a✝ : (A ⧸ J) ⧸ map (Quotient.mkₐ R J) I
⊢ (AlgEquiv.ofRingEquiv ⋯).symm a✝ = (AlgEquiv.ofRingEquiv ⋯) a✝

Tactic:
congr

Result:
no goals

Proof state:
R : Type u
A : Type u_1
inst✝² : CommSemiring R
inst✝¹ : CommRing A
inst✝ : Algebra R A
I J : Ideal A
⊢ (quotQuotEquivCommₐ R I J).symm = quotQuotEquivCommₐ R J I

Tactic:
ext

Result:
case h
R : Type u
A : Type u_1
inst✝² : CommSemiring R
inst✝¹ : CommRing A
inst✝ : Algebra R A
I J : Ideal A
a✝ : (A ⧸ J) ⧸ map (Quotient.mkₐ R J) I
⊢ (quotQuotEquivCommₐ R I J).symm a✝ = (quotQuotEquivCommₐ R J I) a✝

Proof state:
case h
R : Type u
A : Type u_1
inst✝² : CommSemiring R
inst✝¹ : CommRing A
inst✝ : Algebra R A
I J : Ideal A
a✝ : (A ⧸ J) ⧸ map (Quotient.mkₐ R J) I
⊢ (quotQuotEquivCommₐ R I J).symm a✝ = (quotQuotEquivCommₐ R J I) a✝

Tactic:
unfold quotQuotEquivCommₐ

Result:
case h
R : Type u
A : Type u_1
inst✝² : CommSemiring R
inst✝¹ : CommRing A
inst✝ : Algebra R A
I J : Ideal A
a✝ : (A ⧸ J) ⧸ map (Quotient.mkₐ R J) I
⊢ (AlgEquiv.ofRingEquiv ⋯).symm a✝ = (AlgEquiv.ofRingEquiv ⋯) a✝
-- Mathlib/Computability/AkraBazzi/AkraBazzi.lean
lemma asympBound_pos (n : ℕ) (hn : 0 < n) : 0 < asympBound g a b n

Proof state:
α : Type u_1
inst✝¹ : Fintype α
T : ℕ → ℝ
g : ℝ → ℝ
a b : α → ℝ
r : α → ℕ → ℕ
inst✝ : Nonempty α
R : AkraBazziRecurrence T g a b r
n : ℕ
hn : 0 < n
⊢ 0 < ↑n ^ p a b * (1 + 0)

Tactic:
aesop (add safe Real.rpow_pos_of_pos)

Result:
no goals

Proof state:
case h.bc
α : Type u_1
inst✝¹ : Fintype α
T : ℕ → ℝ
g : ℝ → ℝ
a b : α → ℝ
r : α → ℕ → ℕ
inst✝ : Nonempty α
R : AkraBazziRecurrence T g a b r
n : ℕ
hn : 0 < n
this : ∀ x ≥ 0, 0 ≤ g x
⊢ 0 ≤ ∑ u ∈ range n, g ↑u / ↑u ^ (p a b + 1)

Tactic:
aesop (add safe Real.rpow_nonneg,
           safe div_nonneg,
           safe Finset.sum_nonneg)

Result:
no goals

Proof state:
α : Type u_1
inst✝¹ : Fintype α
T : ℕ → ℝ
g : ℝ → ℝ
a b : α → ℝ
r : α → ℕ → ℕ
inst✝ : Nonempty α
R : AkraBazziRecurrence T g a b r
n : ℕ
hn : 0 < n
⊢ ↑n ^ p a b * (1 + 0) ≤ asympBound g a b n

Tactic:
simp only [asympBound_def']

Result:
α : Type u_1
inst✝¹ : Fintype α
T : ℕ → ℝ
g : ℝ → ℝ
a b : α → ℝ
r : α → ℕ → ℕ
inst✝ : Nonempty α
R : AkraBazziRecurrence T g a b r
n : ℕ
hn : 0 < n
⊢ ↑n ^ p a b * (1 + 0) ≤ ↑n ^ p a b * (1 + ∑ u ∈ range n, g ↑u / ↑u ^ (p a b + 1))

Proof state:
case h.bc
α : Type u_1
inst✝¹ : Fintype α
T : ℕ → ℝ
g : ℝ → ℝ
a b : α → ℝ
r : α → ℕ → ℕ
inst✝ : Nonempty α
R : AkraBazziRecurrence T g a b r
n : ℕ
hn : 0 < n
⊢ 0 ≤ ∑ u ∈ range n, g ↑u / ↑u ^ (p a b + 1)

Tactic:
have := R.g_nonneg

Result:
case h.bc
α : Type u_1
inst✝¹ : Fintype α
T : ℕ → ℝ
g : ℝ → ℝ
a b : α → ℝ
r : α → ℕ → ℕ
inst✝ : Nonempty α
R : AkraBazziRecurrence T g a b r
n : ℕ
hn : 0 < n
this : ∀ x ≥ 0, 0 ≤ g x
⊢ 0 ≤ ∑ u ∈ range n, g ↑u / ↑u ^ (p a b + 1)

Proof state:
α : Type u_1
inst✝¹ : Fintype α
T : ℕ → ℝ
g : ℝ → ℝ
a b : α → ℝ
r : α → ℕ → ℕ
inst✝ : Nonempty α
R : AkraBazziRecurrence T g a b r
n : ℕ
hn : 0 < n
⊢ 0 < asympBound g a b n

Tactic:
calc 0 < (n : ℝ) ^ p a b * (1 + 0) := by aesop (add safe Real.rpow_pos_of_pos)
     _ ≤ asympBound g a b n := by
                  simp only [asympBound_def']
                  gcongr n^p a b * (1 + ?_)
                  have := R.g_nonneg
                  aesop (add safe Real.rpow_nonneg,
                             safe div_nonneg,
                             safe Finset.sum_nonneg)

Result:
no goals

Proof state:
α : Type u_1
inst✝¹ : Fintype α
T : ℕ → ℝ
g : ℝ → ℝ
a b : α → ℝ
r : α → ℕ → ℕ
inst✝ : Nonempty α
R : AkraBazziRecurrence T g a b r
n : ℕ
hn : 0 < n
⊢ ↑n ^ p a b * (1 + 0) ≤ ↑n ^ p a b * (1 + ∑ u ∈ range n, g ↑u / ↑u ^ (p a b + 1))

Tactic:
gcongr n^p a b * (1 + ?_)

Result:
case h.bc
α : Type u_1
inst✝¹ : Fintype α
T : ℕ → ℝ
g : ℝ → ℝ
a b : α → ℝ
r : α → ℕ → ℕ
inst✝ : Nonempty α
R : AkraBazziRecurrence T g a b r
n : ℕ
hn : 0 < n
⊢ 0 ≤ ∑ u ∈ range n, g ↑u / ↑u ^ (p a b + 1)