harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/Topology/Order/Basic.lean
theorem pi_Ioo_mem_nhds (ha : ∀ i, a i < x i) (hb : ∀ i, x i < b i) : Ioo a b ∈ 𝓝 x

Proof state:
ι : Type u_1
π : ι → Type u_2
inst✝⁴ : Finite ι
inst✝³ : (i : ι) → LinearOrder (π i)
inst✝² : (i : ι) → TopologicalSpace (π i)
inst✝¹ : ∀ (i : ι), OrderTopology (π i)
a b x : (i : ι) → π i
inst✝ : Nonempty ι
ha : ∀ (i : ι), a i < x i
hb : ∀ (i : ι), x i < b i
i : ι
x✝ : i ∈ univ
⊢ Ioo (a i) (b i) ∈ 𝓝 (x i)

Tactic:
exact Ioo_mem_nhds (ha i) (hb i)

Result:
no goals

Proof state:
ι : Type u_1
π : ι → Type u_2
inst✝⁴ : Finite ι
inst✝³ : (i : ι) → LinearOrder (π i)
inst✝² : (i : ι) → TopologicalSpace (π i)
inst✝¹ : ∀ (i : ι), OrderTopology (π i)
a b x : (i : ι) → π i
inst✝ : Nonempty ι
ha : ∀ (i : ι), a i < x i
hb : ∀ (i : ι), x i < b i
⊢ Ioo a b ∈ 𝓝 x

Tactic:
refine mem_of_superset (set_pi_mem_nhds Set.finite_univ fun i _ => ?_) (pi_univ_Ioo_subset a b)

Result:
ι : Type u_1
π : ι → Type u_2
inst✝⁴ : Finite ι
inst✝³ : (i : ι) → LinearOrder (π i)
inst✝² : (i : ι) → TopologicalSpace (π i)
inst✝¹ : ∀ (i : ι), OrderTopology (π i)
a b x : (i : ι) → π i
inst✝ : Nonempty ι
ha : ∀ (i : ι), a i < x i
hb : ∀ (i : ι), x i < b i
i : ι
x✝ : i ∈ univ
⊢ Ioo (a i) (b i) ∈ 𝓝 (x i)
-- Mathlib/Data/List/Lattice.lean
theorem Subset.union_eq_right {xs ys : List α} (h : xs ⊆ ys) : xs ∪ ys = ys

Proof state:
case nil
α : Type u_1
inst✝ : DecidableEq α
ys : List α
h : [] ⊆ ys
⊢ [] ∪ ys = ys

Tactic:
simp

Result:
no goals

Proof state:
α : Type u_1
inst✝ : DecidableEq α
xs ys : List α
h : xs ⊆ ys
⊢ xs ∪ ys = ys

Tactic:
induction xs with
| nil => simp
| cons x xs ih =>
  rw [cons_union, insert_of_mem <| mem_union_right _ <| h <| mem_cons_self _ _,
    ih <| subset_of_cons_subset h]

Result:
no goals

Proof state:
case cons
α : Type u_1
inst✝ : DecidableEq α
ys : List α
x : α
xs : List α
ih : xs ⊆ ys → xs ∪ ys = ys
h : x :: xs ⊆ ys
⊢ x :: xs ∪ ys = ys

Tactic:
rw [cons_union, insert_of_mem <| mem_union_right _ <| h <| mem_cons_self _ _,
  ih <| subset_of_cons_subset h]

Result:
no goals
-- Mathlib/Order/SuccPred/Basic.lean
theorem _root_.OrderIso.map_succ [PartialOrder β] [SuccOrder β] (f : α ≃o β) (a : α) :
    f (succ a) = succ (f a)

Proof state:
α : Type u_1
β : Type u_2
inst✝³ : PartialOrder α
inst✝² : SuccOrder α
inst✝¹ : PartialOrder β
inst✝ : SuccOrder β
f : α ≃o β
a : α
⊢ f (succ a) = succ (f a)

Tactic:
by_cases h : IsMax a

Result:
case pos
α : Type u_1
β : Type u_2
inst✝³ : PartialOrder α
inst✝² : SuccOrder α
inst✝¹ : PartialOrder β
inst✝ : SuccOrder β
f : α ≃o β
a : α
h : IsMax a
⊢ f (succ a) = succ (f a)

case neg
α : Type u_1
β : Type u_2
inst✝³ : PartialOrder α
inst✝² : SuccOrder α
inst✝¹ : PartialOrder β
inst✝ : SuccOrder β
f : α ≃o β
a : α
h : ¬IsMax a
⊢ f (succ a) = succ (f a)

