harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/GroupTheory/GroupExtension/Basic.lean
theorem exists_mul_eq_mul_mul_inl : ∃ n : N, σ (g₁ * g₂) = σ g₁ * σ g₂ * S.inl n

Proof state:
case h
N : Type u_1
G : Type u_2
inst✝² : Group N
inst✝¹ : Group G
E : Type u_3
inst✝ : Group E
S : GroupExtension N E G
σ : S.Section
g₁ g₂ : G
n : N
hn : S.inl n = (σ (g₁ * g₂))⁻¹ * σ g₁ * σ g₂
⊢ σ (g₁ * g₂) = σ g₁ * σ g₂ * S.inl n⁻¹

Tactic:
rw [map_inv, eq_mul_inv_iff_mul_eq, ← eq_inv_mul_iff_mul_eq, ← mul_assoc, hn]

Result:
no goals

Proof state:
N : Type u_1
G : Type u_2
inst✝² : Group N
inst✝¹ : Group G
E : Type u_3
inst✝ : Group E
S : GroupExtension N E G
σ : S.Section
g₁ g₂ : G
⊢ ∃ n, σ (g₁ * g₂) = σ g₁ * σ g₂ * S.inl n

Tactic:
obtain ⟨n, hn⟩ := mul_inv_mul_mul_mem_range_inl σ g₁ g₂

Result:
case intro
N : Type u_1
G : Type u_2
inst✝² : Group N
inst✝¹ : Group G
E : Type u_3
inst✝ : Group E
S : GroupExtension N E G
σ : S.Section
g₁ g₂ : G
n : N
hn : S.inl n = (σ (g₁ * g₂))⁻¹ * σ g₁ * σ g₂
⊢ ∃ n, σ (g₁ * g₂) = σ g₁ * σ g₂ * S.inl n

Proof state:
case intro
N : Type u_1
G : Type u_2
inst✝² : Group N
inst✝¹ : Group G
E : Type u_3
inst✝ : Group E
S : GroupExtension N E G
σ : S.Section
g₁ g₂ : G
n : N
hn : S.inl n = (σ (g₁ * g₂))⁻¹ * σ g₁ * σ g₂
⊢ ∃ n, σ (g₁ * g₂) = σ g₁ * σ g₂ * S.inl n

Tactic:
use n⁻¹

Result:
case h
N : Type u_1
G : Type u_2
inst✝² : Group N
inst✝¹ : Group G
E : Type u_3
inst✝ : Group E
S : GroupExtension N E G
σ : S.Section
g₁ g₂ : G
n : N
hn : S.inl n = (σ (g₁ * g₂))⁻¹ * σ g₁ * σ g₂
⊢ σ (g₁ * g₂) = σ g₁ * σ g₂ * S.inl n⁻¹
-- Mathlib/LinearAlgebra/RootSystem/Finite/CanonicalBilinear.lean
lemma pairingIn_zero_iff [Finite ι] [NoZeroDivisors R] :
    P.pairingIn S i j = 0 ↔ P.pairingIn S j i = 0

Proof state:
ι : Type u_1
R : Type u_2
M : Type u_3
N : Type u_4
inst✝¹⁰ : CommRing R
inst✝⁹ : AddCommGroup M
inst✝⁸ : Module R M
inst✝⁷ : AddCommGroup N
inst✝⁶ : Module R N
P : RootPairing ι R M N
S : Type u_5
inst✝⁵ : LinearOrderedCommRing S
inst✝⁴ : Algebra S R
inst✝³ : FaithfulSMul S R
inst✝² : P.IsValuedIn S
i j : ι
inst✝¹ : Finite ι
inst✝ : NoZeroDivisors R
_i : Fintype ι := Fintype.ofFinite ι
⊢ P.pairingIn S i j = 0 ↔ P.pairingIn S j i = 0

Tactic:
simp only [← FaithfulSMul.algebraMap_eq_zero_iff S R, algebraMap_pairingIn]

Result:
ι : Type u_1
R : Type u_2
M : Type u_3
N : Type u_4
inst✝¹⁰ : CommRing R
inst✝⁹ : AddCommGroup M
inst✝⁸ : Module R M
inst✝⁷ : AddCommGroup N
inst✝⁶ : Module R N
P : RootPairing ι R M N
S : Type u_5
inst✝⁵ : LinearOrderedCommRing S
inst✝⁴ : Algebra S R
inst✝³ : FaithfulSMul S R
inst✝² : P.IsValuedIn S
i j : ι
inst✝¹ : Finite ι
inst✝ : NoZeroDivisors R
_i : Fintype ι := Fintype.ofFinite ι
⊢ P.pairing i j = 0 ↔ P.pairing j i = 0

Proof state:
ι : Type u_1
R : Type u_2
M : Type u_3
N : Type u_4
inst✝¹⁰ : CommRing R
inst✝⁹ : AddCommGroup M
inst✝⁸ : Module R M
inst✝⁷ : AddCommGroup N
inst✝⁶ : Module R N
P : RootPairing ι R M N
S : Type u_5
inst✝⁵ : LinearOrderedCommRing S
inst✝⁴ : Algebra S R
inst✝³ : FaithfulSMul S R
inst✝² : P.IsValuedIn S
i j : ι
inst✝¹ : Finite ι
inst✝ : NoZeroDivisors R
_i : Fintype ι := Fintype.ofFinite ι
⊢ P.pairing i j = 0 ↔ P.pairing j i = 0

