harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/Logic/Function/Basic.lean
theorem partialInv_of_injective {α β} {f : α → β} (I : Injective f) : IsPartialInv f (partialInv f)
  | a, b =>
  ⟨fun h =>
    have hpi : partialInv f b = if h : ∃ a, f a = b then some (Classical.choose h) else none :=
      rfl
    if h' : ∃ a, f a = b
    then by rw [hpi, dif_pos h'] at h
            injection h with h
            subst h
            apply Classical.choose_spec h'
    else by rw [hpi, dif_neg h'] at h; contradiction,
  fun e => e ▸ have h : ∃ a', f a' = f a := ⟨_, rfl⟩
              (dif_pos h).trans (congr_arg _ (I <| Classical.choose_spec h))⟩

Proof state:
α : Type u_4
β : Sort u_5
f : α → β
I : Injective f
a : α
b : β
h : none = some a
hpi : partialInv f b = if h : ∃ a, f a = b then some (Classical.choose h) else none
h' : ¬∃ a, f a = b
⊢ f a = b

Tactic:
contradiction

Result:
no goals

Proof state:
α : Type u_4
β : Sort u_5
f : α → β
I : Injective f
a : α
b : β
h : partialInv f b = some a
hpi : partialInv f b = if h : ∃ a, f a = b then some (Classical.choose h) else none
h' : ∃ a, f a = b
⊢ f a = b

Tactic:
rw [hpi, dif_pos h'] at h

Result:
α : Type u_4
β : Sort u_5
f : α → β
I : Injective f
a : α
b : β
hpi : partialInv f b = if h : ∃ a, f a = b then some (Classical.choose h) else none
h' : ∃ a, f a = b
h : some (Classical.choose h') = some a
⊢ f a = b

Proof state:
α : Type u_4
β : Sort u_5
f : α → β
I : Injective f
b : β
hpi : partialInv f b = if h : ∃ a, f a = b then some (Classical.choose h) else none
h' : ∃ a, f a = b
⊢ f (Classical.choose h') = b

Tactic:
apply Classical.choose_spec h'

Result:
no goals

Proof state:
α : Type u_4
β : Sort u_5
f : α → β
I : Injective f
a : α
b : β
hpi : partialInv f b = if h : ∃ a, f a = b then some (Classical.choose h) else none
h' : ∃ a, f a = b
h : some (Classical.choose h') = some a
⊢ f a = b

Tactic:
injection h with h

Result:
α : Type u_4
β : Sort u_5
f : α → β
I : Injective f
a : α
b : β
hpi : partialInv f b = if h : ∃ a, f a = b then some (Classical.choose h) else none
h' : ∃ a, f a = b
h : Classical.choose h' = a
⊢ f a = b

Proof state:
α : Type u_4
β : Sort u_5
f : α → β
I : Injective f
a : α
b : β
hpi : partialInv f b = if h : ∃ a, f a = b then some (Classical.choose h) else none
h' : ∃ a, f a = b
h : Classical.choose h' = a
⊢ f a = b

Tactic:
subst h

Result:
α : Type u_4
β : Sort u_5
f : α → β
I : Injective f
b : β
hpi : partialInv f b = if h : ∃ a, f a = b then some (Classical.choose h) else none
h' : ∃ a, f a = b
⊢ f (Classical.choose h') = b

Proof state:
α : Type u_4
β : Sort u_5
f : α → β
I : Injective f
a : α
b : β
h : partialInv f b = some a
hpi : partialInv f b = if h : ∃ a, f a = b then some (Classical.choose h) else none
h' : ¬∃ a, f a = b
⊢ f a = b

Tactic:
rw [hpi, dif_neg h'] at h

Result:
α : Type u_4
β : Sort u_5
f : α → β
I : Injective f
a : α
b : β
h : none = some a
hpi : partialInv f b = if h : ∃ a, f a = b then some (Classical.choose h) else none
h' : ¬∃ a, f a = b
⊢ f a = b
-- Mathlib/Analysis/InnerProductSpace/PiL2.lean
theorem LinearIsometry.extend_apply (L : S →ₗᵢ[𝕜] V) (s : S) : L.extend s = L s

Proof state:
𝕜 : Type u_3
inst✝³ : RCLike 𝕜
V : Type u_7
inst✝² : NormedAddCommGroup V
inst✝¹ : InnerProductSpace 𝕜 V
inst✝ : FiniteDimensional 𝕜 V
S : Submodule 𝕜 V
L : ↥S →ₗᵢ[𝕜] V
s : ↥S
⊢ L.extend ↑s = L s

Tactic:
haveI : CompleteSpace S := FiniteDimensional.complete 𝕜 S

Result:
𝕜 : Type u_3
inst✝³ : RCLike 𝕜
V : Type u_7
inst✝² : NormedAddCommGroup V
inst✝¹ : InnerProductSpace 𝕜 V
inst✝ : FiniteDimensional 𝕜 V
S : Submodule 𝕜 V
L : ↥S →ₗᵢ[𝕜] V
s : ↥S
this : CompleteSpace ↥S
⊢ L.extend ↑s = L s

Proof state:
𝕜 : Type u_3
inst✝³ : RCLike 𝕜
V : Type u_7
inst✝² : NormedAddCommGroup V
inst✝¹ : InnerProductSpace 𝕜 V
inst✝ : FiniteDimensional 𝕜 V
S : Submodule 𝕜 V
L : ↥S →ₗᵢ[𝕜] V
s : ↥S
this : CompleteSpace ↥S
⊢ L.extend ↑s = L s

Tactic:
simp only [LinearIsometry.extend, ← LinearIsometry.coe_toLinearMap]

Result:
𝕜 : Type u_3
inst✝³ : RCLike 𝕜
V : Type u_7
inst✝² : NormedAddCommGroup V
inst✝¹ : InnerProductSpace 𝕜 V
inst✝ : FiniteDimensional 𝕜 V
S : Submodule 𝕜 V
L : ↥S →ₗᵢ[𝕜] V
s : ↥S
this : CompleteSpace ↥S
⊢ (L.toLinearMap ∘ₗ ↑(orthogonalProjection S) +
        ((LinearMap.range L.toLinearMap)ᗮ.subtypeₗᵢ.comp
              ((stdOrthonormalBasis 𝕜 ↥Sᗮ).repr.trans
                  ((stdOrthonormalBasis 𝕜 ↥(LinearMap.range L.toLinearMap)ᗮ).reindex
                        (finCongr ⋯)).repr.symm).toLinearIsometry).toLinearMap ∘ₗ
          ↑(orthogonalProjection Sᗮ))
      ↑s =
    L.toLinearMap s

Proof state:
𝕜 : Type u_3
inst✝³ : RCLike 𝕜
V : Type u_7
inst✝² : NormedAddCommGroup V
inst✝¹ : InnerProductSpace 𝕜 V
inst✝ : FiniteDimensional 𝕜 V
S : Submodule 𝕜 V
L : ↥S →ₗᵢ[𝕜] V
s : ↥S
this : CompleteSpace ↥S
⊢ (L.toLinearMap ∘ₗ ↑(orthogonalProjection S) +
        ((LinearMap.range L.toLinearMap)ᗮ.subtypeₗᵢ.comp
              ((stdOrthonormalBasis 𝕜 ↥Sᗮ).repr.trans
                  ((stdOrthonormalBasis 𝕜 ↥(LinearMap.range L.toLinearMap)ᗮ).reindex
                        (finCongr ⋯)).repr.symm).toLinearIsometry).toLinearMap ∘ₗ
          ↑(orthogonalProjection Sᗮ))
      ↑s =
    L.toLinearMap s

Tactic:
simp only [add_right_eq_self, LinearIsometry.coe_toLinearMap,
  LinearIsometryEquiv.coe_toLinearIsometry, LinearIsometry.coe_comp, Function.comp_apply,
  orthogonalProjection_mem_subspace_eq_self, LinearMap.coe_comp, ContinuousLinearMap.coe_coe,
  Submodule.coe_subtype, LinearMap.add_apply, Submodule.coe_eq_zero,
  LinearIsometryEquiv.map_eq_zero_iff, Submodule.coe_subtypeₗᵢ,
  orthogonalProjection_mem_subspace_orthogonalComplement_eq_zero, Submodule.orthogonal_orthogonal,
  Submodule.coe_mem]

Result:
no goals
-- Mathlib/Algebra/Star/StarAlgHom.lean
theorem fst_prod (f : A →⋆ₙₐ[R] B) (g : A →⋆ₙₐ[R] C) : (fst R B C).comp (prod f g) = f

Proof state:
R : Type u_1
A : Type u_2
B : Type u_3
C : Type u_4
inst✝⁹ : Monoid R
inst✝⁸ : NonUnitalNonAssocSemiring A
inst✝⁷ : DistribMulAction R A
inst✝⁶ : Star A
inst✝⁵ : NonUnitalNonAssocSemiring B
inst✝⁴ : DistribMulAction R B
inst✝³ : Star B
inst✝² : NonUnitalNonAssocSemiring C
inst✝¹ : DistribMulAction R C
inst✝ : Star C
f : A →⋆ₙₐ[R] B
g : A →⋆ₙₐ[R] C
⊢ (fst R B C).comp (f.prod g) = f

Tactic:
ext

Result:
case h
R : Type u_1
A : Type u_2
B : Type u_3
C : Type u_4
inst✝⁹ : Monoid R
inst✝⁸ : NonUnitalNonAssocSemiring A
inst✝⁷ : DistribMulAction R A
inst✝⁶ : Star A
inst✝⁵ : NonUnitalNonAssocSemiring B
inst✝⁴ : DistribMulAction R B
inst✝³ : Star B
inst✝² : NonUnitalNonAssocSemiring C
inst✝¹ : DistribMulAction R C
inst✝ : Star C
f : A →⋆ₙₐ[R] B
g : A →⋆ₙₐ[R] C
x✝ : A
⊢ ((fst R B C).comp (f.prod g)) x✝ = f x✝

Proof state:
case h
R : Type u_1
A : Type u_2
B : Type u_3
C : Type u_4
inst✝⁹ : Monoid R
inst✝⁸ : NonUnitalNonAssocSemiring A
inst✝⁷ : DistribMulAction R A
inst✝⁶ : Star A
inst✝⁵ : NonUnitalNonAssocSemiring B
inst✝⁴ : DistribMulAction R B
inst✝³ : Star B
inst✝² : NonUnitalNonAssocSemiring C
inst✝¹ : DistribMulAction R C
inst✝ : Star C
f : A →⋆ₙₐ[R] B
g : A →⋆ₙₐ[R] C
x✝ : A
⊢ ((fst R B C).comp (f.prod g)) x✝ = f x✝

Tactic:
rfl

Result:
no goals
-- Mathlib/Combinatorics/Quiver/Cast.lean
theorem eq_nil_of_length_zero {u v : U} (p : Path u v) (hzero : p.length = 0) :
    p.cast (eq_of_length_zero p hzero) rfl = Path.nil

Proof state:
case cons
U : Type u_1
inst✝ : Quiver U
u v b✝ : U
a✝¹ : Path u b✝
a✝ : b✝ ⟶ v
hzero : (a✝¹.cons a✝).length = 0
⊢ Path.cast ⋯ ⋯ (a✝¹.cons a✝) = nil

Tactic:
simp only [Nat.succ_ne_zero, length_cons] at hzero

Result:
no goals

Proof state:
U : Type u_1
inst✝ : Quiver U
u v : U
p : Path u v
hzero : p.length = 0
⊢ Path.cast ⋯ ⋯ p = nil

Tactic:
cases p

Result:
case nil
U : Type u_1
inst✝ : Quiver U
u : U
hzero : nil.length = 0
⊢ Path.cast ⋯ ⋯ nil = nil

case cons
U : Type u_1
inst✝ : Quiver U
u v b✝ : U
a✝¹ : Path u b✝
a✝ : b✝ ⟶ v
hzero : (a✝¹.cons a✝).length = 0
⊢ Path.cast ⋯ ⋯ (a✝¹.cons a✝) = nil

Proof state:
case nil
U : Type u_1
inst✝ : Quiver U
u : U
hzero : nil.length = 0
⊢ Path.cast ⋯ ⋯ nil = nil

Tactic:
rfl

Result:
no goals
-- Mathlib/LinearAlgebra/LinearIndependent/Defs.lean
theorem linearIndepOn_iff : LinearIndepOn R v s ↔
      ∀ l ∈ Finsupp.supported R R s, (Finsupp.linearCombination R v) l = 0 → l = 0 :=
  linearIndepOn_iffₛ.trans ⟨fun h l hl ↦ h l hl 0 (zero_mem _), fun h f hf g hg eq ↦
    sub_eq_zero.mp (h (f - g) (sub_mem hf hg) <| by rw [map_sub, eq, sub_self])⟩

Proof state:
ι : Type u'
R : Type u_2
s : Set ι
M : Type u_4
v : ι → M
inst✝² : Ring R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
h : ∀ l ∈ Finsupp.supported R R s, (Finsupp.linearCombination R v) l = 0 → l = 0
f : ι →₀ R
hf : f ∈ Finsupp.supported R R s
g : ι →₀ R
hg : g ∈ Finsupp.supported R R s
eq : (Finsupp.linearCombination R v) f = (Finsupp.linearCombination R v) g
⊢ (Finsupp.linearCombination R v) (f - g) = 0

Tactic:
rw [map_sub, eq, sub_self]

Result:
no goals
-- Mathlib/SetTheory/Ordinal/FixedPointApproximants.lean
theorem not_injective_limitation_set : ¬ InjOn g (Iio (ord <| succ #α))

Proof state:
α : Type u
g : Ordinal.{u} → α
h_inj : InjOn g (Iio (succ #α).ord)
h : lift.{u, u + 1} #↑(Iio (succ #α).ord) ≤ lift.{u + 1, u} #α
⊢ False

Tactic:
have mk_initialSeg_subtype :
    #(Iio (ord <| succ #α)) = lift.{u + 1} (succ #α) := by
  simpa only [coe_setOf, card_typein, card_ord] using mk_Iio_ordinal (ord <| succ #α)

Result:
α : Type u
g : Ordinal.{u} → α
h_inj : InjOn g (Iio (succ #α).ord)
h : lift.{u, u + 1} #↑(Iio (succ #α).ord) ≤ lift.{u + 1, u} #α
mk_initialSeg_subtype : #↑(Iio (succ #α).ord) = lift.{u + 1, u} (succ #α)
⊢ False

Proof state:
α : Type u
g : Ordinal.{u} → α
⊢ ¬InjOn g (Iio (succ #α).ord)

Tactic:
intro h_inj

Result:
α : Type u
g : Ordinal.{u} → α
h_inj : InjOn g (Iio (succ #α).ord)
⊢ False

Proof state:
α : Type u
g : Ordinal.{u} → α
h_inj : InjOn g (Iio (succ #α).ord)
h : lift.{u, u + 1} #↑(Iio (succ #α).ord) ≤ lift.{u + 1, u} #α
⊢ #↑(Iio (succ #α).ord) = lift.{u + 1, u} (succ #α)

Tactic:
simpa only [coe_setOf, card_typein, card_ord] using mk_Iio_ordinal (ord <| succ #α)

Result:
no goals

Proof state:
α : Type u
g : Ordinal.{u} → α
h_inj : InjOn g (Iio (succ #α).ord)
h : succ #α ≤ #α
mk_initialSeg_subtype : #↑(Iio (succ #α).ord) = lift.{u + 1, u} (succ #α)
⊢ False

Tactic:
exact not_le_of_lt (Order.lt_succ #α) h

Result:
no goals

Proof state:
α : Type u
g : Ordinal.{u} → α
h_inj : InjOn g (Iio (succ #α).ord)
h : lift.{u, u + 1} #↑(Iio (succ #α).ord) ≤ lift.{u + 1, u} #α
mk_initialSeg_subtype : #↑(Iio (succ #α).ord) = lift.{u + 1, u} (succ #α)
⊢ False

Tactic:
rw [mk_initialSeg_subtype, lift_lift, lift_le] at h

Result:
α : Type u
g : Ordinal.{u} → α
h_inj : InjOn g (Iio (succ #α).ord)
h : succ #α ≤ #α
mk_initialSeg_subtype : #↑(Iio (succ #α).ord) = lift.{u + 1, u} (succ #α)
⊢ False

Proof state:
α : Type u
g : Ordinal.{u} → α
h_inj : InjOn g (Iio (succ #α).ord)
⊢ False

Tactic:
have h := lift_mk_le_lift_mk_of_injective <| injOn_iff_injective.1 h_inj

Result:
α : Type u
g : Ordinal.{u} → α
h_inj : InjOn g (Iio (succ #α).ord)
h : lift.{u, u + 1} #↑(Iio (succ #α).ord) ≤ lift.{u + 1, u} #α
⊢ False
-- Mathlib/Data/List/EditDistance/Bounds.lean
theorem le_suffixLevenshtein_append_minimum (xs : List α) (ys₁ ys₂) :
    (suffixLevenshtein C xs ys₂).1.minimum ≤ (suffixLevenshtein C xs (ys₁ ++ ys₂)).1.minimum

Proof state:
α : Type u_1
β : Type u_2
δ : Type u_3
C : Levenshtein.Cost α β δ
inst✝¹ : LinearOrderedAddCommMonoid δ
inst✝ : CanonicallyOrderedAdd δ
xs : List α
ys₁ ys₂ : List β
⊢ (↑(suffixLevenshtein C xs ys₂)).minimum ≤ (↑(suffixLevenshtein C xs (ys₁ ++ ys₂))).minimum

Tactic:
induction ys₁ with
| nil => exact le_refl _
| cons y ys₁ ih => exact ih.trans (le_suffixLevenshtein_cons_minimum _ _ _)

Result:
no goals

Proof state:
case cons
α : Type u_1
β : Type u_2
δ : Type u_3
C : Levenshtein.Cost α β δ
inst✝¹ : LinearOrderedAddCommMonoid δ
inst✝ : CanonicallyOrderedAdd δ
xs : List α
ys₂ : List β
y : β
ys₁ : List β
ih : (↑(suffixLevenshtein C xs ys₂)).minimum ≤ (↑(suffixLevenshtein C xs (ys₁ ++ ys₂))).minimum
⊢ (↑(suffixLevenshtein C xs ys₂)).minimum ≤ (↑(suffixLevenshtein C xs (y :: ys₁ ++ ys₂))).minimum

Tactic:
exact ih.trans (le_suffixLevenshtein_cons_minimum _ _ _)

Result:
no goals

Proof state:
case nil
α : Type u_1
β : Type u_2
δ : Type u_3
C : Levenshtein.Cost α β δ
inst✝¹ : LinearOrderedAddCommMonoid δ
inst✝ : CanonicallyOrderedAdd δ
xs : List α
ys₂ : List β
⊢ (↑(suffixLevenshtein C xs ys₂)).minimum ≤ (↑(suffixLevenshtein C xs ([] ++ ys₂))).minimum

Tactic:
exact le_refl _

Result:
no goals
-- Mathlib/NumberTheory/Padics/Hensel.lean
theorem T_lt_one : T < 1

Proof state:
p : ℕ
inst✝ : Fact (Nat.Prime p)
F : Polynomial ℤ_[p]
a : ℤ_[p]
hnorm : ‖Polynomial.eval a F‖ < ‖Polynomial.eval a (Polynomial.derivative F)‖ ^ 2
⊢ T_gen p F a < 1

Tactic:
have h := (div_lt_one (deriv_sq_norm_pos hnorm)).2 hnorm

Result:
p : ℕ
inst✝ : Fact (Nat.Prime p)
F : Polynomial ℤ_[p]
a : ℤ_[p]
hnorm : ‖Polynomial.eval a F‖ < ‖Polynomial.eval a (Polynomial.derivative F)‖ ^ 2
h : ‖Polynomial.eval a F‖ / ‖Polynomial.eval a (Polynomial.derivative F)‖ ^ 2 < 1
⊢ T_gen p F a < 1

Proof state:
p : ℕ
inst✝ : Fact (Nat.Prime p)
F : Polynomial ℤ_[p]
a : ℤ_[p]
hnorm : ‖Polynomial.eval a F‖ < ‖Polynomial.eval a (Polynomial.derivative F)‖ ^ 2
h : ‖Polynomial.eval a F‖ / ‖Polynomial.eval a (Polynomial.derivative F)‖ ^ 2 < 1
⊢ ‖Polynomial.eval a F‖ / ‖Polynomial.eval a (Polynomial.derivative F)‖ ^ 2 < 1

Tactic:
exact h

Result:
no goals

Proof state:
p : ℕ
inst✝ : Fact (Nat.Prime p)
F : Polynomial ℤ_[p]
a : ℤ_[p]
hnorm : ‖Polynomial.eval a F‖ < ‖Polynomial.eval a (Polynomial.derivative F)‖ ^ 2
h : ‖Polynomial.eval a F‖ / ‖Polynomial.eval a (Polynomial.derivative F)‖ ^ 2 < 1
⊢ T_gen p F a < 1

Tactic:
rw [T_def]

Result:
p : ℕ
inst✝ : Fact (Nat.Prime p)
F : Polynomial ℤ_[p]
a : ℤ_[p]
hnorm : ‖Polynomial.eval a F‖ < ‖Polynomial.eval a (Polynomial.derivative F)‖ ^ 2
h : ‖Polynomial.eval a F‖ / ‖Polynomial.eval a (Polynomial.derivative F)‖ ^ 2 < 1
⊢ ‖Polynomial.eval a F‖ / ‖Polynomial.eval a (Polynomial.derivative F)‖ ^ 2 < 1
-- Mathlib/Order/Filter/Cofinite.lean
theorem Nat.frequently_atTop_iff_infinite {p : ℕ → Prop} :
    (∃ᶠ n in atTop, p n) ↔ Set.Infinite { n | p n }

Proof state:
p : ℕ → Prop
⊢ (∃ᶠ (n : ℕ) in atTop, p n) ↔ {n | p n}.Infinite

Tactic:
rw [← Nat.cofinite_eq_atTop, frequently_cofinite_iff_infinite]

Result:
no goals
-- Mathlib/Algebra/Order/ToIntervalMod.lean
theorem toIocDiv_add_left' (a b : α) : toIocDiv hp (p + a) b = toIocDiv hp a b - 1

Proof state:
α : Type u_1
inst✝ : LinearOrderedAddCommGroup α
hα : Archimedean α
p : α
hp : 0 < p
a b : α
⊢ toIocDiv hp (p + a) b = toIocDiv hp a b - 1

Tactic:
rw [add_comm, toIocDiv_add_right']

Result:
no goals
-- Mathlib/SetTheory/Cardinal/ENat.lean
@[simp] lemma ofENat_lt_nat {m : ℕ∞} {n : ℕ} : ofENat m < n ↔ m < n

Proof state:
m : ℕ∞
n : ℕ
⊢ ↑m < ↑n ↔ m < ↑n

Tactic:
norm_cast

Result:
no goals
-- Mathlib/.lake/packages/batteries/Batteries/Data/RBMap/Alter.lean
theorem Balanced.del {path : Path α}
    (hp : path.Balanced c₀ n₀ c n) (ht : t.DelProp c' n) (hc : c = black → c' ≠ red) :
    ∃ n, (path.del t c').Balanced black n

Proof state:
case blackL
α : Type u_1
c₀ : RBColor
n₀ : Nat
c : RBColor
n✝ : Nat
path : Path α
y✝ : RBNode α
c₂✝ : RBColor
n : Nat
parent✝ : Path α
v✝ : α
c₁✝ : RBColor
hb : y✝.Balanced c₂✝ n
hp : Path.Balanced c₀ n₀ parent✝ black (n + 1)
ih :
  ∀ {c' : RBColor} {t : RBNode α},
    DelProp c' t (n + 1) → (black = black → c' ≠ red) → ∃ n, (parent✝.del t c').Balanced black n
c' : RBColor
t : RBNode α
ht : DelProp c' t n
hc : c₁✝ = black → c' ≠ red
⊢ ∃ n, ((left black parent✝ v✝ y✝).del t c').Balanced black n

Tactic:
match c', n, ht with
| red, _, ⟨_, ha⟩ => exact ih ⟨_, rfl, .redred ⟨⟩ ha hb⟩ nofun
| black, _, ⟨_, rfl, ha⟩ => exact ih ⟨_, rfl, (hb.balLeft ha).imp fun _ => ⟨⟩⟩ nofun

Result:
no goals

Proof state:
α : Type u_1
c₀ : RBColor
n₀ : Nat
c : RBColor
n : Nat
c' : RBColor
t : RBNode α
path : Path α
hp : Path.Balanced c₀ n₀ path c n
ht : DelProp c' t n
hc : c = black → c' ≠ red
⊢ ∃ n, (path.del t c').Balanced black n

Tactic:
induction hp generalizing t c' with
| root => match c', ht with
  | red, ⟨_, h⟩ | black, ⟨_, _, h⟩ => exact h.setBlack
| @redL _ n _ _ hb hp ih => match c', n, ht with
  | red, _, _ => cases hc rfl rfl
  | black, _, ⟨_, rfl, ha⟩ => exact ih ((hb.balLeft ha).of_false nofun) nofun
| @redR _ n _ _ ha hp ih => match c', n, ht with
  | red, _, _ => cases hc rfl rfl
  | black, _, ⟨_, rfl, hb⟩ => exact ih ((ha.balRight hb).of_false nofun) nofun
| @blackL _ _ n _ _ _ hb hp ih => match c', n, ht with
  | red, _, ⟨_, ha⟩ => exact ih ⟨_, rfl, .redred ⟨⟩ ha hb⟩ nofun
  | black, _, ⟨_, rfl, ha⟩ => exact ih ⟨_, rfl, (hb.balLeft ha).imp fun _ => ⟨⟩⟩ nofun
| @blackR _ _ n _ _ _ ha hp ih =>  match c', n, ht with
  | red, _, ⟨_, hb⟩ => exact ih ⟨_, rfl, .redred ⟨⟩ ha hb⟩ nofun
  | black, _, ⟨_, rfl, hb⟩ => exact ih ⟨_, rfl, (ha.balRight hb).imp fun _ => ⟨⟩⟩ nofun

Result:
no goals
-- Mathlib/LinearAlgebra/AffineSpace/AffineMap.lean
theorem image_uIcc {k : Type*} [LinearOrderedField k] (f : k →ᵃ[k] k) (a b : k) :
    f '' Set.uIcc a b = Set.uIcc (f a) (f b)

Proof state:
k : Type u_10
inst✝ : LinearOrderedField k
f : k →ᵃ[k] k
a b : k
⊢ ⇑f '' Set.uIcc a b = Set.uIcc (f a) (f b)

Tactic:
have : ⇑f = (fun x => x + f 0) ∘ fun x => x * (f 1 - f 0) := by
  ext x
  change f x = x • (f 1 -ᵥ f 0) +ᵥ f 0
  rw [← f.linearMap_vsub, ← f.linear.map_smul, ← f.map_vadd]
  simp only [vsub_eq_sub, add_zero, mul_one, vadd_eq_add, sub_zero, smul_eq_mul]

Result:
k : Type u_10
inst✝ : LinearOrderedField k
f : k →ᵃ[k] k
a b : k
this : ⇑f = (fun x => x + f 0) ∘ fun x => x * (f 1 - f 0)
⊢ ⇑f '' Set.uIcc a b = Set.uIcc (f a) (f b)

Proof state:
k : Type u_10
inst✝ : LinearOrderedField k
f : k →ᵃ[k] k
a b : k
this : ⇑f = (fun x => x + f 0) ∘ fun x => x * (f 1 - f 0)
⊢ (fun x => x + f 0) '' ((fun x => x * (f 1 - f 0)) '' Set.uIcc a b) =
    Set.uIcc (((fun x => x + f 0) ∘ fun x => x * (f 1 - f 0)) a) (((fun x => x + f 0) ∘ fun x => x * (f 1 - f 0)) b)

Tactic:
simp only [Set.image_add_const_uIcc, Set.image_mul_const_uIcc, Function.comp_apply]

Result:
no goals

Proof state:
k : Type u_10
inst✝ : LinearOrderedField k
f : k →ᵃ[k] k
a b : k
⊢ ⇑f = (fun x => x + f 0) ∘ fun x => x * (f 1 - f 0)

Tactic:
ext x

Result:
case h
k : Type u_10
inst✝ : LinearOrderedField k
f : k →ᵃ[k] k
a b x : k
⊢ f x = ((fun x => x + f 0) ∘ fun x => x * (f 1 - f 0)) x

Proof state:
case h
k : Type u_10
inst✝ : LinearOrderedField k
f : k →ᵃ[k] k
a b x : k
⊢ f x = x • (f 1 -ᵥ f 0) +ᵥ f 0

Tactic:
rw [← f.linearMap_vsub, ← f.linear.map_smul, ← f.map_vadd]

Result:
case h
k : Type u_10
inst✝ : LinearOrderedField k
f : k →ᵃ[k] k
a b x : k
⊢ f x = f (x • (1 -ᵥ 0) +ᵥ 0)

Proof state:
case h
k : Type u_10
inst✝ : LinearOrderedField k
f : k →ᵃ[k] k
a b x : k
⊢ f x = ((fun x => x + f 0) ∘ fun x => x * (f 1 - f 0)) x

Tactic:
change f x = x • (f 1 -ᵥ f 0) +ᵥ f 0

Result:
case h
k : Type u_10
inst✝ : LinearOrderedField k
f : k →ᵃ[k] k
a b x : k
⊢ f x = x • (f 1 -ᵥ f 0) +ᵥ f 0

Proof state:
case h
k : Type u_10
inst✝ : LinearOrderedField k
f : k →ᵃ[k] k
a b x : k
⊢ f x = f (x • (1 -ᵥ 0) +ᵥ 0)

Tactic:
simp only [vsub_eq_sub, add_zero, mul_one, vadd_eq_add, sub_zero, smul_eq_mul]

Result:
no goals

Proof state:
k : Type u_10
inst✝ : LinearOrderedField k
f : k →ᵃ[k] k
a b : k
this : ⇑f = (fun x => x + f 0) ∘ fun x => x * (f 1 - f 0)
⊢ ⇑f '' Set.uIcc a b = Set.uIcc (f a) (f b)

Tactic:
rw [this, Set.image_comp]

Result:
k : Type u_10
inst✝ : LinearOrderedField k
f : k →ᵃ[k] k
a b : k
this : ⇑f = (fun x => x + f 0) ∘ fun x => x * (f 1 - f 0)
⊢ (fun x => x + f 0) '' ((fun x => x * (f 1 - f 0)) '' Set.uIcc a b) =
    Set.uIcc (((fun x => x + f 0) ∘ fun x => x * (f 1 - f 0)) a) (((fun x => x + f 0) ∘ fun x => x * (f 1 - f 0)) b)
-- Mathlib/NumberTheory/LegendreSymbol/JacobiSymbol.lean
theorem isSquare_of_jacobiSym_eq_one {a : ℤ} {p : ℕ} [Fact p.Prime] (h : J(a | p) = 1) :
    IsSquare (a : ZMod p) :=
  Classical.not_not.mp <| by rw [← nonsquare_iff_jacobiSym_eq_neg_one, h]; decide

Proof state:
a : ℤ
p : ℕ
inst✝ : Fact (Nat.Prime p)
h : J(a | p) = 1
⊢ ¬1 = -1

Tactic:
decide

Result:
no goals

Proof state:
a : ℤ
p : ℕ
inst✝ : Fact (Nat.Prime p)
h : J(a | p) = 1
⊢ ¬¬IsSquare ↑a

Tactic:
rw [← nonsquare_iff_jacobiSym_eq_neg_one, h]

Result:
a : ℤ
p : ℕ
inst✝ : Fact (Nat.Prime p)
h : J(a | p) = 1
⊢ ¬1 = -1
-- Mathlib/CategoryTheory/Shift/Adjunction.lean
@[reassoc]
lemma iso_hom_app (X : C) :
    (iso adj a).hom.app X = F.map ((adj.unit.app X)⟦a⟧') ≫
      F.map (G.map (((shiftFunctorCompIsoId D a b h).inv.app (F.obj X)))⟦a⟧') ≫
        F.map (((G.commShiftIso b).hom.app ((F.obj X)⟦a⟧))⟦a⟧') ≫
          F.map ((shiftFunctorCompIsoId C b a (by simp [eq_neg_of_add_eq_zero_left h])).hom.app
            (G.obj ((F.obj X)⟦a⟧))) ≫ adj.counit.app ((F.obj X)⟦a⟧)

Proof state:
C : Type u_1
D : Type u_2
inst✝⁵ : Category.{u_5, u_1} C
inst✝⁴ : Category.{u_4, u_2} D
F : C ⥤ D
G : D ⥤ C
adj : F ⊣ G
A : Type u_3
inst✝³ : AddGroup A
inst✝² : HasShift C A
inst✝¹ : HasShift D A
a : A
inst✝ : G.CommShift A
X : C
h : a + -a = 0
⊢ (iso adj a).hom.app X =
    F.map ((shiftFunctor C a).map (adj.unit.app X)) ≫
      F.map ((shiftFunctor C a).map (G.map ((shiftFunctorCompIsoId D a (-a) h).inv.app (F.obj X)))) ≫
        F.map ((shiftFunctor C a).map ((G.commShiftIso (-a)).hom.app ((shiftFunctor D a).obj (F.obj X)))) ≫
          F.map ((shiftFunctorCompIsoId C (-a) a ⋯).hom.app (G.obj ((shiftFunctor D a).obj (F.obj X)))) ≫
            adj.counit.app ((shiftFunctor D a).obj (F.obj X))

Tactic:
simp [iso, iso', shiftEquiv']

Result:
no goals

Proof state:
C : Type u_1
D : Type u_2
inst✝⁵ : Category.{u_5, u_1} C
inst✝⁴ : Category.{u_4, u_2} D
F : C ⥤ D
G : D ⥤ C
adj : F ⊣ G
A : Type u_3
inst✝³ : AddGroup A
inst✝² : HasShift C A
inst✝¹ : HasShift D A
a b : A
h : a + b = 0
inst✝ : G.CommShift A
X : C
⊢ (iso adj a).hom.app X =
    F.map ((shiftFunctor C a).map (adj.unit.app X)) ≫
      F.map ((shiftFunctor C a).map (G.map ((shiftFunctorCompIsoId D a b h).inv.app (F.obj X)))) ≫
        F.map ((shiftFunctor C a).map ((G.commShiftIso b).hom.app ((shiftFunctor D a).obj (F.obj X)))) ≫
          F.map ((shiftFunctorCompIsoId C b a ⋯).hom.app (G.obj ((shiftFunctor D a).obj (F.obj X)))) ≫
            adj.counit.app ((shiftFunctor D a).obj (F.obj X))

Tactic:
obtain rfl : b = -a := eq_neg_of_add_eq_zero_right h

Result:
C : Type u_1
D : Type u_2
inst✝⁵ : Category.{u_5, u_1} C
inst✝⁴ : Category.{u_4, u_2} D
F : C ⥤ D
G : D ⥤ C
adj : F ⊣ G
A : Type u_3
inst✝³ : AddGroup A
inst✝² : HasShift C A
inst✝¹ : HasShift D A
a : A
inst✝ : G.CommShift A
X : C
h : a + -a = 0
⊢ (iso adj a).hom.app X =
    F.map ((shiftFunctor C a).map (adj.unit.app X)) ≫
      F.map ((shiftFunctor C a).map (G.map ((shiftFunctorCompIsoId D a (-a) h).inv.app (F.obj X)))) ≫
        F.map ((shiftFunctor C a).map ((G.commShiftIso (-a)).hom.app ((shiftFunctor D a).obj (F.obj X)))) ≫
          F.map ((shiftFunctorCompIsoId C (-a) a ⋯).hom.app (G.obj ((shiftFunctor D a).obj (F.obj X)))) ≫
            adj.counit.app ((shiftFunctor D a).obj (F.obj X))

Proof state:
C : Type u_1
D : Type u_2
inst✝⁵ : Category.{?u.220855, u_1} C
inst✝⁴ : Category.{?u.220859, u_2} D
F : C ⥤ D
G : D ⥤ C
adj : F ⊣ G
A : Type u_3
inst✝³ : AddGroup A
inst✝² : HasShift C A
inst✝¹ : HasShift D A
a b : A
h : a + b = 0
inst✝ : G.CommShift A
X : C
⊢ b + a = 0

Tactic:
simp [eq_neg_of_add_eq_zero_left h]

Result:
no goals