Proof state:
case pos
α : Type u_1
β : Type u_2
inst✝³ : PartialOrder α
inst✝² : SuccOrder α
inst✝¹ : PartialOrder β
inst✝ : SuccOrder β
f : α ≃o β
a : α
h : IsMax a
⊢ f (succ a) = succ (f a)

Tactic:
rw [h.succ_eq, (f.isMax_apply.2 h).succ_eq]

Result:
no goals

Proof state:
case neg
α : Type u_1
β : Type u_2
inst✝³ : PartialOrder α
inst✝² : SuccOrder α
inst✝¹ : PartialOrder β
inst✝ : SuccOrder β
f : α ≃o β
a : α
h : ¬IsMax a
⊢ f (succ a) = succ (f a)

Tactic:
exact (f.map_covBy.2 <| covBy_succ_of_not_isMax h).succ_eq.symm

Result:
no goals
-- Mathlib/Data/Semiquot.lean
theorem pure_isPure (a : α) : IsPure (pure a)
  | b, ab, c, ac => by
    rw [mem_pure] at ab ac
    rwa [← ac] at ab

Proof state:
α : Type u_1
a b : α
ab : b = a
c : α
ac : c = a
⊢ b = c

Tactic:
rwa [← ac] at ab

Result:
no goals

Proof state:
α : Type u_1
a b : α
ab : b ∈ pure a
c : α
ac : c ∈ pure a
⊢ b = c

Tactic:
rw [mem_pure] at ab ac

Result:
α : Type u_1
a b : α
ab : b = a
c : α
ac : c = a
⊢ b = c
-- Mathlib/Data/Fin/Basic.lean
theorem coe_int_sub_eq_mod {n : Nat} (u v : Fin n) :
    ((u - v : Fin n) : Int) = ((u : Int) - (v : Int)) % n

Proof state:
n : ℕ
u v : Fin n
⊢ (if v ≤ u then ↑↑u - ↑↑v else ↑↑u - ↑↑v + ↑n) = (↑↑u - ↑↑v) % ↑n

Tactic:
split

Result:
case isTrue
n : ℕ
u v : Fin n
h✝ : v ≤ u
⊢ ↑↑u - ↑↑v = (↑↑u - ↑↑v) % ↑n

case isFalse
n : ℕ
u v : Fin n
h✝ : ¬v ≤ u
⊢ ↑↑u - ↑↑v + ↑n = (↑↑u - ↑↑v) % ↑n

Proof state:
case isFalse
n : ℕ
u v : Fin n
h✝ : ¬v ≤ u
⊢ ↑↑u - ↑↑v + ↑n = (↑↑u - ↑↑v) % ↑n

Tactic:
rw [Int.emod_eq_add_self_emod, Int.emod_eq_of_lt] <;> omega

Result:
no goals

Proof state:
n : ℕ
u v : Fin n
⊢ ↑↑(u - v) = (↑↑u - ↑↑v) % ↑n

Tactic:
rw [coe_int_sub_eq_ite]

Result:
n : ℕ
u v : Fin n
⊢ (if v ≤ u then ↑↑u - ↑↑v else ↑↑u - ↑↑v + ↑n) = (↑↑u - ↑↑v) % ↑n

Proof state:
case isTrue
n : ℕ
u v : Fin n
h✝ : v ≤ u
⊢ ↑↑u - ↑↑v = (↑↑u - ↑↑v) % ↑n

Tactic:
rw [Int.emod_eq_of_lt] <;> omega

Result:
no goals
-- Mathlib/Data/DFinsupp/BigOperators.lean
theorem sumAddHom_single [∀ i, AddZeroClass (β i)] [AddCommMonoid γ] (φ : ∀ i, β i →+ γ) (i)
    (x : β i) : sumAddHom φ (single i x) = φ i x

Proof state:
ι : Type u
γ : Type w
β : ι → Type v
inst✝² : DecidableEq ι
inst✝¹ : (i : ι) → AddZeroClass (β i)
inst✝ : AddCommMonoid γ
φ : (i : ι) → β i →+ γ
i : ι
x : β i
⊢ ∑ i_1 ∈ {i}.toFinset, (φ i_1) (Pi.single i x i_1) = (φ i) x

Tactic:
rw [Multiset.toFinset_singleton, Finset.sum_singleton, Pi.single_eq_same]

Result:
no goals

Proof state:
ι : Type u
γ : Type w
β : ι → Type v
inst✝² : DecidableEq ι
inst✝¹ : (i : ι) → AddZeroClass (β i)
inst✝ : AddCommMonoid γ
φ : (i : ι) → β i →+ γ
i : ι
x : β i
⊢ (sumAddHom φ) (single i x) = (φ i) x

Tactic:
dsimp [sumAddHom, single, Trunc.lift_mk]