Tactic:
exact pairing_zero_iff (P.posRootForm S) i j

Result:
no goals

Proof state:
ι : Type u_1
R : Type u_2
M : Type u_3
N : Type u_4
inst✝¹⁰ : CommRing R
inst✝⁹ : AddCommGroup M
inst✝⁸ : Module R M
inst✝⁷ : AddCommGroup N
inst✝⁶ : Module R N
P : RootPairing ι R M N
S : Type u_5
inst✝⁵ : LinearOrderedCommRing S
inst✝⁴ : Algebra S R
inst✝³ : FaithfulSMul S R
inst✝² : P.IsValuedIn S
i j : ι
inst✝¹ : Finite ι
inst✝ : NoZeroDivisors R
⊢ P.pairingIn S i j = 0 ↔ P.pairingIn S j i = 0

Tactic:
let _i : Fintype ι := Fintype.ofFinite ι

Result:
ι : Type u_1
R : Type u_2
M : Type u_3
N : Type u_4
inst✝¹⁰ : CommRing R
inst✝⁹ : AddCommGroup M
inst✝⁸ : Module R M
inst✝⁷ : AddCommGroup N
inst✝⁶ : Module R N
P : RootPairing ι R M N
S : Type u_5
inst✝⁵ : LinearOrderedCommRing S
inst✝⁴ : Algebra S R
inst✝³ : FaithfulSMul S R
inst✝² : P.IsValuedIn S
i j : ι
inst✝¹ : Finite ι
inst✝ : NoZeroDivisors R
_i : Fintype ι := Fintype.ofFinite ι
⊢ P.pairingIn S i j = 0 ↔ P.pairingIn S j i = 0
-- Mathlib/Data/List/MinMax.lean
theorem le_maximum_of_length_pos_of_mem (h : a ∈ l) (w : 0 < l.length) :
    a ≤ l.maximum_of_length_pos w

Proof state:
α : Type u_1
inst✝ : LinearOrder α
l : List α
a : α
h : a ∈ l
w : 0 < l.length
⊢ a ≤ maximum_of_length_pos w

Tactic:
simp only [le_maximum_of_length_pos_iff]

Result:
α : Type u_1
inst✝ : LinearOrder α
l : List α
a : α
h : a ∈ l
w : 0 < l.length
⊢ ↑a ≤ l.maximum

Proof state:
α : Type u_1
inst✝ : LinearOrder α
l : List α
a : α
h : a ∈ l
w : 0 < l.length
⊢ ↑a ≤ l.maximum

Tactic:
exact le_maximum_of_mem' h

Result:
no goals
-- Mathlib/Algebra/FreeAlgebra/Cardinality.lean
theorem cardinalMk_eq_lift [IsEmpty X] : #(FreeAlgebra R X) = Cardinal.lift.{v} #R

Proof state:
R : Type u
inst✝¹ : CommSemiring R
X : Type v
inst✝ : IsEmpty X
this : Cardinal.lift.{u, max u v} #(FreeMonoid X →₀ R) = Cardinal.lift.{max u v, u} #R
⊢ #(FreeAlgebra R X) = Cardinal.lift.{v, u} #R

