harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/List/Nat/Range.lean
theorem pairwise_lt_range' s n (step := 1) (pos : 0 < step

Proof state:
s✝ n✝ : Nat
step✝ : optParam Nat 1
pos✝ : autoParam (0 < step✝) _auto✝
s n : Nat
step : optParam Nat 1
pos : autoParam (0 < step) _auto✝
⊢ (∀ (a' : Nat), a' ∈ range' (s + step) n step → s < a') ∧ Pairwise (fun x1 x2 => x1 < x2) (range' (s + step) n step)

Tactic:
constructor

Result:
case left
s✝ n✝ : Nat
step✝ : optParam Nat 1
pos✝ : autoParam (0 < step✝) _auto✝
s n : Nat
step : optParam Nat 1
pos : autoParam (0 < step) _auto✝
⊢ ∀ (a' : Nat), a' ∈ range' (s + step) n step → s < a'

case right
s✝ n✝ : Nat
step✝ : optParam Nat 1
pos✝ : autoParam (0 < step✝) _auto✝
s n : Nat
step : optParam Nat 1
pos : autoParam (0 < step) _auto✝
⊢ Pairwise (fun x1 x2 => x1 < x2) (range' (s + step) n step)

Proof state:
case left
s✝ n✝¹ : Nat
step✝ : optParam Nat 1
pos✝ : autoParam (0 < step✝) _auto✝
s n✝ : Nat
step : optParam Nat 1
pos : autoParam (0 < step) _auto✝
n : Nat
m : n ∈ range' (s + step) n✝ step
⊢ s < n

Tactic:
rw [mem_range'] at m

Result:
case left
s✝ n✝¹ : Nat
step✝ : optParam Nat 1
pos✝ : autoParam (0 < step✝) _auto✝
s n✝ : Nat
step : optParam Nat 1
pos : autoParam (0 < step) _auto✝
n : Nat
m : ∃ i, i < n✝ ∧ n = s + step + step * i
⊢ s < n

Proof state:
case right
s✝ n✝ : Nat
step✝ : optParam Nat 1
pos✝ : autoParam (0 < step✝) _auto✝
s n : Nat
step : optParam Nat 1
pos : autoParam (0 < step) _auto✝
⊢ Pairwise (fun x1 x2 => x1 < x2) (range' (s + step) n step)

Tactic:
exact pairwise_lt_range' (s + step) n step pos

Result:
no goals

Proof state:
case left
s✝ n✝ : Nat
step✝ : optParam Nat 1
pos✝ : autoParam (0 < step✝) _auto✝
s n : Nat
step : optParam Nat 1
pos : autoParam (0 < step) _auto✝
⊢ ∀ (a' : Nat), a' ∈ range' (s + step) n step → s < a'

Tactic:
intros n m

Result:
case left
s✝ n✝¹ : Nat
step✝ : optParam Nat 1
pos✝ : autoParam (0 < step✝) _auto✝
s n✝ : Nat
step : optParam Nat 1
pos : autoParam (0 < step) _auto✝
n : Nat
m : n ∈ range' (s + step) n✝ step
⊢ s < n

Proof state:
case left
s✝ n✝¹ : Nat
step✝ : optParam Nat 1
pos✝ : autoParam (0 < step✝) _auto✝
s n✝ : Nat
step : optParam Nat 1
pos : autoParam (0 < step) _auto✝
n : Nat
m : ∃ i, i < n✝ ∧ n = s + step + step * i
⊢ s < n

Tactic:
omega

Result:
no goals

Proof state:
s✝ n✝ : Nat
step✝ : optParam Nat 1
pos✝ : autoParam (0 < step✝) _auto✝
s n : Nat
step : optParam Nat 1
pos : autoParam (0 < step) _auto✝
⊢ Pairwise (fun x1 x2 => x1 < x2) (range' s (n + 1) step)

Tactic:
simp only [range'_succ, pairwise_cons]

Result:
s✝ n✝ : Nat
step✝ : optParam Nat 1
pos✝ : autoParam (0 < step✝) _auto✝
s n : Nat
step : optParam Nat 1
pos : autoParam (0 < step) _auto✝
⊢ (∀ (a' : Nat), a' ∈ range' (s + step) n step → s < a') ∧ Pairwise (fun x1 x2 => x1 < x2) (range' (s + step) n step)
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Nat/Log2.lean
theorem log2_terminates : ∀ n, n ≥ 2 → n / 2 < n
  | 2, _ => by decide
  | 3, _ => by decide
  | n+4, _ => by
    rw [div_eq, if_pos]
    refine succ_lt_succ (Nat.lt_trans ?_ (lt_succ_self _))
    exact log2_terminates (n+2) (by simp)
    simp

Proof state:
case hc
n : Nat
x✝ : n + 4 ≥ 2
⊢ 0 < 2 ∧ 2 ≤ n + 4

Tactic:
simp

Result:
no goals

Proof state:
n : Nat
x✝ : n + 4 ≥ 2
⊢ (n + 4 - 2) / 2 < n + 2

case hc
n : Nat
x✝ : n + 4 ≥ 2
⊢ 0 < 2 ∧ 2 ≤ n + 4

Tactic:
exact log2_terminates (n+2) (by simp)

Result:
case hc
n : Nat
x✝ : n + 4 ≥ 2
⊢ 0 < 2 ∧ 2 ≤ n + 4

Proof state:
x✝ : 2 ≥ 2
⊢ 2 / 2 < 2

Tactic:
decide

Result:
no goals

Proof state:
n : Nat
x✝ : n + 4 ≥ 2
⊢ (n + 4) / 2 < n + 4

Tactic:
rw [div_eq, if_pos]

Result:
n : Nat
x✝ : n + 4 ≥ 2
⊢ (n + 4 - 2) / 2 + 1 < n + 4

case hc
n : Nat
x✝ : n + 4 ≥ 2
⊢ 0 < 2 ∧ 2 ≤ n + 4

Proof state:
n : Nat
x✝ : n + 4 ≥ 2
⊢ n + 2 ≥ 2

Tactic:
simp

Result:
no goals

Proof state:
n : Nat
x✝ : n + 4 ≥ 2
⊢ (n + 4 - 2) / 2 + 1 < n + 4

case hc
n : Nat
x✝ : n + 4 ≥ 2
⊢ 0 < 2 ∧ 2 ≤ n + 4

Tactic:
refine succ_lt_succ (Nat.lt_trans ?_ (lt_succ_self _))

Result:
n : Nat
x✝ : n + 4 ≥ 2
⊢ (n + 4 - 2) / 2 < n + 2

case hc
n : Nat
x✝ : n + 4 ≥ 2
⊢ 0 < 2 ∧ 2 ≤ n + 4

Proof state:
x✝ : 3 ≥ 2
⊢ 3 / 2 < 3

Tactic:
decide

Result:
no goals
-- Mathlib/Data/Matrix/Basis.lean
theorem diag_same : diag (stdBasisMatrix i i c) = Pi.single i c

Proof state:
case pos
n : Type u_3
α : Type u_5
inst✝¹ : DecidableEq n
inst✝ : Zero α
i : n
c : α
j : n
hij : i = j
⊢ (stdBasisMatrix i i c).diag j = Pi.single i c j

Tactic:
try rw [hij]

Result:
case pos
n : Type u_3
α : Type u_5
inst✝¹ : DecidableEq n
inst✝ : Zero α
i : n
c : α
j : n
hij : i = j
⊢ (stdBasisMatrix j j c).diag j = Pi.single j c j

Proof state:
case h
n : Type u_3
α : Type u_5
inst✝¹ : DecidableEq n
inst✝ : Zero α
i : n
c : α
j : n
⊢ (stdBasisMatrix i i c).diag j = Pi.single i c j

Tactic:
by_cases hij : i = j <;> (try rw [hij]) <;> simp [hij]

Result:
no goals

Proof state:
n : Type u_3
α : Type u_5
inst✝¹ : DecidableEq n
inst✝ : Zero α
i : n
c : α
⊢ (stdBasisMatrix i i c).diag = Pi.single i c

Tactic:
ext j

Result:
case h
n : Type u_3
α : Type u_5
inst✝¹ : DecidableEq n
inst✝ : Zero α
i : n
c : α
j : n
⊢ (stdBasisMatrix i i c).diag j = Pi.single i c j

Proof state:
case pos
n : Type u_3
α : Type u_5
inst✝¹ : DecidableEq n
inst✝ : Zero α
i : n
c : α
j : n
hij : i = j
⊢ (stdBasisMatrix i i c).diag j = Pi.single i c j

Tactic:
rw [hij]

Result:
case pos
n : Type u_3
α : Type u_5
inst✝¹ : DecidableEq n
inst✝ : Zero α
i : n
c : α
j : n
hij : i = j
⊢ (stdBasisMatrix j j c).diag j = Pi.single j c j
-- Mathlib/Data/Matrix/RowCol.lean
theorem col_add [Add α] (v w : m → α) : col ι (v + w) = col ι v + col ι w

Proof state:
case a
m : Type u_2
α : Type v
ι : Type u_6
inst✝ : Add α
v w : m → α
i✝ : m
j✝ : ι
⊢ col ι (v + w) i✝ j✝ = (col ι v + col ι w) i✝ j✝

Tactic:
rfl

Result:
no goals

Proof state:
m : Type u_2
α : Type v
ι : Type u_6
inst✝ : Add α
v w : m → α
⊢ col ι (v + w) = col ι v + col ι w

Tactic:
ext

Result:
case a
m : Type u_2
α : Type v
ι : Type u_6
inst✝ : Add α
v w : m → α
i✝ : m
j✝ : ι
⊢ col ι (v + w) i✝ j✝ = (col ι v + col ι w) i✝ j✝
-- Mathlib/Geometry/Euclidean/Basic.lean
theorem orthogonalProjection_vsub_orthogonalProjection (s : AffineSubspace ℝ P) [Nonempty s]
    [HasOrthogonalProjection s.direction] (p : P) :
    _root_.orthogonalProjection s.direction (p -ᵥ orthogonalProjection s p) = 0

Proof state:
V : Type u_1
P : Type u_2
inst✝⁵ : NormedAddCommGroup V
inst✝⁴ : InnerProductSpace ℝ V
inst✝³ : MetricSpace P
inst✝² : NormedAddTorsor V P
s : AffineSubspace ℝ P
inst✝¹ : Nonempty ↥s
inst✝ : HasOrthogonalProjection s.direction
p : P
⊢ (_root_.orthogonalProjection s.direction) (p -ᵥ ↑((orthogonalProjection s) p)) = 0

Tactic:
apply orthogonalProjection_mem_subspace_orthogonalComplement_eq_zero

Result:
case hv
V : Type u_1
P : Type u_2
inst✝⁵ : NormedAddCommGroup V
inst✝⁴ : InnerProductSpace ℝ V
inst✝³ : MetricSpace P
inst✝² : NormedAddTorsor V P
s : AffineSubspace ℝ P
inst✝¹ : Nonempty ↥s
inst✝ : HasOrthogonalProjection s.direction
p : P
⊢ p -ᵥ ↑((orthogonalProjection s) p) ∈ s.directionᗮ

Proof state:
case hv
V : Type u_1
P : Type u_2
inst✝⁵ : NormedAddCommGroup V
inst✝⁴ : InnerProductSpace ℝ V
inst✝³ : MetricSpace P
inst✝² : NormedAddTorsor V P
s : AffineSubspace ℝ P
inst✝¹ : Nonempty ↥s
inst✝ : HasOrthogonalProjection s.direction
p : P
⊢ p -ᵥ ↑((orthogonalProjection s) p) ∈ s.directionᗮ

Tactic:
intro c hc

Result:
case hv
V : Type u_1
P : Type u_2
inst✝⁵ : NormedAddCommGroup V
inst✝⁴ : InnerProductSpace ℝ V
inst✝³ : MetricSpace P
inst✝² : NormedAddTorsor V P
s : AffineSubspace ℝ P
inst✝¹ : Nonempty ↥s
inst✝ : HasOrthogonalProjection s.direction
p : P
c : V
hc : c ∈ s.direction
⊢ inner c (p -ᵥ ↑((orthogonalProjection s) p)) = 0

Proof state:
case hv
V : Type u_1
P : Type u_2
inst✝⁵ : NormedAddCommGroup V
inst✝⁴ : InnerProductSpace ℝ V
inst✝³ : MetricSpace P
inst✝² : NormedAddTorsor V P
s : AffineSubspace ℝ P
inst✝¹ : Nonempty ↥s
inst✝ : HasOrthogonalProjection s.direction
p : P
c : V
hc : c ∈ s.direction
⊢ inner c (p -ᵥ ↑((orthogonalProjection s) p)) = 0

Tactic:
rw [← neg_vsub_eq_vsub_rev, inner_neg_right,
  orthogonalProjection_vsub_mem_direction_orthogonal s p c hc, neg_zero]

Result:
no goals
-- Mathlib/RingTheory/Spectrum/Prime/Basic.lean
theorem mem_compl_zeroLocus_iff_not_mem {f : R} {I : PrimeSpectrum R} :
    I ∈ (zeroLocus {f} : Set (PrimeSpectrum R))ᶜ ↔ f ∉ I.asIdeal

Proof state:
R : Type u
inst✝ : CommSemiring R
f : R
I : PrimeSpectrum R
⊢ I ∈ (zeroLocus {f})ᶜ ↔ f ∉ I.asIdeal

Tactic:
rw [Set.mem_compl_iff, mem_zeroLocus, Set.singleton_subset_iff]

Result:
R : Type u
inst✝ : CommSemiring R
f : R
I : PrimeSpectrum R
⊢ f ∉ ↑I.asIdeal ↔ f ∉ I.asIdeal

Proof state:
R : Type u
inst✝ : CommSemiring R
f : R
I : PrimeSpectrum R
⊢ f ∉ ↑I.asIdeal ↔ f ∉ I.asIdeal

Tactic:
rfl

Result:
no goals
-- Mathlib/Data/List/DropRight.lean
theorem rdrop_concat_succ (x : α) : rdrop (l ++ [x]) (n + 1) = rdrop l n

Proof state:
α : Type u_1
l : List α
n : ℕ
x : α
⊢ (l ++ [x]).rdrop (n + 1) = l.rdrop n

Tactic:
simp [rdrop_eq_reverse_drop_reverse]

Result:
no goals
-- Mathlib/RingTheory/Algebraic/Integral.lean
protected lemma mul : IsAlgebraic R (a * b)

Proof state:
R : Type u_1
S : Type u_2
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
nzd : NoZeroDivisors R
a b : S
ha : IsAlgebraic R a
hb : IsAlgebraic R b
ra : R
a0 : ra ≠ 0
int_a : IsIntegral R (ra • a)
⊢ IsAlgebraic R (a * b)

Tactic:
have ⟨rb, b0, int_b⟩ := hb.exists_integral_multiple

Result:
R : Type u_1
S : Type u_2
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
nzd : NoZeroDivisors R
a b : S
ha : IsAlgebraic R a
hb : IsAlgebraic R b
ra : R
a0 : ra ≠ 0
int_a : IsIntegral R (ra • a)
rb : R
b0 : rb ≠ 0
int_b : IsIntegral R (rb • b)
⊢ IsAlgebraic R (a * b)

Proof state:
R : Type u_1
S : Type u_2
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
nzd : NoZeroDivisors R
a b : S
ha : IsAlgebraic R a
hb : IsAlgebraic R b
ra : R
a0 : ra ≠ 0
int_a : IsIntegral R (ra • a)
rb : R
b0 : rb ≠ 0
int_b : IsIntegral R (rb • b)
⊢ IsIntegral R ((ra * rb) • (a * b))

Tactic:
simp_rw [Algebra.smul_def, map_mul, mul_mul_mul_comm, ← Algebra.smul_def]

Result:
R : Type u_1
S : Type u_2
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
nzd : NoZeroDivisors R
a b : S
ha : IsAlgebraic R a
hb : IsAlgebraic R b
ra : R
a0 : ra ≠ 0
int_a : IsIntegral R (ra • a)
rb : R
b0 : rb ≠ 0
int_b : IsIntegral R (rb • b)
⊢ IsIntegral R (ra • a * rb • b)

Proof state:
R : Type u_1
S : Type u_2
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
nzd : NoZeroDivisors R
a b : S
ha : IsAlgebraic R a
hb : IsAlgebraic R b
ra : R
a0 : ra ≠ 0
int_a : IsIntegral R (ra • a)
rb : R
b0 : rb ≠ 0
int_b : IsIntegral R (rb • b)
⊢ IsAlgebraic R (a * b)

Tactic:
refine IsAlgebraic.iff_exists_smul_integral.mpr ⟨_, mul_ne_zero a0 b0, ?_⟩

Result:
R : Type u_1
S : Type u_2
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
nzd : NoZeroDivisors R
a b : S
ha : IsAlgebraic R a
hb : IsAlgebraic R b
ra : R
a0 : ra ≠ 0
int_a : IsIntegral R (ra • a)
rb : R
b0 : rb ≠ 0
int_b : IsIntegral R (rb • b)
⊢ IsIntegral R ((ra * rb) • (a * b))

Proof state:
R : Type u_1
S : Type u_2
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
nzd : NoZeroDivisors R
a b : S
ha : IsAlgebraic R a
hb : IsAlgebraic R b
⊢ IsAlgebraic R (a * b)

Tactic:
have ⟨ra, a0, int_a⟩ := ha.exists_integral_multiple

Result:
R : Type u_1
S : Type u_2
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
nzd : NoZeroDivisors R
a b : S
ha : IsAlgebraic R a
hb : IsAlgebraic R b
ra : R
a0 : ra ≠ 0
int_a : IsIntegral R (ra • a)
⊢ IsAlgebraic R (a * b)

Proof state:
R : Type u_1
S : Type u_2
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
nzd : NoZeroDivisors R
a b : S
ha : IsAlgebraic R a
hb : IsAlgebraic R b
ra : R
a0 : ra ≠ 0
int_a : IsIntegral R (ra • a)
rb : R
b0 : rb ≠ 0
int_b : IsIntegral R (rb • b)
⊢ IsIntegral R (ra • a * rb • b)

Tactic:
exact int_a.mul int_b

Result:
no goals
-- Mathlib/MeasureTheory/PiSystem.lean
theorem IsPiSystem.insert_univ {S : Set (Set α)} (h_pi : IsPiSystem S) :
    IsPiSystem (insert Set.univ S)

Proof state:
α : Type u_1
S : Set (Set α)
h_pi : IsPiSystem S
⊢ IsPiSystem (insert univ S)

Tactic:
intro s hs t ht hst

Result:
α : Type u_1
S : Set (Set α)
h_pi : IsPiSystem S
s : Set α
hs : s ∈ insert univ S
t : Set α
ht : t ∈ insert univ S
hst : (s ∩ t).Nonempty
⊢ s ∩ t ∈ insert univ S

Proof state:
case inr.inl
α : Type u_1
S : Set (Set α)
h_pi : IsPiSystem S
s t : Set α
hst : (s ∩ t).Nonempty
hs : s ∈ S
ht : t = univ
⊢ s ∩ t ∈ insert univ S

Tactic:
simp [hs, ht]

Result:
no goals

Proof state:
α : Type u_1
S : Set (Set α)
h_pi : IsPiSystem S
s : Set α
hs : s ∈ insert univ S
t : Set α
ht : t ∈ insert univ S
hst : (s ∩ t).Nonempty
⊢ s ∩ t ∈ insert univ S

Tactic:
rcases hs with hs | hs

Result:
case inl
α : Type u_1
S : Set (Set α)
h_pi : IsPiSystem S
s t : Set α
ht : t ∈ insert univ S
hst : (s ∩ t).Nonempty
hs : s = univ
⊢ s ∩ t ∈ insert univ S

case inr
α : Type u_1
S : Set (Set α)
h_pi : IsPiSystem S
s t : Set α
ht : t ∈ insert univ S
hst : (s ∩ t).Nonempty
hs : s ∈ S
⊢ s ∩ t ∈ insert univ S

Proof state:
case inr.inr
α : Type u_1
S : Set (Set α)
h_pi : IsPiSystem S
s t : Set α
hst : (s ∩ t).Nonempty
hs : s ∈ S
ht : t ∈ S
⊢ s ∩ t ∈ insert univ S

Tactic:
exact Set.mem_insert_of_mem _ (h_pi s hs t ht hst)

Result:
no goals

Proof state:
case inr
α : Type u_1
S : Set (Set α)
h_pi : IsPiSystem S
s t : Set α
ht : t ∈ insert univ S
hst : (s ∩ t).Nonempty
hs : s ∈ S
⊢ s ∩ t ∈ insert univ S

Tactic:
rcases ht with ht | ht

Result:
case inr.inl
α : Type u_1
S : Set (Set α)
h_pi : IsPiSystem S
s t : Set α
hst : (s ∩ t).Nonempty
hs : s ∈ S
ht : t = univ
⊢ s ∩ t ∈ insert univ S

case inr.inr
α : Type u_1
S : Set (Set α)
h_pi : IsPiSystem S
s t : Set α
hst : (s ∩ t).Nonempty
hs : s ∈ S
ht : t ∈ S
⊢ s ∩ t ∈ insert univ S

Proof state:
case inl
α : Type u_1
S : Set (Set α)
h_pi : IsPiSystem S
s t : Set α
ht : t ∈ insert univ S
hst : (s ∩ t).Nonempty
hs : s = univ
⊢ s ∩ t ∈ insert univ S

Tactic:
rcases ht with ht | ht <;> simp [hs, ht]

Result:
no goals
-- Mathlib/Topology/MetricSpace/Pseudo/Defs.lean
theorem Real.Icc_eq_closedBall (x y : ℝ) : Icc x y = closedBall ((x + y) / 2) ((y - x) / 2)

Proof state:
x y : ℝ
⊢ Icc x y = closedBall ((x + y) / 2) ((y - x) / 2)

Tactic:
rw [Real.closedBall_eq_Icc, ← sub_div, add_comm, ← sub_add, add_sub_cancel_left, add_self_div_two,
  ← add_div, add_assoc, add_sub_cancel, add_self_div_two]

Result:
no goals
-- Mathlib/Logic/Denumerable.lean
theorem le_succ_of_forall_lt_le {x y : s} (h : ∀ z < x, z ≤ y) : x ≤ succ y :=
  have hx : ∃ m, (y : ℕ) + m + 1 ∈ s := exists_succ _
  show (x : ℕ) ≤ (y : ℕ) + Nat.find hx + 1 from
    le_of_not_gt fun hxy =>
      (h ⟨_, Nat.find_spec hx⟩ hxy).not_lt <|
        (by omega : (y : ℕ) < (y : ℕ) + Nat.find hx + 1)

Proof state:
s : Set ℕ
inst✝¹ : Infinite ↑s
inst✝ : DecidablePred fun x => x ∈ s
x y : ↑s
h : ∀ z < x, z ≤ y
hx : ∃ m, ↑y + m + 1 ∈ s
hxy : ↑x > ↑y + Nat.find hx + 1
⊢ ↑y < ↑y + Nat.find hx + 1

Tactic:
omega

Result:
no goals
-- Mathlib/LinearAlgebra/TensorProduct/Basic.lean
theorem rTensor_pow (f : M ≃ₗ[R] M) (n : ℕ) : f.rTensor N ^ n = (f ^ n).rTensor N

Proof state:
R : Type u_1
inst✝⁴ : CommSemiring R
M : Type u_5
N : Type u_6
inst✝³ : AddCommMonoid M
inst✝² : AddCommMonoid N
inst✝¹ : Module R M
inst✝ : Module R N
f : M ≃ₗ[R] M
n : ℕ
⊢ rTensor N f ^ n = rTensor N (f ^ n)

Tactic:
simpa only [one_pow] using TensorProduct.congr_pow f (1 : N ≃ₗ[R] N) n

Result:
no goals
-- Mathlib/LinearAlgebra/CliffordAlgebra/Equivs.lean
theorem ofComplex_conj (c : ℂ) : ofComplex (conj c) = involute (ofComplex c) :=
  CliffordAlgebraComplex.equiv.injective <| by
    rw [equiv_apply, equiv_apply, toComplex_involute, toComplex_ofComplex, toComplex_ofComplex]

Proof state:
c : ℂ
⊢ CliffordAlgebraComplex.equiv (ofComplex ((starRingEnd ℂ) c)) = CliffordAlgebraComplex.equiv (involute (ofComplex c))

Tactic:
rw [equiv_apply, equiv_apply, toComplex_involute, toComplex_ofComplex, toComplex_ofComplex]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Array/Range.lean
theorem range_succ (n : Nat) : range (succ n) = range n ++ #[n]

Proof state:
case h₂
n i : Nat
h₁✝ : i < (range n.succ).size
h₂ : i < (range n ++ #[n]).size
h₁ : i < n + 1
⊢ (range n.succ)[i] = (range n ++ #[n])[i]

Tactic:
simp only [succ_eq_add_one, getElem_range, append_singleton, getElem_push, size_range,
  dite_eq_ite]

Result:
case h₂
n i : Nat
h₁✝ : i < (range n.succ).size
h₂ : i < (range n ++ #[n]).size
h₁ : i < n + 1
⊢ i = if i < n then i else n

Proof state:
case h₂
n i : Nat
h₁✝ : i < (range n.succ).size
h₂ : i < (range n ++ #[n]).size
h₁ : i < n + 1
⊢ i = if i < n then i else n

Tactic:
split <;> omega

Result:
no goals

Proof state:
case h₁
n : Nat
⊢ (range n.succ).size = (range n ++ #[n]).size

Tactic:
simp

Result:
no goals

Proof state:
n : Nat
⊢ range n.succ = range n ++ #[n]

Tactic:
ext i h₁ h₂

Result:
case h₁
n : Nat
⊢ (range n.succ).size = (range n ++ #[n]).size

case h₂
n i : Nat
h₁ : i < (range n.succ).size
h₂ : i < (range n ++ #[n]).size
⊢ (range n.succ)[i] = (range n ++ #[n])[i]

Proof state:
case h₂
n i : Nat
h₁ : i < (range n.succ).size
h₂ : i < (range n ++ #[n]).size
⊢ (range n.succ)[i] = (range n ++ #[n])[i]

Tactic:
simp only [succ_eq_add_one, size_range] at h₁

Result:
case h₂
n i : Nat
h₁✝ : i < (range n.succ).size
h₂ : i < (range n ++ #[n]).size
h₁ : i < n + 1
⊢ (range n.succ)[i] = (range n ++ #[n])[i]
-- Mathlib/.lake/packages/lean4/src/lean/Std/Sat/AIG/CNF.lean
theorem State.unsat_def (state : State aig) :
    state.Unsat ↔ state.cnf.Unsat

Proof state:
aig : AIG Nat
state : State aig
⊢ state.Unsat ↔ state.cnf.Unsat

Tactic:
rfl

Result:
no goals
-- Mathlib/Algebra/Polynomial/Reverse.lean
theorem reflect_support (N : ℕ) (f : R[X]) :
    (reflect N f).support = Finset.image (revAt N) f.support

Proof state:
case ofFinsupp
R : Type u_1
inst✝ : Semiring R
N : ℕ
toFinsupp✝ : AddMonoidAlgebra R ℕ
⊢ (reflect N { toFinsupp := toFinsupp✝ }).support = image ⇑(revAt N) { toFinsupp := toFinsupp✝ }.support

Tactic:
ext1

Result:
case ofFinsupp.h
R : Type u_1
inst✝ : Semiring R
N : ℕ
toFinsupp✝ : AddMonoidAlgebra R ℕ
a✝ : ℕ
⊢ a✝ ∈ (reflect N { toFinsupp := toFinsupp✝ }).support ↔ a✝ ∈ image ⇑(revAt N) { toFinsupp := toFinsupp✝ }.support

Proof state:
R : Type u_1
inst✝ : Semiring R
N : ℕ
f : R[X]
⊢ (reflect N f).support = image (⇑(revAt N)) f.support

Tactic:
rcases f with ⟨⟩

Result:
case ofFinsupp
R : Type u_1
inst✝ : Semiring R
N : ℕ
toFinsupp✝ : AddMonoidAlgebra R ℕ
⊢ (reflect N { toFinsupp := toFinsupp✝ }).support = image ⇑(revAt N) { toFinsupp := toFinsupp✝ }.support

Proof state:
case ofFinsupp.h
R : Type u_1
inst✝ : Semiring R
N : ℕ
toFinsupp✝ : AddMonoidAlgebra R ℕ
a✝ : ℕ
⊢ a✝ ∈ (reflect N { toFinsupp := toFinsupp✝ }).support ↔ a✝ ∈ image ⇑(revAt N) { toFinsupp := toFinsupp✝ }.support

Tactic:
simp only [reflect, support_ofFinsupp, support_embDomain, Finset.mem_map, Finset.mem_image]

Result:
no goals
-- Mathlib/Data/Stream/Init.lean
theorem tail_const (a : α) : tail (const a) = const a :=
  suffices tail (a::const a) = const a by rwa [← const_eq] at this
  rfl

Proof state:
α : Type u
a : α
this : (a :: const a).tail = const a
⊢ (const a).tail = const a

Tactic:
rwa [← const_eq] at this

Result:
no goals
-- Mathlib/Analysis/Analytic/Basic.lean
lemma AnalyticWithinAt.congr_of_eventuallyEq {f g : E → F} {s : Set E} {x : E}
    (hf : AnalyticWithinAt 𝕜 f s x) (hs : g =ᶠ[𝓝[s] x] f) (hx : g x = f x) :
    AnalyticWithinAt 𝕜 g s x

Proof state:
case intro
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst✝⁴ : NontriviallyNormedField 𝕜
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
f g : E → F
s : Set E
x : E
hs : g =ᶠ[𝓝[s] x] f
hx : g x = f x
p : FormalMultilinearSeries 𝕜 E F
hp : HasFPowerSeriesWithinAt f p s x
⊢ AnalyticWithinAt 𝕜 g s x

Tactic:
exact ⟨p, hp.congr hs hx⟩

Result:
no goals

Proof state:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst✝⁴ : NontriviallyNormedField 𝕜
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
f g : E → F
s : Set E
x : E
hf : AnalyticWithinAt 𝕜 f s x
hs : g =ᶠ[𝓝[s] x] f
hx : g x = f x
⊢ AnalyticWithinAt 𝕜 g s x

Tactic:
rcases hf with ⟨p, hp⟩

Result:
case intro
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst✝⁴ : NontriviallyNormedField 𝕜
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
f g : E → F
s : Set E
x : E
hs : g =ᶠ[𝓝[s] x] f
hx : g x = f x
p : FormalMultilinearSeries 𝕜 E F
hp : HasFPowerSeriesWithinAt f p s x
⊢ AnalyticWithinAt 𝕜 g s x
-- Mathlib/Topology/ContinuousOn.lean
theorem continuous_prod_of_discrete_right [DiscreteTopology β] {f : α × β → γ} :
    Continuous f ↔ ∀ b, Continuous (f ⟨·, b⟩)

Proof state:
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝³ : TopologicalSpace α
inst✝² : TopologicalSpace β
inst✝¹ : TopologicalSpace γ
inst✝ : DiscreteTopology β
f : α × β → γ
⊢ Continuous f ↔ ∀ (b : β), Continuous fun x => f (x, b)

Tactic:
simp_rw [continuous_iff_continuousOn_univ]

Result:
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝³ : TopologicalSpace α
inst✝² : TopologicalSpace β
inst✝¹ : TopologicalSpace γ
inst✝ : DiscreteTopology β
f : α × β → γ
⊢ ContinuousOn f univ ↔ ∀ (b : β), ContinuousOn (fun x => f (x, b)) univ

Proof state:
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝³ : TopologicalSpace α
inst✝² : TopologicalSpace β
inst✝¹ : TopologicalSpace γ
inst✝ : DiscreteTopology β
f : α × β → γ
⊢ ContinuousOn f univ ↔ ∀ (b : β), ContinuousOn (fun x => f (x, b)) univ

Tactic:
exact continuousOn_prod_of_discrete_right

Result:
no goals
-- Mathlib/Combinatorics/SimpleGraph/Dart.lean
theorem dart_edge_eq_mk'_iff :
    ∀ {d : G.Dart} {p : V × V}, d.edge = Sym2.mk p ↔ d.toProd = p ∨ d.toProd = p.swap

Proof state:
case mk
V : Type u_1
G : SimpleGraph V
p : V × V
h : G.Adj p.1 p.2
⊢ ∀ {p_1 : V × V},
    { toProd := p, adj := h }.edge = Sym2.mk p_1 ↔
      { toProd := p, adj := h }.toProd = p_1 ∨ { toProd := p, adj := h }.toProd = p_1.swap

Tactic:
apply Sym2.mk_eq_mk_iff

Result:
no goals

Proof state:
V : Type u_1
G : SimpleGraph V
⊢ ∀ {d : G.Dart} {p : V × V}, d.edge = Sym2.mk p ↔ d.toProd = p ∨ d.toProd = p.swap

Tactic:
rintro ⟨p, h⟩

Result:
case mk
V : Type u_1
G : SimpleGraph V
p : V × V
h : G.Adj p.1 p.2
⊢ ∀ {p_1 : V × V},
    { toProd := p, adj := h }.edge = Sym2.mk p_1 ↔
      { toProd := p, adj := h }.toProd = p_1 ∨ { toProd := p, adj := h }.toProd = p_1.swap
-- Mathlib/CategoryTheory/FiberedCategory/Cartesian.lean
@[simp]
lemma map_self : map p f φ (id_comp f).symm φ = 𝟙 a

Proof state:
case map
𝒮 : Type u₁
𝒳 : Type u₂
inst✝² : Category.{v₁, u₁} 𝒮
inst✝¹ : Category.{v₂, u₂} 𝒳
p : 𝒳 ⥤ 𝒮
a✝ b✝ : 𝒳
φ : a✝ ⟶ b✝
R S : 𝒮
a b : 𝒳
inst✝ : p.IsStronglyCartesian (p.map φ) φ
⊢ map p (p.map φ) φ ⋯ φ = 𝟙 a✝

Tactic:
symm

Result:
case map
𝒮 : Type u₁
𝒳 : Type u₂
inst✝² : Category.{v₁, u₁} 𝒮
inst✝¹ : Category.{v₂, u₂} 𝒳
p : 𝒳 ⥤ 𝒮
a✝ b✝ : 𝒳
φ : a✝ ⟶ b✝
R S : 𝒮
a b : 𝒳
inst✝ : p.IsStronglyCartesian (p.map φ) φ
⊢ 𝟙 a✝ = map p (p.map φ) φ ⋯ φ

Proof state:
case map
𝒮 : Type u₁
𝒳 : Type u₂
inst✝² : Category.{v₁, u₁} 𝒮
inst✝¹ : Category.{v₂, u₂} 𝒳
p : 𝒳 ⥤ 𝒮
a✝ b✝ : 𝒳
φ : a✝ ⟶ b✝
R S : 𝒮
a b : 𝒳
inst✝ : p.IsStronglyCartesian (p.map φ) φ
⊢ 𝟙 a✝ = map p (p.map φ) φ ⋯ φ

Tactic:
apply map_uniq

Result:
case map.hψ
𝒮 : Type u₁
𝒳 : Type u₂
inst✝² : Category.{v₁, u₁} 𝒮
inst✝¹ : Category.{v₂, u₂} 𝒳
p : 𝒳 ⥤ 𝒮
a✝ b✝ : 𝒳
φ : a✝ ⟶ b✝
R S : 𝒮
a b : 𝒳
inst✝ : p.IsStronglyCartesian (p.map φ) φ
⊢ 𝟙 a✝ ≫ φ = φ

Proof state:
𝒮 : Type u₁
𝒳 : Type u₂
inst✝² : Category.{v₁, u₁} 𝒮
inst✝¹ : Category.{v₂, u₂} 𝒳
p : 𝒳 ⥤ 𝒮
R S : 𝒮
a b : 𝒳
f : R ⟶ S
φ : a ⟶ b
inst✝ : p.IsStronglyCartesian f φ
⊢ map p f φ ⋯ φ = 𝟙 a

Tactic:
subst_hom_lift p f φ

Result:
case map
𝒮 : Type u₁
𝒳 : Type u₂
inst✝² : Category.{v₁, u₁} 𝒮
inst✝¹ : Category.{v₂, u₂} 𝒳
p : 𝒳 ⥤ 𝒮
a✝ b✝ : 𝒳
φ : a✝ ⟶ b✝
R S : 𝒮
a b : 𝒳
inst✝ : p.IsStronglyCartesian (p.map φ) φ
⊢ map p (p.map φ) φ ⋯ φ = 𝟙 a✝

Proof state:
case map.hψ
𝒮 : Type u₁
𝒳 : Type u₂
inst✝² : Category.{v₁, u₁} 𝒮
inst✝¹ : Category.{v₂, u₂} 𝒳
p : 𝒳 ⥤ 𝒮
a✝ b✝ : 𝒳
φ : a✝ ⟶ b✝
R S : 𝒮
a b : 𝒳
inst✝ : p.IsStronglyCartesian (p.map φ) φ
⊢ 𝟙 a✝ ≫ φ = φ

Tactic:
simp only [id_comp]

Result:
no goals