Result:
ι : Type u
γ : Type w
β : ι → Type v
inst✝² : DecidableEq ι
inst✝¹ : (i : ι) → AddZeroClass (β i)
inst✝ : AddCommMonoid γ
φ : (i : ι) → β i →+ γ
i : ι
x : β i
⊢ ∑ i_1 ∈ {i}.toFinset, (φ i_1) (Pi.single i x i_1) = (φ i) x
-- Mathlib/LinearAlgebra/LinearIndependent/Basic.lean
theorem LinearIndependent.units_smul_iff (v : ι → M) (w : ι → Rˣ) :
    LinearIndependent R (w • v) ↔ LinearIndependent R v

Proof state:
ι : Type u'
R : Type u_2
M : Type u_4
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
v : ι → M
w : ι → Rˣ
⊢ LinearIndependent R (w • v) ↔ LinearIndependent R v

Tactic:
refine ⟨fun h ↦ ?_, fun h ↦ h.units_smul w⟩

Result:
ι : Type u'
R : Type u_2
M : Type u_4
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
v : ι → M
w : ι → Rˣ
h : LinearIndependent R (w • v)
⊢ LinearIndependent R v

Proof state:
case h.e'_4
ι : Type u'
R : Type u_2
M : Type u_4
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
v : ι → M
w : ι → Rˣ
h : LinearIndependent R (w • v)
⊢ v = (fun i => (w i)⁻¹) • w • v

Tactic:
simp [funext_iff]

Result:
no goals

Proof state:
ι : Type u'
R : Type u_2
M : Type u_4
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
v : ι → M
w : ι → Rˣ
h : LinearIndependent R (w • v)
⊢ LinearIndependent R v

Tactic:
convert h.units_smul (fun i ↦ (w i)⁻¹)

Result:
case h.e'_4
ι : Type u'
R : Type u_2
M : Type u_4
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
v : ι → M
w : ι → Rˣ
h : LinearIndependent R (w • v)
⊢ v = (fun i => (w i)⁻¹) • w • v
-- Mathlib/NumberTheory/LegendreSymbol/JacobiSymbol.lean
theorem legendreSym.to_jacobiSym (p : ℕ) [fp : Fact p.Prime] (a : ℤ) :
    legendreSym p a = J(a | p)

Proof state:
p : ℕ
fp : Fact (Nat.Prime p)
a : ℤ
⊢ legendreSym p a = J(a | p)

Tactic:
simp only [jacobiSym, primeFactorsList_prime fp.1, List.prod_cons, List.prod_nil, mul_one,
  List.pmap]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/BitVec/Lemmas.lean
theorem getMsbD_cast (h : w = v) (x : BitVec w) : (x.cast h).getMsbD i = x.getMsbD i

Proof state:
w v i : Nat
h : w = v
x : BitVec w
⊢ (BitVec.cast h x).getMsbD i = x.getMsbD i

Tactic:
subst h

Result:
w i : Nat
x : BitVec w
⊢ (BitVec.cast ⋯ x).getMsbD i = x.getMsbD i

Proof state:
w i : Nat
x : BitVec w
⊢ (BitVec.cast ⋯ x).getMsbD i = x.getMsbD i

Tactic:
simp

Result:
no goals
-- Mathlib/Data/Nat/Cast/SetInterval.lean
theorem image_cast_int_Icc (a b : ℕ) : (↑) '' Icc a b = Icc (a : ℤ) b :=
  (castOrderEmbedding (α := ℤ)).image_Icc (by simp [ordConnected_Ici]) a b

Proof state:
a b : ℕ
⊢ (range ⇑castOrderEmbedding).OrdConnected

Tactic:
simp [ordConnected_Ici]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Int/Order.lean
theorem min_le_right (a b : Int) : min a b ≤ b

Proof state:
a b : Int
⊢ min a b ≤ b

Tactic:
rw [Int.min_def]

Result:
a b : Int
⊢ (if a ≤ b then a else b) ≤ b

Proof state:
a b : Int
⊢ (if a ≤ b then a else b) ≤ b

Tactic:
split <;> simp [*]

Result:
no goals
-- Mathlib/CategoryTheory/MorphismProperty/Comma.lean
@[simp]
lemma eqToHom_left {X Y : P.Comma L R Q W} (h : X = Y) :
    (eqToHom h).left = eqToHom (by rw [h])

Proof state:
A : Type u_1
inst✝⁴ : Category.{u_4, u_1} A
B : Type u_2
inst✝³ : Category.{u_5, u_2} B
T : Type u_3
inst✝² : Category.{u_6, u_3} T
L : A ⥤ T
R : B ⥤ T
P : MorphismProperty T
Q : MorphismProperty A
W : MorphismProperty B
inst✝¹ : Q.IsMultiplicative
inst✝ : W.IsMultiplicative
X : MorphismProperty.Comma L R P Q W
⊢ (eqToHom ⋯).left = eqToHom ⋯