Tactic:
rw [lift_id'.{u, v}, lift_umax] at this

Result:
R : Type u
inst✝¹ : CommSemiring R
X : Type v
inst✝ : IsEmpty X
this : #(FreeMonoid X →₀ R) = Cardinal.lift.{v, u} #R
⊢ #(FreeAlgebra R X) = Cardinal.lift.{v, u} #R

Proof state:
R : Type u
inst✝¹ : CommSemiring R
X : Type v
inst✝ : IsEmpty X
this : #(FreeMonoid X →₀ R) = Cardinal.lift.{v, u} #R
⊢ #(FreeAlgebra R X) = Cardinal.lift.{v, u} #R

Tactic:
rwa [equivMonoidAlgebraFreeMonoid.toEquiv.cardinal_eq, MonoidAlgebra]

Result:
no goals

Proof state:
R : Type u
inst✝¹ : CommSemiring R
X : Type v
inst✝ : IsEmpty X
⊢ #(FreeAlgebra R X) = Cardinal.lift.{v, u} #R

Tactic:
have := lift_mk_eq'.2 ⟨show (FreeMonoid X →₀ R) ≃ R from Equiv.finsuppUnique⟩

Result:
R : Type u
inst✝¹ : CommSemiring R
X : Type v
inst✝ : IsEmpty X
this : Cardinal.lift.{u, max u v} #(FreeMonoid X →₀ R) = Cardinal.lift.{max u v, u} #R
⊢ #(FreeAlgebra R X) = Cardinal.lift.{v, u} #R
-- Mathlib/Data/Finset/Image.lean
theorem map_toFinset [DecidableEq α] [DecidableEq β] {s : Multiset α} :
    s.toFinset.map f = (s.map f).toFinset :=
  ext fun _ => by simp only [mem_map, Multiset.mem_map, exists_prop, Multiset.mem_toFinset]

Proof state:
α : Type u_1
β : Type u_2
f : α ↪ β
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
s : Multiset α
x✝ : β
⊢ x✝ ∈ map f s.toFinset ↔ x✝ ∈ (Multiset.map (⇑f) s).toFinset

Tactic:
simp only [mem_map, Multiset.mem_map, exists_prop, Multiset.mem_toFinset]

Result:
no goals
-- Mathlib/Data/Finset/Piecewise.lean
@[simp]
lemma piecewise_insert_of_ne [DecidableEq ι] {i j : ι} [∀ i, Decidable (i ∈ insert j s)]
    (h : i ≠ j) : (insert j s).piecewise f g i = s.piecewise f g i

Proof state:
ι : Type u_1
π : ι → Sort u_2
s : Finset ι
f g : (i : ι) → π i
inst✝² : (j : ι) → Decidable (j ∈ s)
inst✝¹ : DecidableEq ι
i j : ι
inst✝ : (i : ι) → Decidable (i ∈ insert j s)
h : i ≠ j
⊢ (insert j s).piecewise f g i = s.piecewise f g i

Tactic:
simp [piecewise, h]

Result:
no goals
-- Mathlib/LinearAlgebra/Eigenspace/Zero.lean
lemma IsNilpotent.charpoly_eq_X_pow_finrank {φ : Module.End R M} (h : IsNilpotent φ) :
    φ.charpoly = X ^ finrank R M

Proof state:
case h
R : Type u_1
M : Type u_3
inst✝⁵ : CommRing R
inst✝⁴ : IsDomain R
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : Module.Finite R M
inst✝ : Free R M
φ : End R M
h : IsNilpotent φ
⊢ IsNilpotent (LinearMap.charpoly φ - X ^ Fintype.card (ChooseBasisIndex R M))

Tactic:
apply Matrix.isNilpotent_charpoly_sub_pow_of_isNilpotent

Result:
case h.hM
R : Type u_1
M : Type u_3
inst✝⁵ : CommRing R
inst✝⁴ : IsDomain R
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : Module.Finite R M
inst✝ : Free R M
φ : End R M
h : IsNilpotent φ
⊢ IsNilpotent ((LinearMap.toMatrix (chooseBasis R M) (chooseBasis R M)) φ)

Proof state:
case h
R : Type u_1
M : Type u_3
inst✝⁵ : CommRing R
inst✝⁴ : IsDomain R
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : Module.Finite R M
inst✝ : Free R M
φ : End R M
h : IsNilpotent φ
⊢ IsNilpotent (LinearMap.charpoly φ - X ^ finrank R M)

Tactic:
rw [finrank_eq_card_chooseBasisIndex]

Result:
case h
R : Type u_1
M : Type u_3
inst✝⁵ : CommRing R
inst✝⁴ : IsDomain R
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : Module.Finite R M
inst✝ : Free R M
φ : End R M
h : IsNilpotent φ
⊢ IsNilpotent (LinearMap.charpoly φ - X ^ Fintype.card (ChooseBasisIndex R M))

Proof state:
case h.hM
R : Type u_1
M : Type u_3
inst✝⁵ : CommRing R
inst✝⁴ : IsDomain R
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : Module.Finite R M
inst✝ : Free R M
φ : End R M
h : IsNilpotent φ
⊢ IsNilpotent ((LinearMap.toMatrix (chooseBasis R M) (chooseBasis R M)) φ)

Tactic:
exact h.map (LinearMap.toMatrixAlgEquiv (chooseBasis R M))

Result:
no goals

Proof state:
R : Type u_1
M : Type u_3
inst✝⁵ : CommRing R
inst✝⁴ : IsDomain R
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : Module.Finite R M
inst✝ : Free R M
φ : End R M
h : IsNilpotent φ
⊢ LinearMap.charpoly φ - X ^ finrank R M = 0

Tactic:
apply IsNilpotent.eq_zero

Result:
case h
R : Type u_1
M : Type u_3
inst✝⁵ : CommRing R
inst✝⁴ : IsDomain R
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : Module.Finite R M
inst✝ : Free R M
φ : End R M
h : IsNilpotent φ
⊢ IsNilpotent (LinearMap.charpoly φ - X ^ finrank R M)

Proof state:
R : Type u_1
M : Type u_3
inst✝⁵ : CommRing R
inst✝⁴ : IsDomain R
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : Module.Finite R M
inst✝ : Free R M
φ : End R M
h : IsNilpotent φ
⊢ LinearMap.charpoly φ = X ^ finrank R M

Tactic:
rw [← sub_eq_zero]

Result:
R : Type u_1
M : Type u_3
inst✝⁵ : CommRing R
inst✝⁴ : IsDomain R
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : Module.Finite R M
inst✝ : Free R M
φ : End R M
h : IsNilpotent φ
⊢ LinearMap.charpoly φ - X ^ finrank R M = 0
-- Mathlib/NumberTheory/Cyclotomic/Discriminant.lean
theorem discr_zeta_eq_discr_zeta_sub_one (hζ : IsPrimitiveRoot ζ n) :
    discr ℚ (hζ.powerBasis ℚ).basis = discr ℚ (hζ.subOnePowerBasis ℚ).basis

Proof state:
n : ℕ+
K : Type u
inst✝¹ : Field K
inst✝ : CharZero K
ζ : K
ce : IsCyclotomicExtension {n} ℚ K
hζ : IsPrimitiveRoot ζ ↑n
this : NumberField K
⊢ (aeval (IsPrimitiveRoot.powerBasis ℚ hζ).gen) (X - 1) = (subOnePowerBasis ℚ hζ).gen

Tactic:
simp

Result:
no goals

Proof state:
n : ℕ+
K : Type u
inst✝¹ : Field K
inst✝ : CharZero K
ζ : K
ce : IsCyclotomicExtension {n} ℚ K
hζ : IsPrimitiveRoot ζ ↑n
this : NumberField K
H₁ : (aeval (IsPrimitiveRoot.powerBasis ℚ hζ).gen) (X - 1) = (subOnePowerBasis ℚ hζ).gen
⊢ discr ℚ ⇑(IsPrimitiveRoot.powerBasis ℚ hζ).basis = discr ℚ ⇑(subOnePowerBasis ℚ hζ).basis

Tactic:
have H₂ : (aeval (hζ.subOnePowerBasis ℚ).gen) (X + 1 : ℤ[X]) = (hζ.powerBasis ℚ).gen := by simp

Result:
n : ℕ+
K : Type u
inst✝¹ : Field K
inst✝ : CharZero K
ζ : K
ce : IsCyclotomicExtension {n} ℚ K
hζ : IsPrimitiveRoot ζ ↑n
this : NumberField K
H₁ : (aeval (IsPrimitiveRoot.powerBasis ℚ hζ).gen) (X - 1) = (subOnePowerBasis ℚ hζ).gen
H₂ : (aeval (subOnePowerBasis ℚ hζ).gen) (X + 1) = (IsPrimitiveRoot.powerBasis ℚ hζ).gen
⊢ discr ℚ ⇑(IsPrimitiveRoot.powerBasis ℚ hζ).basis = discr ℚ ⇑(subOnePowerBasis ℚ hζ).basis
-- Mathlib/Topology/VectorBundle/Basic.lean
theorem coe_linearMapAt_of_mem (e : Pretrivialization F (π F E)) [e.IsLinear R] {b : B}
    (hb : b ∈ e.baseSet) : ⇑(e.linearMapAt R b) = fun y => (e ⟨b, y⟩).2

Proof state:
R : Type u_1
B : Type u_2
F : Type u_3
E : B → Type u_4
inst✝⁷ : Semiring R
inst✝⁶ : TopologicalSpace F
inst✝⁵ : TopologicalSpace B
inst✝⁴ : AddCommMonoid F
inst✝³ : Module R F
inst✝² : (x : B) → AddCommMonoid (E x)
inst✝¹ : (x : B) → Module R (E x)
e : Pretrivialization F TotalSpace.proj
inst✝ : Pretrivialization.IsLinear R e
b : B
hb : b ∈ e.baseSet
⊢ ⇑(Pretrivialization.linearMapAt R e b) = fun y => (↑e { proj := b, snd := y }).2

Tactic:
simp_rw [coe_linearMapAt, if_pos hb]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/BitVec/Lemmas.lean
theorem toInt_not {x : BitVec w} :
    (~~~x).toInt = Int.bmod (2^w - 1 - x.toNat) (2^w)

Proof state:
w : Nat
x : BitVec w
⊢ 2 ^ w - 1 - x.toNat < 2 ^ w

Tactic:
omega

Result:
no goals

Proof state:
w : Nat
x : BitVec w
⊢ (if 2 * (2 ^ w - 1 - x.toNat) < 2 ^ w then ↑(2 ^ w - 1 - x.toNat) else ↑(2 ^ w - 1 - x.toNat) - ↑(2 ^ w)) =
    if ↑(2 ^ w - 1 - x.toNat) % ↑(2 ^ w) < (↑(2 ^ w) + 1) / 2 then ↑(2 ^ w - 1 - x.toNat) % ↑(2 ^ w)
    else ↑(2 ^ w - 1 - x.toNat) % ↑(2 ^ w) - ↑(2 ^ w)

Tactic:
rw_mod_cast [Nat.mod_eq_of_lt (by omega)]

Result:
w : Nat
x : BitVec w
⊢ (if 2 * (2 ^ w - 1 - x.toNat) < 2 ^ w then ↑(2 ^ w - 1 - x.toNat) else ↑(2 ^ w - 1 - x.toNat) - ↑(2 ^ w)) =
    if 2 ^ w - 1 - x.toNat < (2 ^ w + 1) / 2 then ↑(2 ^ w - 1 - x.toNat) else ↑(2 ^ w - 1 - x.toNat) - ↑(2 ^ w)

Proof state:
w : Nat
x : BitVec w
⊢ (if 2 * (2 ^ w - 1 - x.toNat) < 2 ^ w then ↑(2 ^ w - 1 - x.toNat) else ↑(2 ^ w - 1 - x.toNat) - ↑(2 ^ w)) =
    if (↑(2 ^ w) - 1 - ↑x.toNat) % ↑(2 ^ w) < (↑(2 ^ w) + 1) / 2 then (↑(2 ^ w) - 1 - ↑x.toNat) % ↑(2 ^ w)
    else (↑(2 ^ w) - 1 - ↑x.toNat) % ↑(2 ^ w) - ↑(2 ^ w)

Tactic:
simp [show ((2^w : Nat) : Int) - 1 - x.toNat = ((2^w - 1 - x.toNat) : Nat) by omega]

Result:
w : Nat
x : BitVec w
⊢ (if 2 * (2 ^ w - 1 - x.toNat) < 2 ^ w then ↑(2 ^ w - 1 - x.toNat) else ↑(2 ^ w - 1 - x.toNat) - ↑(2 ^ w)) =
    if ↑(2 ^ w - 1 - x.toNat) % ↑(2 ^ w) < (↑(2 ^ w) + 1) / 2 then ↑(2 ^ w - 1 - x.toNat) % ↑(2 ^ w)
    else ↑(2 ^ w - 1 - x.toNat) % ↑(2 ^ w) - ↑(2 ^ w)

Proof state:
w : Nat
x : BitVec w
⊢ ↑(2 ^ w) - 1 - ↑x.toNat = ↑(2 ^ w - 1 - x.toNat)

Tactic:
omega

Result:
no goals

Proof state:
w : Nat
x : BitVec w
⊢ (if 2 * (2 ^ w - 1 - x.toNat) < 2 ^ w then ↑(2 ^ w - 1 - x.toNat) else ↑(2 ^ w - 1 - x.toNat) - ↑(2 ^ w)) =
    if 2 ^ w - 1 - x.toNat < (2 ^ w + 1) / 2 then ↑(2 ^ w - 1 - x.toNat) else ↑(2 ^ w - 1 - x.toNat) - ↑(2 ^ w)

Tactic:
omega

Result:
no goals

Proof state:
w : Nat
x : BitVec w
⊢ (~~~x).toInt = (2 ^ w - 1 - ↑x.toNat).bmod (2 ^ w)

Tactic:
rw_mod_cast [BitVec.toInt, BitVec.toNat_not, Int.bmod_def]

Result:
w : Nat
x : BitVec w
⊢ (if 2 * (2 ^ w - 1 - x.toNat) < 2 ^ w then ↑(2 ^ w - 1 - x.toNat) else ↑(2 ^ w - 1 - x.toNat) - ↑(2 ^ w)) =
    if (↑(2 ^ w) - 1 - ↑x.toNat) % ↑(2 ^ w) < (↑(2 ^ w) + 1) / 2 then (↑(2 ^ w) - 1 - ↑x.toNat) % ↑(2 ^ w)
    else (↑(2 ^ w) - 1 - ↑x.toNat) % ↑(2 ^ w) - ↑(2 ^ w)
-- Mathlib/AlgebraicGeometry/Pullbacks.lean
/--
The composition of the isomorphism `pullbackSepcIso R S T` (from the pullback of
`Spec S ⟶ Spec R` and `Spec T ⟶ Spec R` to `Spec (S ⊗[R] T)`) with the morphism
`Spec (S ⊗[R] T) ⟶ Spec S` obtained by applying `Spec.map` to the ring morphism `s ↦ s ⊗ₜ[R] 1`
is the first projection.
-/
@[reassoc (attr := simp)]
lemma pullbackSpecIso_hom_fst :
    (pullbackSpecIso R S T).hom ≫ Spec.map (ofHom includeLeftRingHom) = pullback.fst _ _

Proof state:
R S T : Type u
inst✝⁴ : CommRing R
inst✝³ : CommRing S
inst✝² : CommRing T
inst✝¹ : Algebra R S
inst✝ : Algebra R T
⊢ (pullbackSpecIso R S T).hom ≫ Spec.map (ofHom includeLeftRingHom) =
    pullback.fst (Spec.map (ofHom (algebraMap R S))) (Spec.map (ofHom (algebraMap R T)))

Tactic:
rw [← pullbackSpecIso_inv_fst, Iso.hom_inv_id_assoc]

Result:
no goals
-- Mathlib/AlgebraicGeometry/Gluing.lean
theorem hom_ext {Y : Scheme} (f₁ f₂ : X ⟶ Y) (h : ∀ x, 𝒰.map x ≫ f₁ = 𝒰.map x ≫ f₂) : f₁ = f₂

Proof state:
case h
X : Scheme
𝒰 : X.OpenCover
Y : Scheme
f₁ f₂ : X ⟶ Y
h : ∀ (x : 𝒰.J), 𝒰.map x ≫ f₁ = 𝒰.map x ≫ f₂
⊢ ∀ (b : (MultispanShape.prod (gluedCover 𝒰).J).R),
    Multicoequalizer.π (gluedCover 𝒰).diagram b ≫ fromGlued 𝒰 ≫ f₁ =
      Multicoequalizer.π (gluedCover 𝒰).diagram b ≫ fromGlued 𝒰 ≫ f₂

Tactic:
intro x

Result:
case h
X : Scheme
𝒰 : X.OpenCover
Y : Scheme
f₁ f₂ : X ⟶ Y
h : ∀ (x : 𝒰.J), 𝒰.map x ≫ f₁ = 𝒰.map x ≫ f₂
x : (MultispanShape.prod (gluedCover 𝒰).J).R
⊢ Multicoequalizer.π (gluedCover 𝒰).diagram x ≫ fromGlued 𝒰 ≫ f₁ =
    Multicoequalizer.π (gluedCover 𝒰).diagram x ≫ fromGlued 𝒰 ≫ f₂

Proof state:
X : Scheme
𝒰 : X.OpenCover
Y : Scheme
f₁ f₂ : X ⟶ Y
h : ∀ (x : 𝒰.J), 𝒰.map x ≫ f₁ = 𝒰.map x ≫ f₂
⊢ fromGlued 𝒰 ≫ f₁ = fromGlued 𝒰 ≫ f₂

Tactic:
apply Multicoequalizer.hom_ext

Result:
case h
X : Scheme
𝒰 : X.OpenCover
Y : Scheme
f₁ f₂ : X ⟶ Y
h : ∀ (x : 𝒰.J), 𝒰.map x ≫ f₁ = 𝒰.map x ≫ f₂
⊢ ∀ (b : (MultispanShape.prod (gluedCover 𝒰).J).R),
    Multicoequalizer.π (gluedCover 𝒰).diagram b ≫ fromGlued 𝒰 ≫ f₁ =
      Multicoequalizer.π (gluedCover 𝒰).diagram b ≫ fromGlued 𝒰 ≫ f₂

Proof state:
X : Scheme
𝒰 : X.OpenCover
Y : Scheme
f₁ f₂ : X ⟶ Y
h : ∀ (x : 𝒰.J), 𝒰.map x ≫ f₁ = 𝒰.map x ≫ f₂
⊢ f₁ = f₂

Tactic:
rw [← cancel_epi 𝒰.fromGlued]

Result:
X : Scheme
𝒰 : X.OpenCover
Y : Scheme
f₁ f₂ : X ⟶ Y
h : ∀ (x : 𝒰.J), 𝒰.map x ≫ f₁ = 𝒰.map x ≫ f₂
⊢ fromGlued 𝒰 ≫ f₁ = fromGlued 𝒰 ≫ f₂

Proof state:
case h
X : Scheme
𝒰 : X.OpenCover
Y : Scheme
f₁ f₂ : X ⟶ Y
h : ∀ (x : 𝒰.J), 𝒰.map x ≫ f₁ = 𝒰.map x ≫ f₂
x : (MultispanShape.prod (gluedCover 𝒰).J).R
⊢ 𝒰.map x ≫ f₁ = 𝒰.map x ≫ f₂

Tactic:
exact h x

Result:
no goals

Proof state:
case h
X : Scheme
𝒰 : X.OpenCover
Y : Scheme
f₁ f₂ : X ⟶ Y
h : ∀ (x : 𝒰.J), 𝒰.map x ≫ f₁ = 𝒰.map x ≫ f₂
x : (MultispanShape.prod (gluedCover 𝒰).J).R
⊢ Multicoequalizer.π (gluedCover 𝒰).diagram x ≫ fromGlued 𝒰 ≫ f₁ =
    Multicoequalizer.π (gluedCover 𝒰).diagram x ≫ fromGlued 𝒰 ≫ f₂

Tactic:
rw [fromGlued, Multicoequalizer.π_desc_assoc, Multicoequalizer.π_desc_assoc]

Result:
case h
X : Scheme
𝒰 : X.OpenCover
Y : Scheme
f₁ f₂ : X ⟶ Y
h : ∀ (x : 𝒰.J), 𝒰.map x ≫ f₁ = 𝒰.map x ≫ f₂
x : (MultispanShape.prod (gluedCover 𝒰).J).R
⊢ 𝒰.map x ≫ f₁ = 𝒰.map x ≫ f₂
-- Mathlib/MeasureTheory/Integral/DominatedConvergence.lean
theorem tendsto_integral_filter_of_norm_le_const {ι} {l : Filter ι} [l.IsCountablyGenerated]
    {F : ι → α → G} [IsFiniteMeasure μ] {f : α → G}
    (h_meas : ∀ᶠ n in l, AEStronglyMeasurable (F n) μ)
    (h_bound : ∃ C, ∀ᶠ n in l, (∀ᵐ ω ∂μ, ‖F n ω‖ ≤ C))
    (h_lim : ∀ᵐ ω ∂μ, Tendsto (fun n => F n ω) l (𝓝 (f ω))) :
    Tendsto (fun n => ∫ ω, F n ω ∂μ) l (nhds (∫ ω, f ω ∂μ))

Proof state:
α : Type u_1
G : Type u_3
inst✝³ : NormedAddCommGroup G
inst✝² : NormedSpace ℝ G
m : MeasurableSpace α
μ : Measure α
ι : Type u_4
l : Filter ι
inst✝¹ : l.IsCountablyGenerated
F : ι → α → G
inst✝ : IsFiniteMeasure μ
f : α → G
h_meas : ∀ᶠ (n : ι) in l, AEStronglyMeasurable (F n) μ
h_bound : ∃ C, ∀ᶠ (n : ι) in l, ∀ᵐ (ω : α) ∂μ, ‖F n ω‖ ≤ C
h_lim : ∀ᵐ (ω : α) ∂μ, Tendsto (fun n => F n ω) l (𝓝 (f ω))
⊢ Tendsto (fun n => ∫ (ω : α), F n ω ∂μ) l (𝓝 (∫ (ω : α), f ω ∂μ))

Tactic:
obtain ⟨c, h_boundc⟩ := h_bound

Result:
case intro
α : Type u_1
G : Type u_3
inst✝³ : NormedAddCommGroup G
inst✝² : NormedSpace ℝ G
m : MeasurableSpace α
μ : Measure α
ι : Type u_4
l : Filter ι
inst✝¹ : l.IsCountablyGenerated
F : ι → α → G
inst✝ : IsFiniteMeasure μ
f : α → G
h_meas : ∀ᶠ (n : ι) in l, AEStronglyMeasurable (F n) μ
h_lim : ∀ᵐ (ω : α) ∂μ, Tendsto (fun n => F n ω) l (𝓝 (f ω))
c : ℝ
h_boundc : ∀ᶠ (n : ι) in l, ∀ᵐ (ω : α) ∂μ, ‖F n ω‖ ≤ c
⊢ Tendsto (fun n => ∫ (ω : α), F n ω ∂μ) l (𝓝 (∫ (ω : α), f ω ∂μ))

Proof state:
case intro
α : Type u_1
G : Type u_3
inst✝³ : NormedAddCommGroup G
inst✝² : NormedSpace ℝ G
m : MeasurableSpace α
μ : Measure α
ι : Type u_4
l : Filter ι
inst✝¹ : l.IsCountablyGenerated
F : ι → α → G
inst✝ : IsFiniteMeasure μ
f : α → G
h_meas : ∀ᶠ (n : ι) in l, AEStronglyMeasurable (F n) μ
h_lim : ∀ᵐ (ω : α) ∂μ, Tendsto (fun n => F n ω) l (𝓝 (f ω))
c : ℝ
h_boundc : ∀ᶠ (n : ι) in l, ∀ᵐ (ω : α) ∂μ, ‖F n ω‖ ≤ c
⊢ Tendsto (fun n => ∫ (ω : α), F n ω ∂μ) l (𝓝 (∫ (ω : α), f ω ∂μ))

Tactic:
let C : α → ℝ := (fun _ => c)

Result:
case intro
α : Type u_1
G : Type u_3
inst✝³ : NormedAddCommGroup G
inst✝² : NormedSpace ℝ G
m : MeasurableSpace α
μ : Measure α
ι : Type u_4
l : Filter ι
inst✝¹ : l.IsCountablyGenerated
F : ι → α → G
inst✝ : IsFiniteMeasure μ
f : α → G
h_meas : ∀ᶠ (n : ι) in l, AEStronglyMeasurable (F n) μ
h_lim : ∀ᵐ (ω : α) ∂μ, Tendsto (fun n => F n ω) l (𝓝 (f ω))
c : ℝ
h_boundc : ∀ᶠ (n : ι) in l, ∀ᵐ (ω : α) ∂μ, ‖F n ω‖ ≤ c
C : α → ℝ := fun x => c
⊢ Tendsto (fun n => ∫ (ω : α), F n ω ∂μ) l (𝓝 (∫ (ω : α), f ω ∂μ))

Proof state:
case intro
α : Type u_1
G : Type u_3
inst✝³ : NormedAddCommGroup G
inst✝² : NormedSpace ℝ G
m : MeasurableSpace α
μ : Measure α
ι : Type u_4
l : Filter ι
inst✝¹ : l.IsCountablyGenerated
F : ι → α → G
inst✝ : IsFiniteMeasure μ
f : α → G
h_meas : ∀ᶠ (n : ι) in l, AEStronglyMeasurable (F n) μ
h_lim : ∀ᵐ (ω : α) ∂μ, Tendsto (fun n => F n ω) l (𝓝 (f ω))
c : ℝ
h_boundc : ∀ᶠ (n : ι) in l, ∀ᵐ (ω : α) ∂μ, ‖F n ω‖ ≤ c
C : α → ℝ := fun x => c
⊢ Tendsto (fun n => ∫ (ω : α), F n ω ∂μ) l (𝓝 (∫ (ω : α), f ω ∂μ))

Tactic:
exact tendsto_integral_filter_of_dominated_convergence
  C h_meas h_boundc (integrable_const c) h_lim

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Int/DivModLemmas.lean
theorem dvd_add_right {a b c : Int} (H : a ∣ b) : a ∣ b + c ↔ a ∣ c

Proof state:
a b c : Int
H : a ∣ b
⊢ a ∣ b + c ↔ a ∣ c

Tactic:
rw [Int.add_comm, Int.dvd_add_left H]

Result:
no goals
-- Mathlib/Geometry/Euclidean/Angle/Unoriented/Affine.lean
theorem _root_.Sbtw.angle₁₂₃_eq_pi {p₁ p₂ p₃ : P} (h : Sbtw ℝ p₁ p₂ p₃) : ∠ p₁ p₂ p₃ = π

Proof state:
case intro.intro.intro.intro.intro
V : Type u_1
P : Type u_2
inst✝³ : NormedAddCommGroup V
inst✝² : InnerProductSpace ℝ V
inst✝¹ : MetricSpace P
inst✝ : NormedAddTorsor V P
p₁ p₂ p₃ : P
r : ℝ
hp₂ : (AffineMap.lineMap p₁ p₃) r = p₂
hp₂p₁ : p₂ ≠ p₁
hp₂p₃ : p₂ ≠ p₃
hr0' : r ≠ 0
hr1' : r ≠ 1
hr0 : 0 < r
hr1 : r < 1
⊢ -(1 - r) / r < 0 ∧ p₃ -ᵥ p₂ = (-(1 - r) / r) • (p₁ -ᵥ p₂)

Tactic:
refine ⟨div_neg_of_neg_of_pos (Left.neg_neg_iff.2 (sub_pos.2 hr1)) hr0, ?_⟩

Result:
case intro.intro.intro.intro.intro
V : Type u_1
P : Type u_2
inst✝³ : NormedAddCommGroup V
inst✝² : InnerProductSpace ℝ V
inst✝¹ : MetricSpace P
inst✝ : NormedAddTorsor V P
p₁ p₂ p₃ : P
r : ℝ
hp₂ : (AffineMap.lineMap p₁ p₃) r = p₂
hp₂p₁ : p₂ ≠ p₁
hp₂p₃ : p₂ ≠ p₃
hr0' : r ≠ 0
hr1' : r ≠ 1
hr0 : 0 < r
hr1 : r < 1
⊢ p₃ -ᵥ p₂ = (-(1 - r) / r) • (p₁ -ᵥ p₂)

Proof state:
V : Type u_1
P : Type u_2
inst✝³ : NormedAddCommGroup V
inst✝² : InnerProductSpace ℝ V
inst✝¹ : MetricSpace P
inst✝ : NormedAddTorsor V P
p₁ p₂ p₃ : P
r : ℝ
hp₂ : (AffineMap.lineMap p₁ p₃) r = p₂
hr0 : 0 ≤ r
hr1 : r ≤ 1
hp₂p₁ : p₂ ≠ p₁
hp₂p₃ : p₂ ≠ p₃
hr0' : r ≠ 0
⊢ r ≠ 1

Tactic:
rintro rfl

Result:
V : Type u_1
P : Type u_2
inst✝³ : NormedAddCommGroup V
inst✝² : InnerProductSpace ℝ V
inst✝¹ : MetricSpace P
inst✝ : NormedAddTorsor V P
p₁ p₂ p₃ : P
hp₂p₁ : p₂ ≠ p₁
hp₂p₃ : p₂ ≠ p₃
hp₂ : (AffineMap.lineMap p₁ p₃) 1 = p₂
hr0 : 0 ≤ 1
hr1 : 1 ≤ 1
hr0' : 1 ≠ 0
⊢ False

Proof state:
V : Type u_1
P : Type u_2
inst✝³ : NormedAddCommGroup V
inst✝² : InnerProductSpace ℝ V
inst✝¹ : MetricSpace P
inst✝ : NormedAddTorsor V P
p₁ p₂ p₃ : P
h : Sbtw ℝ p₁ p₂ p₃
⊢ ∠ p₁ p₂ p₃ = π

Tactic:
rw [angle, angle_eq_pi_iff]

Result:
V : Type u_1
P : Type u_2
inst✝³ : NormedAddCommGroup V
inst✝² : InnerProductSpace ℝ V
inst✝¹ : MetricSpace P
inst✝ : NormedAddTorsor V P
p₁ p₂ p₃ : P
h : Sbtw ℝ p₁ p₂ p₃
⊢ p₁ -ᵥ p₂ ≠ 0 ∧ ∃ r < 0, p₃ -ᵥ p₂ = r • (p₁ -ᵥ p₂)

Proof state:
V : Type u_1
P : Type u_2
inst✝³ : NormedAddCommGroup V
inst✝² : InnerProductSpace ℝ V
inst✝¹ : MetricSpace P
inst✝ : NormedAddTorsor V P
p₁ p₂ p₃ : P
hp₂p₁ : p₂ ≠ p₁
hp₂p₃ : (AffineMap.lineMap p₁ p₃) 1 ≠ p₃
hp₂ : (AffineMap.lineMap p₁ p₃) 1 = p₂
hr0 : 0 ≤ 1
hr1 : 1 ≤ 1
hr0' : 1 ≠ 0
⊢ False

Tactic:
simp at hp₂p₃

Result:
no goals