harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/LinearAlgebra/Finsupp/LinearCombination.lean
theorem linearCombination_comp (f : α' → α) :
    linearCombination R (v ∘ f) = (linearCombination R v).comp (lmapDomain R R f)

Proof state:
case h.h
α : Type u_1
M : Type u_2
R : Type u_5
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
α' : Type u_7
v : α → M
f : α' → α
a✝ : α'
⊢ (linearCombination R (v ∘ f) ∘ₗ lsingle a✝) 1 = ((linearCombination R v ∘ₗ lmapDomain R R f) ∘ₗ lsingle a✝) 1

Tactic:
simp [linearCombination_apply]

Result:
no goals

Proof state:
α : Type u_1
M : Type u_2
R : Type u_5
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
α' : Type u_7
v : α → M
f : α' → α
⊢ linearCombination R (v ∘ f) = linearCombination R v ∘ₗ lmapDomain R R f

Tactic:
ext

Result:
case h.h
α : Type u_1
M : Type u_2
R : Type u_5
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
α' : Type u_7
v : α → M
f : α' → α
a✝ : α'
⊢ (linearCombination R (v ∘ f) ∘ₗ lsingle a✝) 1 = ((linearCombination R v ∘ₗ lmapDomain R R f) ∘ₗ lsingle a✝) 1
-- Mathlib/Geometry/Euclidean/Angle/Unoriented/RightAngle.lean
theorem angle_add_eq_arctan_of_inner_eq_zero {x y : V} (h : ⟪x, y⟫ = 0) (h0 : x ≠ 0) :
    angle x (x + y) = Real.arctan (‖y‖ / ‖x‖)

Proof state:
V : Type u_1
inst✝¹ : NormedAddCommGroup V
inst✝ : InnerProductSpace ℝ V
x y : V
h : inner x y = 0
h0 : x ≠ 0
⊢ Real.arcsin (‖y‖ / √(‖x‖ * ‖x‖ + ‖y‖ * ‖y‖)) = Real.arcsin (‖y‖ / (‖x‖ * √(1 + (‖y‖ / ‖x‖) ^ 2)))

Tactic:
nth_rw 3 [← Real.sqrt_sq (norm_nonneg x)]

Result:
V : Type u_1
inst✝¹ : NormedAddCommGroup V
inst✝ : InnerProductSpace ℝ V
x y : V
h : inner x y = 0
h0 : x ≠ 0
⊢ Real.arcsin (‖y‖ / √(‖x‖ * ‖x‖ + ‖y‖ * ‖y‖)) = Real.arcsin (‖y‖ / (√(‖x‖ ^ 2) * √(1 + (‖y‖ / ‖x‖) ^ 2)))

Proof state:
V : Type u_1
inst✝¹ : NormedAddCommGroup V
inst✝ : InnerProductSpace ℝ V
x y : V
h : inner x y = 0
h0 : x ≠ 0
⊢ Real.arcsin (‖y‖ / √(‖x‖ * ‖x‖ + ‖y‖ * ‖y‖)) = Real.arcsin (‖y‖ / (√(‖x‖ ^ 2) * √(1 + (‖y‖ / ‖x‖) ^ 2)))

Tactic:
rw_mod_cast [← Real.sqrt_mul (sq_nonneg _), div_pow, pow_two, pow_two, mul_add, mul_one, mul_div,
  mul_comm (‖x‖ * ‖x‖), ← mul_div, div_self (mul_self_pos.2 (norm_ne_zero_iff.2 h0)).ne', mul_one]

Result:
no goals

Proof state:
V : Type u_1
inst✝¹ : NormedAddCommGroup V
inst✝ : InnerProductSpace ℝ V
x y : V
h : inner x y = 0
h0 : x ≠ 0
⊢ angle x (x + y) = Real.arctan (‖y‖ / ‖x‖)

Tactic:
rw [angle_add_eq_arcsin_of_inner_eq_zero h (Or.inl h0), Real.arctan_eq_arcsin, ←
  div_mul_eq_div_div, norm_add_eq_sqrt_iff_real_inner_eq_zero.2 h]

Result:
V : Type u_1
inst✝¹ : NormedAddCommGroup V
inst✝ : InnerProductSpace ℝ V
x y : V
h : inner x y = 0
h0 : x ≠ 0
⊢ Real.arcsin (‖y‖ / √(‖x‖ * ‖x‖ + ‖y‖ * ‖y‖)) = Real.arcsin (‖y‖ / (‖x‖ * √(1 + (‖y‖ / ‖x‖) ^ 2)))
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Array/Zip.lean
theorem zip_eq_zipWith (l₁ : Array α) (l₂ : Array β) : zip l₁ l₂ = zipWith Prod.mk l₁ l₂

Proof state:
case mk.mk
α : Type u_1
β : Type u_2
toList✝¹ : List α
toList✝ : List β
⊢ { toList := toList✝¹ }.zip { toList := toList✝ } = zipWith Prod.mk { toList := toList✝¹ } { toList := toList✝ }

Tactic:
simp [List.zip_eq_zipWith]

Result:
no goals

Proof state:
case mk
α : Type u_1
β : Type u_2
l₂ : Array β
toList✝ : List α
⊢ { toList := toList✝ }.zip l₂ = zipWith Prod.mk { toList := toList✝ } l₂

Tactic:
cases l₂

Result:
case mk.mk
α : Type u_1
β : Type u_2
toList✝¹ : List α
toList✝ : List β
⊢ { toList := toList✝¹ }.zip { toList := toList✝ } = zipWith Prod.mk { toList := toList✝¹ } { toList := toList✝ }

Proof state:
α : Type u_1
β : Type u_2
l₁ : Array α
l₂ : Array β
⊢ l₁.zip l₂ = zipWith Prod.mk l₁ l₂

Tactic:
cases l₁

Result:
case mk
α : Type u_1
β : Type u_2
l₂ : Array β
toList✝ : List α
⊢ { toList := toList✝ }.zip l₂ = zipWith Prod.mk { toList := toList✝ } l₂
-- Mathlib/Data/ENat/Lattice.lean
lemma iInf_eq_zero : ⨅ i, (f i : ℕ∞) = 0 ↔ ∃ i, f i = 0

Proof state:
case inr
ι : Sort u_1
f : ι → ℕ
h✝ : Nonempty ι
⊢ ⨅ i, ↑(f i) = 0 ↔ ∃ i, f i = 0

Tactic:
norm_cast

Result:
case inr
ι : Sort u_1
f : ι → ℕ
h✝ : Nonempty ι
⊢ ⨅ i, f i = 0 ↔ ∃ i, f i = 0

Proof state:
case inl
ι : Sort u_1
f : ι → ℕ
h✝ : IsEmpty ι
⊢ ⨅ i, ↑(f i) = 0 ↔ ∃ i, f i = 0

Tactic:
simp

Result:
no goals

Proof state:
ι : Sort u_1
f : ι → ℕ
⊢ ⨅ i, ↑(f i) = 0 ↔ ∃ i, f i = 0

Tactic:
cases isEmpty_or_nonempty ι

Result:
case inl
ι : Sort u_1
f : ι → ℕ
h✝ : IsEmpty ι
⊢ ⨅ i, ↑(f i) = 0 ↔ ∃ i, f i = 0

case inr
ι : Sort u_1
f : ι → ℕ
h✝ : Nonempty ι
⊢ ⨅ i, ↑(f i) = 0 ↔ ∃ i, f i = 0

Proof state:
case inr
ι : Sort u_1
f : ι → ℕ
h✝ : Nonempty ι
⊢ (0 ∈ range fun i => f i) ∨ (range fun i => f i) = ∅ ↔ ∃ i, f i = 0

Tactic:
exact ⟨fun h ↦ by simp_all, .inl⟩

Result:
no goals

Proof state:
case inr
ι : Sort u_1
f : ι → ℕ
h✝ : Nonempty ι
⊢ ⨅ i, f i = 0 ↔ ∃ i, f i = 0

Tactic:
rw [iInf, Nat.sInf_eq_zero]

Result:
case inr
ι : Sort u_1
f : ι → ℕ
h✝ : Nonempty ι
⊢ (0 ∈ range fun i => f i) ∨ (range fun i => f i) = ∅ ↔ ∃ i, f i = 0

Proof state:
ι : Sort u_1
f : ι → ℕ
h✝ : Nonempty ι
h : (0 ∈ range fun i => f i) ∨ (range fun i => f i) = ∅
⊢ ∃ i, f i = 0

Tactic:
simp_all

Result:
no goals
-- Mathlib/Data/Set/NAry.lean
theorem image_image2_distrib {g : γ → δ} {f' : α' → β' → δ} {g₁ : α → α'} {g₂ : β → β'}
    (h_distrib : ∀ a b, g (f a b) = f' (g₁ a) (g₂ b)) :
    (image2 f s t).image g = image2 f' (s.image g₁) (t.image g₂)

Proof state:
α : Type u_1
α' : Type u_2
β : Type u_3
β' : Type u_4
γ : Type u_5
δ : Type u_7
f : α → β → γ
s : Set α
t : Set β
g : γ → δ
f' : α' → β' → δ
g₁ : α → α'
g₂ : β → β'
h_distrib : ∀ (a : α) (b : β), g (f a b) = f' (g₁ a) (g₂ b)
⊢ g '' image2 f s t = image2 f' (g₁ '' s) (g₂ '' t)

Tactic:
simp_rw [image_image2, image2_image_left, image2_image_right, h_distrib]

Result:
no goals
-- Mathlib/RingTheory/Adjoin/Basic.lean
theorem Subalgebra.adjoin_eq_span_basis {ι : Type*} (bL : Basis ι F L) :
    toSubmodule (adjoin E (L : Set K)) = span E (Set.range fun i : ι ↦ (bL i).1) :=
  L.adjoin_eq_span_of_eq_span E <| by
    simpa only [← L.range_val, Submodule.map_span, Submodule.map_top, ← Set.range_comp]
      using congr_arg (Submodule.map L.val) bL.span_eq.symm

Proof state:
F : Type u_1
E : Type u_2
K : Type u_3
inst✝⁶ : CommSemiring E
inst✝⁵ : Semiring K
inst✝⁴ : SMul F E
inst✝³ : Algebra E K
inst✝² : CommSemiring F
inst✝¹ : Algebra F K
inst✝ : IsScalarTower F E K
L : Subalgebra F K
ι : Type u_4
bL : Basis ι F ↥L
⊢ toSubmodule L = span F (Set.range fun i => ↑(bL i))

Tactic:
simpa only [← L.range_val, Submodule.map_span, Submodule.map_top, ← Set.range_comp]
  using congr_arg (Submodule.map L.val) bL.span_eq.symm

Result:
no goals
-- Mathlib/Data/Num/Lemmas.lean
theorem cast_inj [AddMonoidWithOne α] [CharZero α] {m n : PosNum} : (m : α) = n ↔ m = n

Proof state:
α : Type u_1
inst✝¹ : AddMonoidWithOne α
inst✝ : CharZero α
m n : PosNum
⊢ ↑m = ↑n ↔ m = n

Tactic:
rw [← cast_to_nat m, ← cast_to_nat n, Nat.cast_inj, to_nat_inj]

Result:
no goals
-- Mathlib/Data/List/Rotate.lean
theorem cyclicPermutations_of_ne_nil (l : List α) (h : l ≠ []) :
    cyclicPermutations l = dropLast (zipWith (· ++ ·) (tails l) (inits l))

Proof state:
case intro.intro
α : Type u
hd : α
tl : List α
h : hd :: tl ≠ []
⊢ (hd :: tl).cyclicPermutations = (zipWith (fun x1 x2 => x1 ++ x2) (hd :: tl).tails (hd :: tl).inits).dropLast

Tactic:
exact cyclicPermutations_cons _ _

Result:
no goals

Proof state:
α : Type u
l : List α
h : l ≠ []
⊢ l.cyclicPermutations = (zipWith (fun x1 x2 => x1 ++ x2) l.tails l.inits).dropLast

Tactic:
obtain ⟨hd, tl, rfl⟩ := exists_cons_of_ne_nil h

Result:
case intro.intro
α : Type u
hd : α
tl : List α
h : hd :: tl ≠ []
⊢ (hd :: tl).cyclicPermutations = (zipWith (fun x1 x2 => x1 ++ x2) (hd :: tl).tails (hd :: tl).inits).dropLast
-- Mathlib/Analysis/Convex/Deriv.lean
/-- If `f` is convex on `S` and differentiable on `S`, then its derivative within `S` is monotone
on `S`. -/
lemma monotoneOn_derivWithin (hfc : ConvexOn ℝ S f) (hfd : DifferentiableOn ℝ f S) :
    MonotoneOn (derivWithin f S) S

Proof state:
case inl
S : Set ℝ
f : ℝ → ℝ
hfc : ConvexOn ℝ S f
hfd : DifferentiableOn ℝ f S
x : ℝ
hx hy : x ∈ S
hxy : x ≤ x
⊢ derivWithin f S x ≤ derivWithin f S x

Tactic:
rfl

Result:
no goals

Proof state:
S : Set ℝ
f : ℝ → ℝ
hfc : ConvexOn ℝ S f
hfd : DifferentiableOn ℝ f S
x : ℝ
hx : x ∈ S
y : ℝ
hy : y ∈ S
hxy : x ≤ y
⊢ derivWithin f S x ≤ derivWithin f S y

Tactic:
rcases eq_or_lt_of_le hxy with rfl | hxy'

Result:
case inl
S : Set ℝ
f : ℝ → ℝ
hfc : ConvexOn ℝ S f
hfd : DifferentiableOn ℝ f S
x : ℝ
hx hy : x ∈ S
hxy : x ≤ x
⊢ derivWithin f S x ≤ derivWithin f S x

case inr
S : Set ℝ
f : ℝ → ℝ
hfc : ConvexOn ℝ S f
hfd : DifferentiableOn ℝ f S
x : ℝ
hx : x ∈ S
y : ℝ
hy : y ∈ S
hxy : x ≤ y
hxy' : x < y
⊢ derivWithin f S x ≤ derivWithin f S y

Proof state:
S : Set ℝ
f : ℝ → ℝ
hfc : ConvexOn ℝ S f
hfd : DifferentiableOn ℝ f S
⊢ MonotoneOn (derivWithin f S) S

Tactic:
intro x hx y hy hxy

Result:
S : Set ℝ
f : ℝ → ℝ
hfc : ConvexOn ℝ S f
hfd : DifferentiableOn ℝ f S
x : ℝ
hx : x ∈ S
y : ℝ
hy : y ∈ S
hxy : x ≤ y
⊢ derivWithin f S x ≤ derivWithin f S y

Proof state:
case inr
S : Set ℝ
f : ℝ → ℝ
hfc : ConvexOn ℝ S f
hfd : DifferentiableOn ℝ f S
x : ℝ
hx : x ∈ S
y : ℝ
hy : y ∈ S
hxy : x ≤ y
hxy' : x < y
⊢ derivWithin f S x ≤ derivWithin f S y

Tactic:
exact (hfc.derivWithin_le_slope hx hy hxy' (hfd x hx)).trans
  (hfc.slope_le_derivWithin hx hy hxy' (hfd y hy))

Result:
no goals
-- Mathlib/NumberTheory/ModularForms/EisensteinSeries/UniformConvergence.lean
lemma div_max_sq_ge_one (x : Fin 2 → ℤ) (hx : x ≠ 0) :
    1 ≤ (x 0 / ‖x‖) ^ 2 ∨ 1 ≤ (x 1 / ‖x‖) ^ 2

Proof state:
x : Fin 2 → ℤ
hx : x ≠ 0
⊢ 1 ≤ (↑(x 0) / ‖x‖) ^ 2 ∨ 1 ≤ (↑(x 1) / ‖x‖) ^ 2

Tactic:
refine (max_choice (x 0).natAbs (x 1).natAbs).imp (fun H0 ↦ ?_) (fun H1 ↦ ?_)

Result:
case refine_1
x : Fin 2 → ℤ
hx : x ≠ 0
H0 : (x 0).natAbs ⊔ (x 1).natAbs = (x 0).natAbs
⊢ 1 ≤ (↑(x 0) / ‖x‖) ^ 2

case refine_2
x : Fin 2 → ℤ
hx : x ≠ 0
H1 : (x 0).natAbs ⊔ (x 1).natAbs = (x 1).natAbs
⊢ 1 ≤ (↑(x 1) / ‖x‖) ^ 2

Proof state:
case refine_1
x : Fin 2 → ℤ
hx : x ≠ 0
H0 : (x 0).natAbs ⊔ (x 1).natAbs = (x 0).natAbs
⊢ 1 ≤ (↑(x 0) / ‖x‖) ^ 2

Tactic:
have : x 0 ≠ 0 := by
  rwa [← norm_ne_zero_iff, norm_eq_max_natAbs, H0, Nat.cast_ne_zero, Int.natAbs_ne_zero] at hx

Result:
case refine_1
x : Fin 2 → ℤ
hx : x ≠ 0
H0 : (x 0).natAbs ⊔ (x 1).natAbs = (x 0).natAbs
this : x 0 ≠ 0
⊢ 1 ≤ (↑(x 0) / ‖x‖) ^ 2

Proof state:
case refine_2
x : Fin 2 → ℤ
hx : x ≠ 0
H1 : (x 0).natAbs ⊔ (x 1).natAbs = (x 1).natAbs
⊢ 1 ≤ (↑(x 1) / ‖x‖) ^ 2

Tactic:
have : x 1 ≠ 0 := by
  rwa [← norm_ne_zero_iff, norm_eq_max_natAbs, H1, Nat.cast_ne_zero, Int.natAbs_ne_zero] at hx

Result:
case refine_2
x : Fin 2 → ℤ
hx : x ≠ 0
H1 : (x 0).natAbs ⊔ (x 1).natAbs = (x 1).natAbs
this : x 1 ≠ 0
⊢ 1 ≤ (↑(x 1) / ‖x‖) ^ 2

Proof state:
case refine_1
x : Fin 2 → ℤ
hx : x ≠ 0
H0 : (x 0).natAbs ⊔ (x 1).natAbs = (x 0).natAbs
this : x 0 ≠ 0
⊢ 1 ≤ (↑(x 0) / ‖x‖) ^ 2

Tactic:
simp only [norm_eq_max_natAbs, H0, Int.cast_natAbs, Int.cast_abs, div_pow, sq_abs, ne_eq,
  OfNat.ofNat_ne_zero, not_false_eq_true, pow_eq_zero_iff, Int.cast_eq_zero, this, div_self,
  le_refl]

Result:
no goals

Proof state:
case refine_2
x : Fin 2 → ℤ
hx : x ≠ 0
H1 : (x 0).natAbs ⊔ (x 1).natAbs = (x 1).natAbs
this : x 1 ≠ 0
⊢ 1 ≤ (↑(x 1) / ‖x‖) ^ 2

Tactic:
simp only [norm_eq_max_natAbs, H1, Int.cast_natAbs, Int.cast_abs, div_pow, sq_abs, ne_eq,
  OfNat.ofNat_ne_zero, not_false_eq_true, pow_eq_zero_iff, Int.cast_eq_zero, this, div_self,
  le_refl]

Result:
no goals

Proof state:
x : Fin 2 → ℤ
hx : x ≠ 0
H1 : (x 0).natAbs ⊔ (x 1).natAbs = (x 1).natAbs
⊢ x 1 ≠ 0

Tactic:
rwa [← norm_ne_zero_iff, norm_eq_max_natAbs, H1, Nat.cast_ne_zero, Int.natAbs_ne_zero] at hx

Result:
no goals

Proof state:
x : Fin 2 → ℤ
hx : x ≠ 0
H0 : (x 0).natAbs ⊔ (x 1).natAbs = (x 0).natAbs
⊢ x 0 ≠ 0

Tactic:
rwa [← norm_ne_zero_iff, norm_eq_max_natAbs, H0, Nat.cast_ne_zero, Int.natAbs_ne_zero] at hx

Result:
no goals
-- Mathlib/Data/List/Rotate.lean
theorem rotate_eq_drop_append_take_mod {l : List α} {n : ℕ} :
    l.rotate n = l.drop (n % l.length) ++ l.take (n % l.length)

Proof state:
α : Type u
l : List α
n : ℕ
⊢ l.rotate n = drop (n % l.length) l ++ take (n % l.length) l

Tactic:
rcases l.length.zero_le.eq_or_lt with hl | hl

Result:
case inl
α : Type u
l : List α
n : ℕ
hl : 0 = l.length
⊢ l.rotate n = drop (n % l.length) l ++ take (n % l.length) l

case inr
α : Type u
l : List α
n : ℕ
hl : 0 < l.length
⊢ l.rotate n = drop (n % l.length) l ++ take (n % l.length) l

Proof state:
case inr
α : Type u
l : List α
n : ℕ
hl : 0 < l.length
⊢ l.rotate n = drop (n % l.length) l ++ take (n % l.length) l

Tactic:
rw [← rotate_eq_drop_append_take (n.mod_lt hl).le, rotate_mod]

Result:
no goals

Proof state:
case inl
α : Type u
l : List α
n : ℕ
hl : 0 = l.length
⊢ l.rotate n = drop (n % l.length) l ++ take (n % l.length) l

Tactic:
simp [eq_nil_of_length_eq_zero hl.symm]

Result:
no goals
-- Mathlib/.lake/packages/batteries/Batteries/Data/String/Lemmas.lean
theorem toString_extract : ∀ {s}, Valid s → Valid ⟨s.toString, b, e⟩ →
    (s.extract b e).toString = s.toString.extract b e
  | _, h₁, h₂ => by
    let ⟨l, m, r, h₁⟩ := h₁.validFor
    rw [h₁.toString] at h₂
    let ⟨ml, mm, mr, h₂⟩ := h₂.validFor
    have ⟨l', r', h₃⟩ := h₁.extract h₂
    rw [h₃.toString, h₁.toString, ← h₂.toString, toString]

Proof state:
b e : Pos
x✝ : Substring
h₁✝ : x✝.Valid
l m : List Char
h₂✝ : { str := { data := m }, startPos := b, stopPos := e }.Valid
r : List Char
h₁ : ValidFor l m r x✝
ml mm mr : List Char
h₂ : ValidFor ml mm mr { str := { data := m }, startPos := b, stopPos := e }
⊢ (x✝.extract b e).toString = x✝.toString.extract b e

Tactic:
have ⟨l', r', h₃⟩ := h₁.extract h₂

Result:
b e : Pos
x✝ : Substring
h₁✝ : x✝.Valid
l m : List Char
h₂✝ : { str := { data := m }, startPos := b, stopPos := e }.Valid
r : List Char
h₁ : ValidFor l m r x✝
ml mm mr : List Char
h₂ : ValidFor ml mm mr { str := { data := m }, startPos := b, stopPos := e }
l' r' : List Char
h₃ : ValidFor l' mm r' (x✝.extract b e)
⊢ (x✝.extract b e).toString = x✝.toString.extract b e

Proof state:
b e : Pos
x✝ : Substring
h₁✝ : x✝.Valid
h₂ : { str := x✝.toString, startPos := b, stopPos := e }.Valid
l m r : List Char
h₁ : ValidFor l m r x✝
⊢ (x✝.extract b e).toString = x✝.toString.extract b e

Tactic:
rw [h₁.toString] at h₂

Result:
b e : Pos
x✝ : Substring
h₁✝ : x✝.Valid
l m : List Char
h₂ : { str := { data := m }, startPos := b, stopPos := e }.Valid
r : List Char
h₁ : ValidFor l m r x✝
⊢ (x✝.extract b e).toString = x✝.toString.extract b e

Proof state:
b e : Pos
x✝ : Substring
h₁ : x✝.Valid
h₂ : { str := x✝.toString, startPos := b, stopPos := e }.Valid
⊢ (x✝.extract b e).toString = x✝.toString.extract b e

Tactic:
let ⟨l, m, r, h₁⟩ := h₁.validFor

Result:
b e : Pos
x✝ : Substring
h₁✝ : x✝.Valid
h₂ : { str := x✝.toString, startPos := b, stopPos := e }.Valid
l m r : List Char
h₁ : ValidFor l m r x✝
⊢ (x✝.extract b e).toString = x✝.toString.extract b e

Proof state:
b e : Pos
x✝ : Substring
h₁✝ : x✝.Valid
l m : List Char
h₂✝ : { str := { data := m }, startPos := b, stopPos := e }.Valid
r : List Char
h₁ : ValidFor l m r x✝
ml mm mr : List Char
h₂ : ValidFor ml mm mr { str := { data := m }, startPos := b, stopPos := e }
l' r' : List Char
h₃ : ValidFor l' mm r' (x✝.extract b e)
⊢ (x✝.extract b e).toString = x✝.toString.extract b e

Tactic:
rw [h₃.toString, h₁.toString, ← h₂.toString, toString]

Result:
no goals

Proof state:
b e : Pos
x✝ : Substring
h₁✝ : x✝.Valid
l m : List Char
h₂ : { str := { data := m }, startPos := b, stopPos := e }.Valid
r : List Char
h₁ : ValidFor l m r x✝
⊢ (x✝.extract b e).toString = x✝.toString.extract b e

Tactic:
let ⟨ml, mm, mr, h₂⟩ := h₂.validFor

Result:
b e : Pos
x✝ : Substring
h₁✝ : x✝.Valid
l m : List Char
h₂✝ : { str := { data := m }, startPos := b, stopPos := e }.Valid
r : List Char
h₁ : ValidFor l m r x✝
ml mm mr : List Char
h₂ : ValidFor ml mm mr { str := { data := m }, startPos := b, stopPos := e }
⊢ (x✝.extract b e).toString = x✝.toString.extract b e
-- Mathlib/Analysis/Complex/Isometry.lean
theorem linear_isometry_complex_aux {f : ℂ ≃ₗᵢ[ℝ] ℂ} (h : f 1 = 1) :
    f = LinearIsometryEquiv.refl ℝ ℂ ∨ f = conjLIE

Proof state:
case refine_2.a
f : ℂ ≃ₗᵢ[ℝ] ℂ
h : f 1 = 1
h0 : f I = I ∨ f I = -I
h' : f I = -I
⊢ ∀ (i : Fin 2), f.toLinearEquiv (basisOneI i) = conjLIE.toLinearEquiv (basisOneI i)

Tactic:
intro i

Result:
case refine_2.a
f : ℂ ≃ₗᵢ[ℝ] ℂ
h : f 1 = 1
h0 : f I = I ∨ f I = -I
h' : f I = -I
i : Fin 2
⊢ f.toLinearEquiv (basisOneI i) = conjLIE.toLinearEquiv (basisOneI i)

Proof state:
case refine_2.a
f : ℂ ≃ₗᵢ[ℝ] ℂ
h : f 1 = 1
h0 : f I = I ∨ f I = -I
h' : f I = -I
⊢ f.toLinearEquiv = conjLIE.toLinearEquiv

Tactic:
apply Complex.basisOneI.ext'

Result:
case refine_2.a
f : ℂ ≃ₗᵢ[ℝ] ℂ
h : f 1 = 1
h0 : f I = I ∨ f I = -I
h' : f I = -I
⊢ ∀ (i : Fin 2), f.toLinearEquiv (basisOneI i) = conjLIE.toLinearEquiv (basisOneI i)

Proof state:
case refine_2.a
f : ℂ ≃ₗᵢ[ℝ] ℂ
h : f 1 = 1
h0 : f I = I ∨ f I = -I
h' : f I = -I
i : Fin 2
⊢ f.toLinearEquiv (basisOneI i) = conjLIE.toLinearEquiv (basisOneI i)

Tactic:
fin_cases i <;> simp [h, h']

Result:
no goals

Proof state:
case refine_2
f : ℂ ≃ₗᵢ[ℝ] ℂ
h : f 1 = 1
h0 : f I = I ∨ f I = -I
h' : f I = -I
⊢ f = conjLIE

Tactic:
apply LinearIsometryEquiv.toLinearEquiv_injective

Result:
case refine_2.a
f : ℂ ≃ₗᵢ[ℝ] ℂ
h : f 1 = 1
h0 : f I = I ∨ f I = -I
h' : f I = -I
⊢ f.toLinearEquiv = conjLIE.toLinearEquiv

Proof state:
f : ℂ ≃ₗᵢ[ℝ] ℂ
h : f 1 = 1
⊢ (f I).re = 0 ∧ ((f I).im = I.im ∨ (f I).im = -I.im)

Tactic:
constructor

Result:
case left
f : ℂ ≃ₗᵢ[ℝ] ℂ
h : f 1 = 1
⊢ (f I).re = 0

case right
f : ℂ ≃ₗᵢ[ℝ] ℂ
h : f 1 = 1
⊢ (f I).im = I.im ∨ (f I).im = -I.im

Proof state:
case right
f : ℂ ≃ₗᵢ[ℝ] ℂ
h : f 1 = 1
⊢ (f I).im = I.im ∨ (f I).im = -I.im

Tactic:
apply @LinearIsometry.im_apply_eq_im_or_neg_of_re_apply_eq_re f.toLinearIsometry

Result:
case right.h₂
f : ℂ ≃ₗᵢ[ℝ] ℂ
h : f 1 = 1
⊢ ∀ (z : ℂ), (f.toLinearIsometry z).re = z.re

Proof state:
case right.h₂
f : ℂ ≃ₗᵢ[ℝ] ℂ
h : f 1 = 1
⊢ ∀ (z : ℂ), (f.toLinearIsometry z).re = z.re

Tactic:
intro z

Result:
case right.h₂
f : ℂ ≃ₗᵢ[ℝ] ℂ
h : f 1 = 1
z : ℂ
⊢ (f.toLinearIsometry z).re = z.re

Proof state:
case left
f : ℂ ≃ₗᵢ[ℝ] ℂ
h : f 1 = 1
⊢ (f I).re = I.re

Tactic:
exact @LinearIsometry.re_apply_eq_re f.toLinearIsometry h I

Result:
no goals

Proof state:
case right.h₂
f : ℂ ≃ₗᵢ[ℝ] ℂ
h : f 1 = 1
z : ℂ
⊢ (f.toLinearIsometry z).re = z.re

Tactic:
rw [@LinearIsometry.re_apply_eq_re f.toLinearIsometry h]

Result:
no goals

Proof state:
case left
f : ℂ ≃ₗᵢ[ℝ] ℂ
h : f 1 = 1
⊢ (f I).re = 0

Tactic:
rw [← I_re]

Result:
case left
f : ℂ ≃ₗᵢ[ℝ] ℂ
h : f 1 = 1
⊢ (f I).re = I.re

Proof state:
f : ℂ ≃ₗᵢ[ℝ] ℂ
h : f 1 = 1
⊢ f I = I ∨ f I = -I

Tactic:
simp only [Complex.ext_iff, ← and_or_left, neg_re, I_re, neg_im, neg_zero]

Result:
f : ℂ ≃ₗᵢ[ℝ] ℂ
h : f 1 = 1
⊢ (f I).re = 0 ∧ ((f I).im = I.im ∨ (f I).im = -I.im)
-- Mathlib/Probability/ProbabilityMassFunction/Monad.lean
theorem support_bindOnSupport :
    (p.bindOnSupport f).support = ⋃ (a : α) (h : a ∈ p.support), (f a h).support

Proof state:
α : Type u_1
β : Type u_2
p : PMF α
f : (a : α) → a ∈ p.support → PMF β
b : β
⊢ b ∈ (p.bindOnSupport f).support ↔ b ∈ ⋃ a, ⋃ (h : a ∈ p.support), (f a h).support

Tactic:
simp only [ENNReal.tsum_eq_zero, not_or, mem_support_iff, bindOnSupport_apply, Ne, not_forall,
  mul_eq_zero, Set.mem_iUnion]

Result:
α : Type u_1
β : Type u_2
p : PMF α
f : (a : α) → a ∈ p.support → PMF β
b : β
⊢ (∃ x, ¬p x = 0 ∧ ¬(if h : p x = 0 then 0 else (f x h) b) = 0) ↔ ∃ i, ∃ (h : ¬p i = 0), ¬(f i ⋯) b = 0

Proof state:
α : Type u_1
β : Type u_2
p : PMF α
f : (a : α) → a ∈ p.support → PMF β
b : β
hb : ∃ i, ∃ (h : ¬p i = 0), ¬(f i ⋯) b = 0
a : α
ha : ¬p a = 0
ha' : ¬(f a ⋯) b = 0
⊢ ¬(if h : p a = 0 then 0 else (f a h) b) = 0

Tactic:
simpa [(mem_support_iff _ a).1 ha] using ha'

Result:
no goals

Proof state:
α : Type u_1
β : Type u_2
p : PMF α
f : (a : α) → a ∈ p.support → PMF β
b : β
⊢ (∃ x, ¬p x = 0 ∧ ¬(if h : p x = 0 then 0 else (f x h) b) = 0) ↔ ∃ i, ∃ (h : ¬p i = 0), ¬(f i ⋯) b = 0

Tactic:
exact
  ⟨fun hb =>
    let ⟨a, ⟨ha, ha'⟩⟩ := hb
    ⟨a, ha, by simpa [ha] using ha'⟩,
    fun hb =>
    let ⟨a, ha, ha'⟩ := hb
    ⟨a, ⟨ha, by simpa [(mem_support_iff _ a).1 ha] using ha'⟩⟩⟩

Result:
no goals

Proof state:
α : Type u_1
β : Type u_2
p : PMF α
f : (a : α) → a ∈ p.support → PMF β
b : β
hb : ∃ x, ¬p x = 0 ∧ ¬(if h : p x = 0 then 0 else (f x h) b) = 0
a : α
ha : ¬p a = 0
ha' : ¬(if h : p a = 0 then 0 else (f a h) b) = 0
⊢ ¬(f a ⋯) b = 0

Tactic:
simpa [ha] using ha'

Result:
no goals

Proof state:
α : Type u_1
β : Type u_2
p : PMF α
f : (a : α) → a ∈ p.support → PMF β
⊢ (p.bindOnSupport f).support = ⋃ a, ⋃ (h : a ∈ p.support), (f a h).support

Tactic:
refine Set.ext fun b => ?_

Result:
α : Type u_1
β : Type u_2
p : PMF α
f : (a : α) → a ∈ p.support → PMF β
b : β
⊢ b ∈ (p.bindOnSupport f).support ↔ b ∈ ⋃ a, ⋃ (h : a ∈ p.support), (f a h).support
-- Mathlib/NumberTheory/Cyclotomic/Basic.lean
theorem iff_singleton :
    IsCyclotomicExtension {n} A B ↔
      (∃ r : B, IsPrimitiveRoot r n) ∧ ∀ x, x ∈ adjoin A {b : B | b ^ (n : ℕ) = 1}

Proof state:
n : ℕ+
A : Type u
B : Type v
inst✝² : CommRing A
inst✝¹ : CommRing B
inst✝ : Algebra A B
⊢ IsCyclotomicExtension {n} A B ↔ (∃ r, IsPrimitiveRoot r ↑n) ∧ ∀ (x : B), x ∈ adjoin A {b | b ^ ↑n = 1}

Tactic:
simp [isCyclotomicExtension_iff]

Result:
no goals
-- Mathlib/LinearAlgebra/Matrix/SpecialLinearGroup.lean
theorem coe_T_zpow (n : ℤ) : (T ^ n).1 = !![1, n; 0, 1]

Proof state:
case hn
n : ℕ
h : ↑(T ^ (-↑n)) = !![1, -↑n; 0, 1]
⊢ !![1 * 1 + -↑n * 0, 1 * -1 + -↑n * 1; 0 * 1 + 1 * 0, 0 * -1 + 1 * 1] = !![1, -↑n - 1; 0, 1]

Tactic:
congrm !![?_, ?_; _, _] <;> ring

Result:
no goals

Proof state:
n : ℤ
⊢ ↑(T ^ n) = !![1, n; 0, 1]

Tactic:
induction n with
| hz => rw [zpow_zero, coe_one, Matrix.one_fin_two]
| hp n h =>
  simp_rw [zpow_add, zpow_one, coe_mul, h, coe_T, Matrix.mul_fin_two]
  congrm !![_, ?_; _, _]
  rw [mul_one, mul_one, add_comm]
| hn n h =>
  simp_rw [zpow_sub, zpow_one, coe_mul, h, coe_T_inv, Matrix.mul_fin_two]
  congrm !![?_, ?_; _, _] <;> ring

Result:
no goals

Proof state:
case hp
n : ℕ
h : ↑(T ^ ↑n) = !![1, ↑n; 0, 1]
⊢ ↑(T ^ (↑n + 1)) = !![1, ↑n + 1; 0, 1]

Tactic:
simp_rw [zpow_add, zpow_one, coe_mul, h, coe_T, Matrix.mul_fin_two]

Result:
case hp
n : ℕ
h : ↑(T ^ ↑n) = !![1, ↑n; 0, 1]
⊢ !![1 * 1 + ↑n * 0, 1 * 1 + ↑n * 1; 0 * 1 + 1 * 0, 0 * 1 + 1 * 1] = !![1, ↑n + 1; 0, 1]

Proof state:
case hp
n : ℕ
h : ↑(T ^ ↑n) = !![1, ↑n; 0, 1]
⊢ !![1 * 1 + ↑n * 0, 1 * 1 + ↑n * 1; 0 * 1 + 1 * 0, 0 * 1 + 1 * 1] = !![1, ↑n + 1; 0, 1]

Tactic:
congrm !![_, ?_; _, _]

Result:
case hp
n : ℕ
h : ↑(T ^ ↑n) = !![1, ↑n; 0, 1]
⊢ 1 * 1 + ↑n * 1 = ↑n + 1

Proof state:
case hn
n : ℕ
h : ↑(T ^ (-↑n)) = !![1, -↑n; 0, 1]
⊢ ↑(T ^ (-↑n - 1)) = !![1, -↑n - 1; 0, 1]

Tactic:
simp_rw [zpow_sub, zpow_one, coe_mul, h, coe_T_inv, Matrix.mul_fin_two]

Result:
case hn
n : ℕ
h : ↑(T ^ (-↑n)) = !![1, -↑n; 0, 1]
⊢ !![1 * 1 + -↑n * 0, 1 * -1 + -↑n * 1; 0 * 1 + 1 * 0, 0 * -1 + 1 * 1] = !![1, -↑n - 1; 0, 1]

Proof state:
case hz

⊢ ↑(T ^ 0) = !![1, 0; 0, 1]

Tactic:
rw [zpow_zero, coe_one, Matrix.one_fin_two]

Result:
no goals

Proof state:
case hp
n : ℕ
h : ↑(T ^ ↑n) = !![1, ↑n; 0, 1]
⊢ 1 * 1 + ↑n * 1 = ↑n + 1

Tactic:
rw [mul_one, mul_one, add_comm]

Result:
no goals
-- Mathlib/CategoryTheory/Limits/Shapes/Pullback/CommSq.lean
theorem zero_left (X : C) : IsPullback (0 : 0 ⟶ X) (0 : (0 : C) ⟶ 0) (𝟙 X) (0 : 0 ⟶ X) :=
  { w

Proof state:
C : Type u₁
inst✝² : Category.{v₁, u₁} C
inst✝¹ : HasZeroObject C
inst✝ : HasZeroMorphisms C
X : C
⊢ 0 ≫ 𝟙 X = 0 ≫ 0

Tactic:
simp

Result:
no goals

Proof state:
C : Type u₁
inst✝² : Category.{v₁, u₁} C
inst✝¹ : HasZeroObject C
inst✝ : HasZeroMorphisms C
X : C
s : Cone (cospan (𝟙 X) 0)
⊢ 0 ≫ PullbackCone.fst s = 𝟙 s.pt ≫ PullbackCone.fst s

Tactic:
simpa using (PullbackCone.condition s).symm

Result:
no goals

Proof state:
C : Type u₁
inst✝² : Category.{v₁, u₁} C
inst✝¹ : HasZeroObject C
inst✝ : HasZeroMorphisms C
X : C
s : Cone (cospan (𝟙 X) 0)
⊢ ∀ (j : WalkingCospan), (fun x => 0) s ≫ (PullbackCone.mk 0 0 ⋯).π.app j = s.π.app j

Tactic:
simpa [eq_iff_true_of_subsingleton] using
  @PullbackCone.equalizer_ext _ _ _ _ _ _ _ s _ 0 (𝟙 _)
    (by simpa using (PullbackCone.condition s).symm)

Result:
no goals