Tactic:
rfl

Result:
no goals

Proof state:
A : Type u_1
inst✝⁴ : Category.{?u.84010, u_1} A
B : Type u_2
inst✝³ : Category.{?u.84017, u_2} B
T : Type u_3
inst✝² : Category.{?u.84024, u_3} T
L : A ⥤ T
R : B ⥤ T
P : MorphismProperty T
Q : MorphismProperty A
W : MorphismProperty B
inst✝¹ : Q.IsMultiplicative
inst✝ : W.IsMultiplicative
X Y : MorphismProperty.Comma L R P Q W
h : X = Y
⊢ X.left = Y.left

Tactic:
rw [h]

Result:
no goals

Proof state:
A : Type u_1
inst✝⁴ : Category.{u_4, u_1} A
B : Type u_2
inst✝³ : Category.{u_5, u_2} B
T : Type u_3
inst✝² : Category.{u_6, u_3} T
L : A ⥤ T
R : B ⥤ T
P : MorphismProperty T
Q : MorphismProperty A
W : MorphismProperty B
inst✝¹ : Q.IsMultiplicative
inst✝ : W.IsMultiplicative
X Y : MorphismProperty.Comma L R P Q W
h : X = Y
⊢ (eqToHom h).left = eqToHom ⋯

Tactic:
subst h

Result:
A : Type u_1
inst✝⁴ : Category.{u_4, u_1} A
B : Type u_2
inst✝³ : Category.{u_5, u_2} B
T : Type u_3
inst✝² : Category.{u_6, u_3} T
L : A ⥤ T
R : B ⥤ T
P : MorphismProperty T
Q : MorphismProperty A
W : MorphismProperty B
inst✝¹ : Q.IsMultiplicative
inst✝ : W.IsMultiplicative
X : MorphismProperty.Comma L R P Q W
⊢ (eqToHom ⋯).left = eqToHom ⋯
-- Mathlib/.lake/packages/lean4/src/lean/Init/Grind/Offset.lean
theorem Nat.ro_le (u w v k : Nat) : u ≤ w + k → w ≤ v → u ≤ v + k

Proof state:
u w v k : Nat
⊢ u ≤ w + k → w ≤ v → u ≤ v + k

Tactic:
omega

Result:
no goals
-- Mathlib/Analysis/Calculus/VectorField.lean
@[simp] lemma lieBracket_self : lieBracket 𝕜 V V = 0

Proof state:
𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
V : E → E
⊢ lieBracket 𝕜 V V = 0

Tactic:
ext x

Result:
case h
𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
V : E → E
x : E
⊢ lieBracket 𝕜 V V x = 0 x

Proof state:
case h
𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
V : E → E
x : E
⊢ lieBracket 𝕜 V V x = 0 x

Tactic:
simp [lieBracket]

Result:
no goals
-- Mathlib/CategoryTheory/MorphismProperty/Limits.lean
lemma coproducts_monotone : Monotone (coproducts.{w} (C := C))

Proof state:
C : Type u
inst✝ : Category.{v, u} C
⊢ Monotone coproducts.{w, v, u}

Tactic:
rintro W₁ W₂ h X Y f hf

Result:
C : Type u
inst✝ : Category.{v, u} C
W₁ W₂ : MorphismProperty C
h : W₁ ≤ W₂
X Y : C
f : X ⟶ Y
hf : coproducts.{w, v, u} W₁ f
⊢ coproducts.{w, v, u} W₂ f

Proof state:
C : Type u
inst✝ : Category.{v, u} C
W₁ W₂ : MorphismProperty C
h : W₁ ≤ W₂
X Y : C
f : X ⟶ Y
hf : coproducts.{w, v, u} W₁ f
⊢ coproducts.{w, v, u} W₂ f

Tactic:
rw [coproducts_iff] at hf

Result:
C : Type u
inst✝ : Category.{v, u} C
W₁ W₂ : MorphismProperty C
h : W₁ ≤ W₂
X Y : C
f : X ⟶ Y
hf : ∃ J, W₁.colimitsOfShape (Discrete J) f
⊢ coproducts.{w, v, u} W₂ f

Proof state:
case intro
C : Type u
inst✝ : Category.{v, u} C
W₁ W₂ : MorphismProperty C
h : W₁ ≤ W₂
X Y : C
f : X ⟶ Y
J : Type w
hf : W₁.colimitsOfShape (Discrete J) f
⊢ coproducts.{w, v, u} W₂ f

Tactic:
exact W₂.colimitsOfShape_le_coproducts J _
  (colimitsOfShape_monotone h _ _ hf)

