harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/GroupTheory/SpecificGroups/Cyclic.lean
theorem isCyclic_of_surjective {F : Type*} [hH : IsCyclic G']
    [FunLike F G' G] [MonoidHomClass F G' G] (f : F) (hf : Function.Surjective f) :
    IsCyclic G

Proof state:
case mk.intro
G : Type u_2
G' : Type u_3
inst✝³ : Group G
inst✝² : Group G'
F : Type u_4
inst✝¹ : FunLike F G' G
inst✝ : MonoidHomClass F G' G
f : F
hf : Function.Surjective ⇑f
x : G'
hx : Function.Surjective fun x_1 => x ^ x_1
a : G
⊢ ∃ a_1, (fun x_1 => f x ^ x_1) a_1 = a

Tactic:
obtain ⟨a, rfl⟩ := hf a

Result:
case mk.intro.intro
G : Type u_2
G' : Type u_3
inst✝³ : Group G
inst✝² : Group G'
F : Type u_4
inst✝¹ : FunLike F G' G
inst✝ : MonoidHomClass F G' G
f : F
hf : Function.Surjective ⇑f
x : G'
hx : Function.Surjective fun x_1 => x ^ x_1
a : G'
⊢ ∃ a_1, (fun x_1 => f x ^ x_1) a_1 = f a

Proof state:
G : Type u_2
G' : Type u_3
inst✝³ : Group G
inst✝² : Group G'
F : Type u_4
hH : IsCyclic G'
inst✝¹ : FunLike F G' G
inst✝ : MonoidHomClass F G' G
f : F
hf : Function.Surjective ⇑f
⊢ IsCyclic G

Tactic:
obtain ⟨x, hx⟩ := hH

Result:
case mk.intro
G : Type u_2
G' : Type u_3
inst✝³ : Group G
inst✝² : Group G'
F : Type u_4
inst✝¹ : FunLike F G' G
inst✝ : MonoidHomClass F G' G
f : F
hf : Function.Surjective ⇑f
x : G'
hx : Function.Surjective fun x_1 => x ^ x_1
⊢ IsCyclic G

Proof state:
case mk.intro
G : Type u_2
G' : Type u_3
inst✝³ : Group G
inst✝² : Group G'
F : Type u_4
inst✝¹ : FunLike F G' G
inst✝ : MonoidHomClass F G' G
f : F
hf : Function.Surjective ⇑f
x : G'
hx : Function.Surjective fun x_1 => x ^ x_1
⊢ IsCyclic G

Tactic:
refine ⟨f x, fun a ↦ ?_⟩

Result:
case mk.intro
G : Type u_2
G' : Type u_3
inst✝³ : Group G
inst✝² : Group G'
F : Type u_4
inst✝¹ : FunLike F G' G
inst✝ : MonoidHomClass F G' G
f : F
hf : Function.Surjective ⇑f
x : G'
hx : Function.Surjective fun x_1 => x ^ x_1
a : G
⊢ ∃ a_1, (fun x_1 => f x ^ x_1) a_1 = a

Proof state:
case mk.intro.intro
G : Type u_2
G' : Type u_3
inst✝³ : Group G
inst✝² : Group G'
F : Type u_4
inst✝¹ : FunLike F G' G
inst✝ : MonoidHomClass F G' G
f : F
hf : Function.Surjective ⇑f
x : G'
hx : Function.Surjective fun x_1 => x ^ x_1
a : G'
⊢ ∃ a_1, (fun x_1 => f x ^ x_1) a_1 = f a

Tactic:
obtain ⟨n, rfl⟩ := hx a

Result:
case mk.intro.intro.intro
G : Type u_2
G' : Type u_3
inst✝³ : Group G
inst✝² : Group G'
F : Type u_4
inst✝¹ : FunLike F G' G
inst✝ : MonoidHomClass F G' G
f : F
hf : Function.Surjective ⇑f
x : G'
hx : Function.Surjective fun x_1 => x ^ x_1
n : ℤ
⊢ ∃ a, (fun x_1 => f x ^ x_1) a = f ((fun x_1 => x ^ x_1) n)

Proof state:
case mk.intro.intro.intro
G : Type u_2
G' : Type u_3
inst✝³ : Group G
inst✝² : Group G'
F : Type u_4
inst✝¹ : FunLike F G' G
inst✝ : MonoidHomClass F G' G
f : F
hf : Function.Surjective ⇑f
x : G'
hx : Function.Surjective fun x_1 => x ^ x_1
n : ℤ
⊢ ∃ a, (fun x_1 => f x ^ x_1) a = f ((fun x_1 => x ^ x_1) n)

Tactic:
exact ⟨n, (map_zpow _ _ _).symm⟩

Result:
no goals
-- Mathlib/Analysis/Analytic/Composition.lean
theorem id_apply_of_one_lt (x : E) {n : ℕ} (h : 1 < n) :
    (FormalMultilinearSeries.id 𝕜 E x) n = 0

Proof state:
𝕜 : Type u_1
E : Type u_2
inst✝² : NontriviallyNormedField 𝕜
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
x : E
n : ℕ
h : 1 < n
⊢ id 𝕜 E x n = 0

Tactic:
match n with
  | 0 => contradiction
  | 1 => contradiction
  | n + 2 => rfl

Result:
no goals

Proof state:
𝕜 : Type u_1
E : Type u_2
inst✝² : NontriviallyNormedField 𝕜
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
x : E
n : ℕ
h : 1 < 1
⊢ id 𝕜 E x 1 = 0

Tactic:
contradiction

Result:
no goals

Proof state:
𝕜 : Type u_1
E : Type u_2
inst✝² : NontriviallyNormedField 𝕜
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
x : E
n : ℕ
h : 1 < 0
⊢ id 𝕜 E x 0 = 0

Tactic:
contradiction

Result:
no goals

Proof state:
𝕜 : Type u_1
E : Type u_2
inst✝² : NontriviallyNormedField 𝕜
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
x : E
n✝ n : ℕ
h : 1 < n + 2
⊢ id 𝕜 E x (n + 2) = 0

Tactic:
rfl

Result:
no goals
-- Mathlib/Algebra/Ring/Periodic.lean
theorem Antiperiodic.sub [AddGroup α] [InvolutiveNeg β] (h1 : Antiperiodic f c₁)
    (h2 : Antiperiodic f c₂) : Periodic f (c₁ - c₂)

Proof state:
α : Type u_1
β : Type u_2
f : α → β
c₁ c₂ : α
inst✝¹ : AddGroup α
inst✝ : InvolutiveNeg β
h1 : Antiperiodic f c₁
h2 : Antiperiodic f c₂
⊢ Periodic f (c₁ - c₂)

Tactic:
simpa only [sub_eq_add_neg] using h1.add h2.neg

Result:
no goals
-- Mathlib/Analysis/Normed/Module/Dual.lean
theorem isBounded_polar_of_mem_nhds_zero {s : Set E} (s_nhd : s ∈ 𝓝 (0 : E)) :
    IsBounded (polar 𝕜 s)

Proof state:
case intro.intro.intro
𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
E : Type u_2
inst✝¹ : SeminormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
s : Set E
s_nhd : s ∈ 𝓝 0
a : 𝕜
ha : 1 < ‖a‖
r : ℝ
r_pos : 0 < r
r_ball : ball 0 r ⊆ s
⊢ IsBounded (polar 𝕜 s)

Tactic:
exact isBounded_closedBall.subset
  (((dualPairing 𝕜 E).flip.polar_antitone r_ball).trans <|
    polar_ball_subset_closedBall_div ha r_pos)

Result:
no goals

Proof state:
case intro
𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
E : Type u_2
inst✝¹ : SeminormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
s : Set E
s_nhd : s ∈ 𝓝 0
a : 𝕜
ha : 1 < ‖a‖
⊢ IsBounded (polar 𝕜 s)

Tactic:
obtain ⟨r, r_pos, r_ball⟩ : ∃ r : ℝ, 0 < r ∧ ball 0 r ⊆ s := Metric.mem_nhds_iff.1 s_nhd

Result:
case intro.intro.intro
𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
E : Type u_2
inst✝¹ : SeminormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
s : Set E
s_nhd : s ∈ 𝓝 0
a : 𝕜
ha : 1 < ‖a‖
r : ℝ
r_pos : 0 < r
r_ball : ball 0 r ⊆ s
⊢ IsBounded (polar 𝕜 s)

Proof state:
𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
E : Type u_2
inst✝¹ : SeminormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
s : Set E
s_nhd : s ∈ 𝓝 0
⊢ IsBounded (polar 𝕜 s)

Tactic:
obtain ⟨a, ha⟩ : ∃ a : 𝕜, 1 < ‖a‖ := NormedField.exists_one_lt_norm 𝕜

Result:
case intro
𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
E : Type u_2
inst✝¹ : SeminormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
s : Set E
s_nhd : s ∈ 𝓝 0
a : 𝕜
ha : 1 < ‖a‖
⊢ IsBounded (polar 𝕜 s)
-- Mathlib/Analysis/NormedSpace/Real.lean
theorem exists_norm_eq {c : ℝ} (hc : 0 ≤ c) : ∃ x : E, ‖x‖ = c

Proof state:
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : Nontrivial E
c : ℝ
hc : 0 ≤ c
⊢ ∃ x, ‖x‖ = c

Tactic:
rcases exists_ne (0 : E) with ⟨x, hx⟩

Result:
case intro
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : Nontrivial E
c : ℝ
hc : 0 ≤ c
x : E
hx : x ≠ 0
⊢ ∃ x, ‖x‖ = c

Proof state:
case h
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : Nontrivial E
c : ℝ
hc : 0 ≤ c
x : E
hx : ‖x‖ ≠ 0
⊢ ‖c • ‖x‖⁻¹ • x‖ = c

Tactic:
simp [norm_smul, Real.norm_of_nonneg hc, abs_of_nonneg hc, inv_mul_cancel₀ hx]

Result:
no goals

Proof state:
case intro
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : Nontrivial E
c : ℝ
hc : 0 ≤ c
x : E
hx : x ≠ 0
⊢ ∃ x, ‖x‖ = c

Tactic:
rw [← norm_ne_zero_iff] at hx

Result:
case intro
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : Nontrivial E
c : ℝ
hc : 0 ≤ c
x : E
hx : ‖x‖ ≠ 0
⊢ ∃ x, ‖x‖ = c

Proof state:
case intro
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : Nontrivial E
c : ℝ
hc : 0 ≤ c
x : E
hx : ‖x‖ ≠ 0
⊢ ∃ x, ‖x‖ = c

Tactic:
use c • ‖x‖⁻¹ • x

Result:
case h
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : Nontrivial E
c : ℝ
hc : 0 ≤ c
x : E
hx : ‖x‖ ≠ 0
⊢ ‖c • ‖x‖⁻¹ • x‖ = c
-- Mathlib/Data/DFinsupp/Multiset.lean
theorem toDFinsupp_replicate (a : α) (n : ℕ) :
    toDFinsupp (Multiset.replicate n a) = DFinsupp.single a n

Proof state:
case h
α : Type u_1
inst✝ : DecidableEq α
a : α
n : ℕ
i : α
⊢ (toDFinsupp (replicate n a)) i = (DFinsupp.single a n) i

Tactic:
dsimp [toDFinsupp]

Result:
case h
α : Type u_1
inst✝ : DecidableEq α
a : α
n : ℕ
i : α
⊢ count i (replicate n a) = (DFinsupp.single a n) i

Proof state:
case h
α : Type u_1
inst✝ : DecidableEq α
a : α
n : ℕ
i : α
⊢ count i (replicate n a) = (DFinsupp.single a n) i

Tactic:
simp [count_replicate, eq_comm]

Result:
no goals

Proof state:
α : Type u_1
inst✝ : DecidableEq α
a : α
n : ℕ
⊢ toDFinsupp (replicate n a) = DFinsupp.single a n

Tactic:
ext i

Result:
case h
α : Type u_1
inst✝ : DecidableEq α
a : α
n : ℕ
i : α
⊢ (toDFinsupp (replicate n a)) i = (DFinsupp.single a n) i
-- Mathlib/RingTheory/Finiteness/Finsupp.lean
theorem fg_ker_comp (f : M →ₗ[R] N) (g : N →ₗ[R] P)
    (hf1 : (LinearMap.ker f).FG) (hf2 : (LinearMap.ker g).FG)
    (hsur : Function.Surjective f) : (g.comp f).ker.FG

Proof state:
R : Type u_1
M : Type u_2
N : Type u_3
P : Type u_4
inst✝⁶ : Ring R
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
inst✝³ : AddCommGroup N
inst✝² : Module R N
inst✝¹ : AddCommGroup P
inst✝ : Module R P
f : M →ₗ[R] N
g : N →ₗ[R] P
hf1 : (LinearMap.ker f).FG
hf2 : (LinearMap.ker g).FG
hsur : Surjective ⇑f
⊢ (LinearMap.ker (g ∘ₗ f)).FG

Tactic:
rw [LinearMap.ker_comp]

Result:
R : Type u_1
M : Type u_2
N : Type u_3
P : Type u_4
inst✝⁶ : Ring R
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
inst✝³ : AddCommGroup N
inst✝² : Module R N
inst✝¹ : AddCommGroup P
inst✝ : Module R P
f : M →ₗ[R] N
g : N →ₗ[R] P
hf1 : (LinearMap.ker f).FG
hf2 : (LinearMap.ker g).FG
hsur : Surjective ⇑f
⊢ (comap f (LinearMap.ker g)).FG

Proof state:
case hs1
R : Type u_1
M : Type u_2
N : Type u_3
P : Type u_4
inst✝⁶ : Ring R
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
inst✝³ : AddCommGroup N
inst✝² : Module R N
inst✝¹ : AddCommGroup P
inst✝ : Module R P
f : M →ₗ[R] N
g : N →ₗ[R] P
hf1 : (LinearMap.ker f).FG
hf2 : (LinearMap.ker g).FG
hsur : Surjective ⇑f
⊢ (map f (comap f (LinearMap.ker g))).FG

Tactic:
rwa [Submodule.map_comap_eq, LinearMap.range_eq_top.2 hsur, top_inf_eq]

Result:
no goals

Proof state:
R : Type u_1
M : Type u_2
N : Type u_3
P : Type u_4
inst✝⁶ : Ring R
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
inst✝³ : AddCommGroup N
inst✝² : Module R N
inst✝¹ : AddCommGroup P
inst✝ : Module R P
f : M →ₗ[R] N
g : N →ₗ[R] P
hf1 : (LinearMap.ker f).FG
hf2 : (LinearMap.ker g).FG
hsur : Surjective ⇑f
⊢ (comap f (LinearMap.ker g)).FG

Tactic:
apply fg_of_fg_map_of_fg_inf_ker f

Result:
case hs1
R : Type u_1
M : Type u_2
N : Type u_3
P : Type u_4
inst✝⁶ : Ring R
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
inst✝³ : AddCommGroup N
inst✝² : Module R N
inst✝¹ : AddCommGroup P
inst✝ : Module R P
f : M →ₗ[R] N
g : N →ₗ[R] P
hf1 : (LinearMap.ker f).FG
hf2 : (LinearMap.ker g).FG
hsur : Surjective ⇑f
⊢ (map f (comap f (LinearMap.ker g))).FG

case hs2
R : Type u_1
M : Type u_2
N : Type u_3
P : Type u_4
inst✝⁶ : Ring R
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
inst✝³ : AddCommGroup N
inst✝² : Module R N
inst✝¹ : AddCommGroup P
inst✝ : Module R P
f : M →ₗ[R] N
g : N →ₗ[R] P
hf1 : (LinearMap.ker f).FG
hf2 : (LinearMap.ker g).FG
hsur : Surjective ⇑f
⊢ (comap f (LinearMap.ker g) ⊓ LinearMap.ker f).FG

Proof state:
case hs2
R : Type u_1
M : Type u_2
N : Type u_3
P : Type u_4
inst✝⁶ : Ring R
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
inst✝³ : AddCommGroup N
inst✝² : Module R N
inst✝¹ : AddCommGroup P
inst✝ : Module R P
f : M →ₗ[R] N
g : N →ₗ[R] P
hf1 : (LinearMap.ker f).FG
hf2 : (LinearMap.ker g).FG
hsur : Surjective ⇑f
⊢ (comap f (LinearMap.ker g) ⊓ LinearMap.ker f).FG

Tactic:
rwa [inf_of_le_right (show (LinearMap.ker f) ≤
  (LinearMap.ker g).comap f from comap_mono bot_le)]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/BitVec/Bitblast.lean
theorem umod_eq_of_mul_add_toNat {d n q r : BitVec w} (hrd : r < d)
    (hdqnr : d.toNat * q.toNat + r.toNat = n.toNat) :
    n % d = r

Proof state:
case a
w : Nat
d n q r : BitVec w
hdqnr : r.toNat % d.toNat = n.toNat % d.toNat
hrd : r.toNat < d.toNat
⊢ n.toNat % d.toNat = r.toNat

Tactic:
rw [Nat.mod_eq_of_lt hrd] at hdqnr

Result:
case a
w : Nat
d n q r : BitVec w
hdqnr : r.toNat = n.toNat % d.toNat
hrd : r.toNat < d.toNat
⊢ n.toNat % d.toNat = r.toNat

Proof state:
w : Nat
d n q r : BitVec w
hrd : r < d
hdqnr : d.toNat * q.toNat + r.toNat = n.toNat
⊢ (d.toNat * q.toNat + r.toNat) % d.toNat = n.toNat % d.toNat

Tactic:
simp [hdqnr]

Result:
no goals

Proof state:
case a
w : Nat
d n q r : BitVec w
hrd : r < d
hdqnr : r.toNat % d.toNat = n.toNat % d.toNat
⊢ n.toNat % d.toNat = r.toNat

Tactic:
replace hrd : r.toNat < d.toNat := by
  simpa [BitVec.lt_def] using hrd

Result:
case a
w : Nat
d n q r : BitVec w
hdqnr : r.toNat % d.toNat = n.toNat % d.toNat
hrd : r.toNat < d.toNat
⊢ n.toNat % d.toNat = r.toNat

Proof state:
case a
w : Nat
d n q r : BitVec w
hrd : r < d
hdqnr : d.toNat * q.toNat + r.toNat = n.toNat
⊢ n.toNat % d.toNat = r.toNat

Tactic:
replace hdqnr : (d.toNat * q.toNat + r.toNat) % d.toNat = n.toNat % d.toNat := by
  simp [hdqnr]

Result:
case a
w : Nat
d n q r : BitVec w
hrd : r < d
hdqnr : (d.toNat * q.toNat + r.toNat) % d.toNat = n.toNat % d.toNat
⊢ n.toNat % d.toNat = r.toNat

Proof state:
case a
w : Nat
d n q r : BitVec w
hrd : r < d
hdqnr : (d.toNat * q.toNat + r.toNat) % d.toNat = n.toNat % d.toNat
⊢ n.toNat % d.toNat = r.toNat

Tactic:
rw [Nat.add_mod, Nat.mul_mod_right] at hdqnr

Result:
case a
w : Nat
d n q r : BitVec w
hrd : r < d
hdqnr : (0 + r.toNat % d.toNat) % d.toNat = n.toNat % d.toNat
⊢ n.toNat % d.toNat = r.toNat

Proof state:
w : Nat
d n q r : BitVec w
hrd : r < d
hdqnr : r.toNat % d.toNat = n.toNat % d.toNat
⊢ r.toNat < d.toNat

Tactic:
simpa [BitVec.lt_def] using hrd

Result:
no goals

Proof state:
case a
w : Nat
d n q r : BitVec w
hdqnr : r.toNat = n.toNat % d.toNat
hrd : r.toNat < d.toNat
⊢ n.toNat % d.toNat = r.toNat

Tactic:
simp [hdqnr]

Result:
no goals

Proof state:
w : Nat
d n q r : BitVec w
hrd : r < d
hdqnr : d.toNat * q.toNat + r.toNat = n.toNat
⊢ n % d = r

Tactic:
apply BitVec.eq_of_toNat_eq

Result:
case a
w : Nat
d n q r : BitVec w
hrd : r < d
hdqnr : d.toNat * q.toNat + r.toNat = n.toNat
⊢ (n % d).toNat = r.toNat

Proof state:
case a
w : Nat
d n q r : BitVec w
hrd : r < d
hdqnr : (0 + r.toNat % d.toNat) % d.toNat = n.toNat % d.toNat
⊢ n.toNat % d.toNat = r.toNat

Tactic:
simp only [Nat.zero_add, mod_mod] at hdqnr

Result:
case a
w : Nat
d n q r : BitVec w
hrd : r < d
hdqnr : r.toNat % d.toNat = n.toNat % d.toNat
⊢ n.toNat % d.toNat = r.toNat

Proof state:
case a
w : Nat
d n q r : BitVec w
hrd : r < d
hdqnr : d.toNat * q.toNat + r.toNat = n.toNat
⊢ (n % d).toNat = r.toNat

Tactic:
rw [toNat_umod]

Result:
case a
w : Nat
d n q r : BitVec w
hrd : r < d
hdqnr : d.toNat * q.toNat + r.toNat = n.toNat
⊢ n.toNat % d.toNat = r.toNat
-- Mathlib/Geometry/Euclidean/Angle/Sphere.lean
theorem Cospherical.two_zsmul_oangle_eq {p₁ p₂ p₃ p₄ : P}
    (h : Cospherical ({p₁, p₂, p₃, p₄} : Set P)) (hp₂p₁ : p₂ ≠ p₁) (hp₂p₄ : p₂ ≠ p₄)
    (hp₃p₁ : p₃ ≠ p₁) (hp₃p₄ : p₃ ≠ p₄) : (2 : ℤ) • ∡ p₁ p₂ p₄ = (2 : ℤ) • ∡ p₁ p₃ p₄

Proof state:
case intro
V : Type u_1
P : Type u_2
inst✝⁴ : NormedAddCommGroup V
inst✝³ : InnerProductSpace ℝ V
inst✝² : MetricSpace P
inst✝¹ : NormedAddTorsor V P
hd2 : Fact (finrank ℝ V = 2)
inst✝ : Oriented ℝ V (Fin 2)
p₁ p₂ p₃ p₄ : P
h : Cospherical {p₁, p₂, p₃, p₄}
hp₂p₁ : p₂ ≠ p₁
hp₂p₄ : p₂ ≠ p₄
hp₃p₁ : p₃ ≠ p₁
hp₃p₄ : p₃ ≠ p₄
s : Sphere P
hs : p₁ ∈ s ∧ p₂ ∈ s ∧ p₃ ∈ s ∧ p₄ ∈ s
⊢ 2 • ∡ p₁ p₂ p₄ = 2 • ∡ p₁ p₃ p₄

Tactic:
exact Sphere.two_zsmul_oangle_eq hs.1 hs.2.1 hs.2.2.1 hs.2.2.2 hp₂p₁ hp₂p₄ hp₃p₁ hp₃p₄

Result:
no goals

Proof state:
V : Type u_1
P : Type u_2
inst✝⁴ : NormedAddCommGroup V
inst✝³ : InnerProductSpace ℝ V
inst✝² : MetricSpace P
inst✝¹ : NormedAddTorsor V P
hd2 : Fact (finrank ℝ V = 2)
inst✝ : Oriented ℝ V (Fin 2)
p₁ p₂ p₃ p₄ : P
h : Cospherical {p₁, p₂, p₃, p₄}
hp₂p₁ : p₂ ≠ p₁
hp₂p₄ : p₂ ≠ p₄
hp₃p₁ : p₃ ≠ p₁
hp₃p₄ : p₃ ≠ p₄
⊢ 2 • ∡ p₁ p₂ p₄ = 2 • ∡ p₁ p₃ p₄

Tactic:
obtain ⟨s, hs⟩ := cospherical_iff_exists_sphere.1 h

Result:
case intro
V : Type u_1
P : Type u_2
inst✝⁴ : NormedAddCommGroup V
inst✝³ : InnerProductSpace ℝ V
inst✝² : MetricSpace P
inst✝¹ : NormedAddTorsor V P
hd2 : Fact (finrank ℝ V = 2)
inst✝ : Oriented ℝ V (Fin 2)
p₁ p₂ p₃ p₄ : P
h : Cospherical {p₁, p₂, p₃, p₄}
hp₂p₁ : p₂ ≠ p₁
hp₂p₄ : p₂ ≠ p₄
hp₃p₁ : p₃ ≠ p₁
hp₃p₄ : p₃ ≠ p₄
s : Sphere P
hs : {p₁, p₂, p₃, p₄} ⊆ Metric.sphere s.center s.radius
⊢ 2 • ∡ p₁ p₂ p₄ = 2 • ∡ p₁ p₃ p₄

Proof state:
case intro
V : Type u_1
P : Type u_2
inst✝⁴ : NormedAddCommGroup V
inst✝³ : InnerProductSpace ℝ V
inst✝² : MetricSpace P
inst✝¹ : NormedAddTorsor V P
hd2 : Fact (finrank ℝ V = 2)
inst✝ : Oriented ℝ V (Fin 2)
p₁ p₂ p₃ p₄ : P
h : Cospherical {p₁, p₂, p₃, p₄}
hp₂p₁ : p₂ ≠ p₁
hp₂p₄ : p₂ ≠ p₄
hp₃p₁ : p₃ ≠ p₁
hp₃p₄ : p₃ ≠ p₄
s : Sphere P
hs : {p₁, p₂, p₃, p₄} ⊆ Metric.sphere s.center s.radius
⊢ 2 • ∡ p₁ p₂ p₄ = 2 • ∡ p₁ p₃ p₄

Tactic:
simp_rw [Set.insert_subset_iff, Set.singleton_subset_iff, Sphere.mem_coe] at hs

Result:
case intro
V : Type u_1
P : Type u_2
inst✝⁴ : NormedAddCommGroup V
inst✝³ : InnerProductSpace ℝ V
inst✝² : MetricSpace P
inst✝¹ : NormedAddTorsor V P
hd2 : Fact (finrank ℝ V = 2)
inst✝ : Oriented ℝ V (Fin 2)
p₁ p₂ p₃ p₄ : P
h : Cospherical {p₁, p₂, p₃, p₄}
hp₂p₁ : p₂ ≠ p₁
hp₂p₄ : p₂ ≠ p₄
hp₃p₁ : p₃ ≠ p₁
hp₃p₄ : p₃ ≠ p₄
s : Sphere P
hs : p₁ ∈ s ∧ p₂ ∈ s ∧ p₃ ∈ s ∧ p₄ ∈ s
⊢ 2 • ∡ p₁ p₂ p₄ = 2 • ∡ p₁ p₃ p₄
-- Mathlib/Combinatorics/SimpleGraph/Connectivity/WalkCounting.lean
theorem reachable_iff_exists_finsetWalkLength_nonempty (u v : V) :
    G.Reachable u v ↔ ∃ n : Fin (Fintype.card V), (G.finsetWalkLength n u v).Nonempty

Proof state:
case mp
V : Type u
G : SimpleGraph V
inst✝² : DecidableEq V
inst✝¹ : Fintype V
inst✝ : DecidableRel G.Adj
u v : V
r : G.Reachable u v
⊢ ∃ n, (G.finsetWalkLength (↑n) u v).Nonempty

Tactic:
refine r.elim_path fun p => ?_

Result:
case mp
V : Type u
G : SimpleGraph V
inst✝² : DecidableEq V
inst✝¹ : Fintype V
inst✝ : DecidableRel G.Adj
u v : V
r : G.Reachable u v
p : G.Path u v
⊢ ∃ n, (G.finsetWalkLength (↑n) u v).Nonempty

Proof state:
case mpr.intro.intro
V : Type u
G : SimpleGraph V
inst✝² : DecidableEq V
inst✝¹ : Fintype V
inst✝ : DecidableRel G.Adj
u v : V
w✝ : Fin (Fintype.card V)
p : G.Walk u v
h✝ : p ∈ G.finsetWalkLength (↑w✝) u v
⊢ G.Reachable u v

Tactic:
exact ⟨p⟩

Result:
no goals

Proof state:
case mp
V : Type u
G : SimpleGraph V
inst✝² : DecidableEq V
inst✝¹ : Fintype V
inst✝ : DecidableRel G.Adj
u v : V
r : G.Reachable u v
p : G.Path u v
⊢ ↑p ∈ G.finsetWalkLength (↑⟨(↑p).length, ⋯⟩) u v

Tactic:
simp [mem_finsetWalkLength_iff]

Result:
no goals

Proof state:
case mp
V : Type u
G : SimpleGraph V
inst✝² : DecidableEq V
inst✝¹ : Fintype V
inst✝ : DecidableRel G.Adj
u v : V
⊢ G.Reachable u v → ∃ n, (G.finsetWalkLength (↑n) u v).Nonempty

Tactic:
intro r

Result:
case mp
V : Type u
G : SimpleGraph V
inst✝² : DecidableEq V
inst✝¹ : Fintype V
inst✝ : DecidableRel G.Adj
u v : V
r : G.Reachable u v
⊢ ∃ n, (G.finsetWalkLength (↑n) u v).Nonempty

Proof state:
V : Type u
G : SimpleGraph V
inst✝² : DecidableEq V
inst✝¹ : Fintype V
inst✝ : DecidableRel G.Adj
u v : V
⊢ G.Reachable u v ↔ ∃ n, (G.finsetWalkLength (↑n) u v).Nonempty

Tactic:
constructor

Result:
case mp
V : Type u
G : SimpleGraph V
inst✝² : DecidableEq V
inst✝¹ : Fintype V
inst✝ : DecidableRel G.Adj
u v : V
⊢ G.Reachable u v → ∃ n, (G.finsetWalkLength (↑n) u v).Nonempty

case mpr
V : Type u
G : SimpleGraph V
inst✝² : DecidableEq V
inst✝¹ : Fintype V
inst✝ : DecidableRel G.Adj
u v : V
⊢ (∃ n, (G.finsetWalkLength (↑n) u v).Nonempty) → G.Reachable u v

Proof state:
case mpr
V : Type u
G : SimpleGraph V
inst✝² : DecidableEq V
inst✝¹ : Fintype V
inst✝ : DecidableRel G.Adj
u v : V
⊢ (∃ n, (G.finsetWalkLength (↑n) u v).Nonempty) → G.Reachable u v

Tactic:
rintro ⟨_, p, _⟩

Result:
case mpr.intro.intro
V : Type u
G : SimpleGraph V
inst✝² : DecidableEq V
inst✝¹ : Fintype V
inst✝ : DecidableRel G.Adj
u v : V
w✝ : Fin (Fintype.card V)
p : G.Walk u v
h✝ : p ∈ G.finsetWalkLength (↑w✝) u v
⊢ G.Reachable u v

Proof state:
case mp
V : Type u
G : SimpleGraph V
inst✝² : DecidableEq V
inst✝¹ : Fintype V
inst✝ : DecidableRel G.Adj
u v : V
r : G.Reachable u v
p : G.Path u v
⊢ ∃ n, (G.finsetWalkLength (↑n) u v).Nonempty

Tactic:
refine ⟨⟨_, p.isPath.length_lt⟩, p, ?_⟩

Result:
case mp
V : Type u
G : SimpleGraph V
inst✝² : DecidableEq V
inst✝¹ : Fintype V
inst✝ : DecidableRel G.Adj
u v : V
r : G.Reachable u v
p : G.Path u v
⊢ ↑p ∈ G.finsetWalkLength (↑⟨(↑p).length, ⋯⟩) u v
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Int/DivModLemmas.lean
theorem fmod_add_fdiv : ∀ a b : Int, a.fmod b + b * a.fdiv b = a
  | 0, ofNat _ | 0, -[_+1] => congrArg ofNat <| by simp
  | succ _, ofNat _ => congrArg ofNat <| Nat.mod_add_div ..
  | succ m, -[n+1] => by
    show subNatNat (m % succ n) n + (↑(succ n * (m / succ n)) + n + 1) = (m + 1)
    rw [Int.add_comm _ n, ← Int.add_assoc, ← Int.add_assoc,
      Int.subNatNat_eq_coe, Int.sub_add_cancel]
    exact congrArg (ofNat · + 1) <| Nat.mod_add_div ..
  | -[_+1], 0 => by rw [fmod_zero]; rfl
  | -[m+1], succ n => by
    show subNatNat .. - (↑(succ n * (m / succ n)) + ↑(succ n)) = -↑(succ m)
    rw [Int.subNatNat_eq_coe, ← Int.sub_sub, ← Int.neg_sub, Int.sub_sub, Int.sub_sub_self]
    exact congrArg (-ofNat ·) <| Nat.succ_add .. ▸ Nat.mod_add_div .. ▸ rfl
  | -[m+1], -[n+1] => by
    show -(↑(succ m % succ n) : Int) + -↑(succ n * (succ m / succ n)) = -↑(succ m)
    rw [← Int.neg_add]; exact congrArg (-ofNat ·) <| Nat.mod_add_div ..

Proof state:
a✝ : Nat
⊢ -[a✝+1] + 0 * -[a✝+1].fdiv 0 = -[a✝+1]

Tactic:
rfl

Result:
no goals

Proof state:
m n : Nat
⊢ -[m+1].fmod -[n+1] + -[n+1] * -[m+1].fdiv -[n+1] = -[m+1]

Tactic:
show -(↑(succ m % succ n) : Int) + -↑(succ n * (succ m / succ n)) = -↑(succ m)

Result:
m n : Nat
⊢ -↑(m.succ % n.succ) + -↑(n.succ * (m.succ / n.succ)) = -↑m.succ

Proof state:
m n : Nat
⊢ subNatNat n.succ (m % n.succ).succ - (↑(n.succ * (m / n.succ)) + ↑n.succ) = -↑m.succ

Tactic:
rw [Int.subNatNat_eq_coe, ← Int.sub_sub, ← Int.neg_sub, Int.sub_sub, Int.sub_sub_self]

Result:
m n : Nat
⊢ -(↑(m % n.succ).succ + ↑(n.succ * (m / n.succ))) = -↑m.succ

Proof state:
m n : Nat
⊢ -↑(m.succ % n.succ) + -↑(n.succ * (m.succ / n.succ)) = -↑m.succ

Tactic:
rw [← Int.neg_add]

Result:
m n : Nat
⊢ -(↑(m.succ % n.succ) + ↑(n.succ * (m.succ / n.succ))) = -↑m.succ

Proof state:
m n : Nat
⊢ -[m+1].fmod ↑n.succ + ↑n.succ * -[m+1].fdiv ↑n.succ = -[m+1]

Tactic:
show subNatNat .. - (↑(succ n * (m / succ n)) + ↑(succ n)) = -↑(succ m)

Result:
m n : Nat
⊢ subNatNat n.succ (m % n.succ).succ - (↑(n.succ * (m / n.succ)) + ↑n.succ) = -↑m.succ

Proof state:
m n : Nat
⊢ (↑m.succ).fmod -[n+1] + -[n+1] * (↑m.succ).fdiv -[n+1] = ↑m.succ

Tactic:
show subNatNat (m % succ n) n + (↑(succ n * (m / succ n)) + n + 1) = (m + 1)

Result:
m n : Nat
⊢ subNatNat (m % n.succ) n + (↑(n.succ * (m / n.succ)) + ↑n + 1) = ↑m + 1

Proof state:
m n : Nat
⊢ subNatNat (m % n.succ) n + (↑(n.succ * (m / n.succ)) + ↑n + 1) = ↑m + 1

Tactic:
rw [Int.add_comm _ n, ← Int.add_assoc, ← Int.add_assoc,
  Int.subNatNat_eq_coe, Int.sub_add_cancel]

Result:
m n : Nat
⊢ ↑(m % n.succ) + ↑(n.succ * (m / n.succ)) + 1 = ↑m + 1

Proof state:
a✝ : Nat
⊢ -[a✝+1].fmod 0 + 0 * -[a✝+1].fdiv 0 = -[a✝+1]

Tactic:
rw [fmod_zero]

Result:
a✝ : Nat
⊢ -[a✝+1] + 0 * -[a✝+1].fdiv 0 = -[a✝+1]

Proof state:
a✝ : Nat
⊢ 0 + 0 = 0

Tactic:
simp

Result:
no goals
-- Mathlib/RingTheory/Norm/Transitivity.lean
lemma auxMat_toSquareBlock_ne : (auxMat M k).toSquareBlock (· ≠ k) True = M k k • 1

Proof state:
case a
S : Type u_2
m : Type u_5
inst✝¹ : CommRing S
M : Matrix m m S
inst✝ : DecidableEq m
k : m
i j : { a // (a ≠ k) = True }
⊢ (auxMat M k).toSquareBlock (fun x => x ≠ k) True i j = (M k k • 1) i j

Tactic:
simp [auxMat, toSquareBlock_def, if_neg (of_eq_true i.2), if_neg (of_eq_true j.2),
  Matrix.one_apply, Subtype.ext_iff]

Result:
no goals

Proof state:
S : Type u_2
m : Type u_5
inst✝¹ : CommRing S
M : Matrix m m S
inst✝ : DecidableEq m
k : m
⊢ (auxMat M k).toSquareBlock (fun x => x ≠ k) True = M k k • 1

Tactic:
ext i j

Result:
case a
S : Type u_2
m : Type u_5
inst✝¹ : CommRing S
M : Matrix m m S
inst✝ : DecidableEq m
k : m
i j : { a // (a ≠ k) = True }
⊢ (auxMat M k).toSquareBlock (fun x => x ≠ k) True i j = (M k k • 1) i j
-- Mathlib/Algebra/Ring/Basic.lean
lemma one_div_neg_one_eq_neg_one : (1 : R) / -1 = -1 :=
  have : -1 * -1 = (1 : R)

Proof state:
R : Type u_1
inst✝¹ : DivisionMonoid R
inst✝ : HasDistribNeg R
⊢ -1 * -1 = 1

Tactic:
rw [neg_mul_neg, one_mul]

Result:
no goals