Result:
no goals

Proof state:
C : Type u
inst✝ : Category.{v, u} C
W₁ W₂ : MorphismProperty C
h : W₁ ≤ W₂
X Y : C
f : X ⟶ Y
hf : ∃ J, W₁.colimitsOfShape (Discrete J) f
⊢ coproducts.{w, v, u} W₂ f

Tactic:
obtain ⟨J, hf⟩ := hf

Result:
case intro
C : Type u
inst✝ : Category.{v, u} C
W₁ W₂ : MorphismProperty C
h : W₁ ≤ W₂
X Y : C
f : X ⟶ Y
J : Type w
hf : W₁.colimitsOfShape (Discrete J) f
⊢ coproducts.{w, v, u} W₂ f
-- Mathlib/Analysis/SpecialFunctions/Pow/Deriv.lean
theorem hasStrictDerivAt_const_rpow {a : ℝ} (ha : 0 < a) (x : ℝ) :
    HasStrictDerivAt (fun x => a ^ x) (a ^ x * log a) x

Proof state:
a : ℝ
ha : 0 < a
x : ℝ
⊢ HasStrictDerivAt (fun x => a ^ x) (a ^ x * log a) x

Tactic:
simpa using (hasStrictDerivAt_const _ _).rpow (hasStrictDerivAt_id x) ha

Result:
no goals
-- Mathlib/.lake/packages/batteries/Batteries/Data/Nat/Lemmas.lean
theorem ofBits_lt_two_pow (f : Fin n → Bool) : ofBits f < 2 ^ n

Proof state:
case zero
f : Fin 0 → Bool
⊢ ofBits f < 2 ^ 0

Tactic:
simp

Result:
no goals

Proof state:
n : Nat
f : Fin n → Bool
⊢ ofBits f < 2 ^ n

Tactic:
induction n with
| zero => simp
| succ n ih =>
  calc ofBits f
      = 2 * ofBits (f ∘ Fin.succ) + (f 0).toNat := ofBits_succ ..
    _ < 2 * (ofBits (f ∘ Fin.succ) + 1) := Nat.add_lt_add_left (Bool.toNat_lt _) ..
    _ ≤ 2 * 2 ^ n := Nat.mul_le_mul_left 2 (ih ..)
    _ = 2 ^ (n + 1) := Nat.pow_add_one' .. |>.symm

Result:
no goals

Proof state:
case succ
n : Nat
ih : ∀ (f : Fin n → Bool), ofBits f < 2 ^ n
f : Fin (n + 1) → Bool
⊢ ofBits f < 2 ^ (n + 1)

Tactic:
calc ofBits f
    = 2 * ofBits (f ∘ Fin.succ) + (f 0).toNat := ofBits_succ ..
  _ < 2 * (ofBits (f ∘ Fin.succ) + 1) := Nat.add_lt_add_left (Bool.toNat_lt _) ..
  _ ≤ 2 * 2 ^ n := Nat.mul_le_mul_left 2 (ih ..)
  _ = 2 ^ (n + 1) := Nat.pow_add_one' .. |>.symm

Result:
no goals
-- Mathlib/AlgebraicGeometry/Morphisms/Proper.lean
@[stacks 01W6 "(2)"]
lemma IsProper.of_comp_of_isSeparated [IsProper (f ≫ g)] [IsSeparated g] :
    IsProper f

Proof state:
X Y Z : Scheme
f : X ⟶ Y
g : Y ⟶ Z
inst✝¹ : IsProper (f ≫ g)
inst✝ : IsSeparated g
⊢ IsProper (Limits.pullback.lift (𝟙 X) f ⋯ ≫ Limits.pullback.snd (f ≫ g) g)

Tactic:
have := MorphismProperty.pullback_snd (P := @IsProper) (f ≫ g) g inferInstance

Result:
X Y Z : Scheme
f : X ⟶ Y
g : Y ⟶ Z
inst✝¹ : IsProper (f ≫ g)
inst✝ : IsSeparated g
this : IsProper (Limits.pullback.snd (f ≫ g) g)
⊢ IsProper (Limits.pullback.lift (𝟙 X) f ⋯ ≫ Limits.pullback.snd (f ≫ g) g)

Proof state:
X Y Z : Scheme
f : X ⟶ Y
g : Y ⟶ Z
inst✝¹ : IsProper (f ≫ g)
inst✝ : IsSeparated g
⊢ IsProper f

Tactic:
rw [← Limits.pullback.lift_snd (𝟙 _) f (Category.id_comp (f ≫ g))]

Result:
X Y Z : Scheme
f : X ⟶ Y
g : Y ⟶ Z
inst✝¹ : IsProper (f ≫ g)
inst✝ : IsSeparated g
⊢ IsProper (Limits.pullback.lift (𝟙 X) f ⋯ ≫ Limits.pullback.snd (f ≫ g) g)

Proof state:
X Y Z : Scheme
f : X ⟶ Y
g : Y ⟶ Z
inst✝¹ : IsProper (f ≫ g)
inst✝ : IsSeparated g
this : IsProper (Limits.pullback.snd (f ≫ g) g)
⊢ IsProper (Limits.pullback.lift (𝟙 X) f ⋯ ≫ Limits.pullback.snd (f ≫ g) g)

Tactic:
infer_instance

Result:
no goals
-- Mathlib/CategoryTheory/Abelian/Projective/Dimension.lean
lemma hasProjectiveDimensionLT_X₂ (h₁ : HasProjectiveDimensionLT S.X₁ n)
    (h₃ : HasProjectiveDimensionLT S.X₃ n) :
    HasProjectiveDimensionLT S.X₂ n

Proof state:
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Abelian C
S : ShortComplex C
hS : S.ShortExact
n : ℕ
h₁ : HasProjectiveDimensionLT S.X₁ n
h₃ : HasProjectiveDimensionLT S.X₃ n
this : HasExt C := HasExt.standard C
i : ℕ
hi : n ≤ i
Y : C
x₂ : Ext S.X₂ Y i
⊢ x₂ = 0

Tactic:
obtain ⟨x₃, rfl⟩ := Ext.contravariant_sequence_exact₂ hS _ x₂
  (Ext.eq_zero_of_hasProjectiveDimensionLT _ n hi)

Result:
case intro
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Abelian C
S : ShortComplex C
hS : S.ShortExact
n : ℕ
h₁ : HasProjectiveDimensionLT S.X₁ n
h₃ : HasProjectiveDimensionLT S.X₃ n
this : HasExt C := HasExt.standard C
i : ℕ
hi : n ≤ i
Y : C
x₃ : Ext S.X₃ Y i
⊢ (Ext.mk₀ S.g).comp x₃ ⋯ = 0

Proof state:
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Abelian C
S : ShortComplex C
hS : S.ShortExact
n : ℕ
h₁ : HasProjectiveDimensionLT S.X₁ n
h₃ : HasProjectiveDimensionLT S.X₃ n
this : HasExt C := HasExt.standard C
⊢ HasProjectiveDimensionLT S.X₂ n

Tactic:
rw [hasProjectiveDimensionLT_iff]

Result:
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Abelian C
S : ShortComplex C
hS : S.ShortExact
n : ℕ
h₁ : HasProjectiveDimensionLT S.X₁ n
h₃ : HasProjectiveDimensionLT S.X₃ n
this : HasExt C := HasExt.standard C
⊢ ∀ (i : ℕ), n ≤ i → ∀ ⦃Y : C⦄ (e : Ext S.X₂ Y i), e = 0

Proof state:
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Abelian C
S : ShortComplex C
hS : S.ShortExact
n : ℕ
h₁ : HasProjectiveDimensionLT S.X₁ n
h₃ : HasProjectiveDimensionLT S.X₃ n
this : HasExt C := HasExt.standard C
⊢ ∀ (i : ℕ), n ≤ i → ∀ ⦃Y : C⦄ (e : Ext S.X₂ Y i), e = 0

Tactic:
intro i hi Y x₂

Result:
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Abelian C
S : ShortComplex C
hS : S.ShortExact
n : ℕ
h₁ : HasProjectiveDimensionLT S.X₁ n
h₃ : HasProjectiveDimensionLT S.X₃ n
this : HasExt C := HasExt.standard C
i : ℕ
hi : n ≤ i
Y : C
x₂ : Ext S.X₂ Y i
⊢ x₂ = 0

Proof state:
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Abelian C
S : ShortComplex C
hS : S.ShortExact
n : ℕ
h₁ : HasProjectiveDimensionLT S.X₁ n
h₃ : HasProjectiveDimensionLT S.X₃ n
⊢ HasProjectiveDimensionLT S.X₂ n

Tactic:
letI := HasExt.standard C

Result:
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Abelian C
S : ShortComplex C
hS : S.ShortExact
n : ℕ
h₁ : HasProjectiveDimensionLT S.X₁ n
h₃ : HasProjectiveDimensionLT S.X₃ n
this : HasExt C := HasExt.standard C
⊢ HasProjectiveDimensionLT S.X₂ n

Proof state:
case intro
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Abelian C
S : ShortComplex C
hS : S.ShortExact
n : ℕ
h₁ : HasProjectiveDimensionLT S.X₁ n
h₃ : HasProjectiveDimensionLT S.X₃ n
this : HasExt C := HasExt.standard C
i : ℕ
hi : n ≤ i
Y : C
x₃ : Ext S.X₃ Y i
⊢ (Ext.mk₀ S.g).comp x₃ ⋯ = 0

Tactic:
rw [x₃.eq_zero_of_hasProjectiveDimensionLT n hi, Ext.comp_zero]

Result:
no goals
-- Mathlib/RingTheory/IsAdjoinRoot.lean
theorem apply_eq_lift (h : IsAdjoinRoot S f) (g : S →+* T) (hmap : ∀ a, g (algebraMap R S a) = i a)
    (hroot : g h.root = x) (a : S) : g a = h.lift i x hx a

Proof state:
R : Type u
S : Type v
inst✝³ : CommRing R
inst✝² : Ring S
f : R[X]
inst✝¹ : Algebra R S
T : Type u_1
inst✝ : CommRing T
i : R →+* T
x : T
hx : eval₂ i x f = 0
h : IsAdjoinRoot S f
g : S →+* T
hmap : ∀ (a : R), g ((algebraMap R S) a) = i a
hroot : g h.root = x
a : S
⊢ g a = (lift i x h hx) a

Tactic:
rw [← h.map_repr a, Polynomial.as_sum_range_C_mul_X_pow (h.repr a)]

Result:
R : Type u
S : Type v
inst✝³ : CommRing R
inst✝² : Ring S
f : R[X]
inst✝¹ : Algebra R S
T : Type u_1
inst✝ : CommRing T
i : R →+* T
x : T
hx : eval₂ i x f = 0
h : IsAdjoinRoot S f
g : S →+* T
hmap : ∀ (a : R), g ((algebraMap R S) a) = i a
hroot : g h.root = x
a : S
⊢ g (h.map (∑ i ∈ Finset.range ((h.repr a).natDegree + 1), C ((h.repr a).coeff i) * X ^ i)) =
    (lift i x h hx) (h.map (∑ i ∈ Finset.range ((h.repr a).natDegree + 1), C ((h.repr a).coeff i) * X ^ i))

Proof state:
R : Type u
S : Type v
inst✝³ : CommRing R
inst✝² : Ring S
f : R[X]
inst✝¹ : Algebra R S
T : Type u_1
inst✝ : CommRing T
i : R →+* T
x : T
hx : eval₂ i x f = 0
h : IsAdjoinRoot S f
g : S →+* T
hmap : ∀ (a : R), g ((algebraMap R S) a) = i a
hroot : g h.root = x
a : S
⊢ g (h.map (∑ i ∈ Finset.range ((h.repr a).natDegree + 1), C ((h.repr a).coeff i) * X ^ i)) =
    (lift i x h hx) (h.map (∑ i ∈ Finset.range ((h.repr a).natDegree + 1), C ((h.repr a).coeff i) * X ^ i))

Tactic:
simp only [map_sum, map_mul, map_pow, h.map_X, hroot, ← h.algebraMap_apply, hmap, lift_root,
  lift_algebraMap]

Result:
no goals
-- Mathlib/Algebra/Order/Antidiag/Nat.lean
theorem finMulAntidiag_zero_left {n : ℕ} (hn : n ≠ 1) :
    finMulAntidiag 0 n = ∅

Proof state:
case h
n : ℕ
hn : n ≠ 1
a✝ : Fin 0 → ℕ
⊢ a✝ ∈ finMulAntidiag 0 n ↔ a✝ ∈ ∅

Tactic:
simp [hn.symm]

Result:
no goals

Proof state:
n : ℕ
hn : n ≠ 1
⊢ finMulAntidiag 0 n = ∅

Tactic:
ext

Result:
case h
n : ℕ
hn : n ≠ 1
a✝ : Fin 0 → ℕ
⊢ a✝ ∈ finMulAntidiag 0 n ↔ a✝ ∈ ∅
-- Mathlib/NumberTheory/Cyclotomic/Discriminant.lean
theorem discr_prime_pow_ne_two' [IsCyclotomicExtension {p ^ (k + 1)} K L] [hp : Fact (p : ℕ).Prime]
    (hζ : IsPrimitiveRoot ζ ↑(p ^ (k + 1))) (hirr : Irreducible (cyclotomic (↑(p ^ (k + 1)) : ℕ) K))
    (hk : p ^ (k + 1) ≠ 2) : discr K (hζ.powerBasis K).basis =
      (-1) ^ ((p : ℕ) ^ k * (p - 1) / 2) * p ^ ((p : ℕ) ^ k * ((p - 1) * (k + 1) - 1))

Proof state:
p : ℕ+
k : ℕ
K : Type u
L : Type v
ζ : L
inst✝³ : Field K
inst✝² : Field L
inst✝¹ : Algebra K L
inst✝ : IsCyclotomicExtension {p ^ (k + 1)} K L
hp : Fact (Nat.Prime ↑p)
hζ : IsPrimitiveRoot ζ ↑(p ^ (k + 1))
hirr : Irreducible (cyclotomic (↑(p ^ (k + 1))) K)
hk : p ^ (k + 1) ≠ 2
⊢ discr K ⇑(IsPrimitiveRoot.powerBasis K hζ).basis =
    (-1) ^ (↑p ^ k * (↑p - 1) / 2) * ↑↑p ^ (↑p ^ k * ((↑p - 1) * (k + 1) - 1))

Tactic:
simpa [totient_prime_pow hp.out (succ_pos k)] using discr_prime_pow_ne_two hζ hirr hk

Result:
no goals
-- Mathlib/GroupTheory/CosetCover.lean
theorem Subspace.top_mem_of_biUnion_eq_univ (hcovers : ⋃ p ∈ s, (p : Set E) = Set.univ) :
    ⊤ ∈ s

Proof state:
k : Type u_1
E : Type u_2
inst✝³ : DivisionRing k
inst✝² : Infinite k
inst✝¹ : AddCommGroup E
inst✝ : Module k E
s : Finset (Subspace k E)
hcovers : ⋃ p ∈ s, ↑p = Set.univ
⊢ ⊤ ∈ s

Tactic:
contrapose! hcovers

Result:
k : Type u_1
E : Type u_2
inst✝³ : DivisionRing k
inst✝² : Infinite k
inst✝¹ : AddCommGroup E
inst✝ : Module k E
s : Finset (Subspace k E)
hcovers : ⊤ ∉ s
⊢ ⋃ p ∈ s, ↑p ≠ Set.univ

Proof state:
k : Type u_1
E : Type u_2
inst✝³ : DivisionRing k
inst✝² : Infinite k
inst✝¹ : AddCommGroup E
inst✝ : Module k E
s : Finset (Subspace k E)
hcovers : ⊤ ∉ s
⊢ ⋃ p ∈ s, ↑p ≠ Set.univ

Tactic:
exact Subspace.biUnion_ne_univ_of_top_nmem hcovers

Result:
no goals
-- Mathlib/Analysis/InnerProductSpace/PiL2.lean
theorem repr_injective :
    Injective (repr : OrthonormalBasis ι 𝕜 E → E ≃ₗᵢ[𝕜] EuclideanSpace 𝕜 ι) := fun f g h => by
  cases f
  cases g
  congr

Proof state:
case ofRepr.ofRepr
ι : Type u_1
𝕜 : Type u_3
inst✝³ : RCLike 𝕜
E : Type u_4
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace 𝕜 E
inst✝ : Fintype ι
repr✝¹ repr✝ : E ≃ₗᵢ[𝕜] EuclideanSpace 𝕜 ι
h : { repr := repr✝¹ }.repr = { repr := repr✝ }.repr
⊢ { repr := repr✝¹ } = { repr := repr✝ }

Tactic:
congr

Result:
no goals

Proof state:
case ofRepr
ι : Type u_1
𝕜 : Type u_3
inst✝³ : RCLike 𝕜
E : Type u_4
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace 𝕜 E
inst✝ : Fintype ι
g : OrthonormalBasis ι 𝕜 E
repr✝ : E ≃ₗᵢ[𝕜] EuclideanSpace 𝕜 ι
h : { repr := repr✝ }.repr = g.repr
⊢ { repr := repr✝ } = g

Tactic:
cases g

Result:
case ofRepr.ofRepr
ι : Type u_1
𝕜 : Type u_3
inst✝³ : RCLike 𝕜
E : Type u_4
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace 𝕜 E
inst✝ : Fintype ι
repr✝¹ repr✝ : E ≃ₗᵢ[𝕜] EuclideanSpace 𝕜 ι
h : { repr := repr✝¹ }.repr = { repr := repr✝ }.repr
⊢ { repr := repr✝¹ } = { repr := repr✝ }

Proof state:
ι : Type u_1
𝕜 : Type u_3
inst✝³ : RCLike 𝕜
E : Type u_4
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace 𝕜 E
inst✝ : Fintype ι
f g : OrthonormalBasis ι 𝕜 E
h : f.repr = g.repr
⊢ f = g

Tactic:
cases f

Result:
case ofRepr
ι : Type u_1
𝕜 : Type u_3
inst✝³ : RCLike 𝕜
E : Type u_4
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace 𝕜 E
inst✝ : Fintype ι
g : OrthonormalBasis ι 𝕜 E
repr✝ : E ≃ₗᵢ[𝕜] EuclideanSpace 𝕜 ι
h : { repr := repr✝ }.repr = g.repr
⊢ { repr := repr✝ } = g