harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/FieldTheory/PurelyInseparable/Basic.lean
theorem IntermediateField.eq_bot_of_isPurelyInseparable_of_isSeparable
    {F : Type u} {E : Type v} [Field F] [Field E] [Algebra F E] (L : IntermediateField F E)
    [IsPurelyInseparable F L] [Algebra.IsSeparable F L] : L = ⊥ := bot_unique fun x hx ↦ by
  obtain ⟨y, hy⟩ := IsPurelyInseparable.surjective_algebraMap_of_isSeparable F L ⟨x, hx⟩
  exact ⟨y, congr_arg (algebraMap L E) hy⟩

Proof state:
F : Type u
E : Type v
inst✝⁴ : Field F
inst✝³ : Field E
inst✝² : Algebra F E
L : IntermediateField F E
inst✝¹ : IsPurelyInseparable F ↥L
inst✝ : Algebra.IsSeparable F ↥L
x : E
hx : x ∈ L
⊢ x ∈ ⊥

Tactic:
obtain ⟨y, hy⟩ := IsPurelyInseparable.surjective_algebraMap_of_isSeparable F L ⟨x, hx⟩

Result:
case intro
F : Type u
E : Type v
inst✝⁴ : Field F
inst✝³ : Field E
inst✝² : Algebra F E
L : IntermediateField F E
inst✝¹ : IsPurelyInseparable F ↥L
inst✝ : Algebra.IsSeparable F ↥L
x : E
hx : x ∈ L
y : F
hy : (algebraMap F ↥L) y = ⟨x, hx⟩
⊢ x ∈ ⊥

Proof state:
case intro
F : Type u
E : Type v
inst✝⁴ : Field F
inst✝³ : Field E
inst✝² : Algebra F E
L : IntermediateField F E
inst✝¹ : IsPurelyInseparable F ↥L
inst✝ : Algebra.IsSeparable F ↥L
x : E
hx : x ∈ L
y : F
hy : (algebraMap F ↥L) y = ⟨x, hx⟩
⊢ x ∈ ⊥

Tactic:
exact ⟨y, congr_arg (algebraMap L E) hy⟩

Result:
no goals
-- Mathlib/Tactic/NormNum/DivMod.lean
lemma isInt_ediv_zero : ∀ {a b r : ℤ}, IsInt a r → IsNat b (nat_lit 0) → IsNat (a / b) (nat_lit 0)
  | _, _, _, ⟨rfl⟩, ⟨rfl⟩ => ⟨by simp [Int.ediv_zero]⟩

Proof state:
n✝ : ℤ
⊢ ↑n✝ / ↑0 = ↑0

Tactic:
simp [Int.ediv_zero]

Result:
no goals
-- Mathlib/Combinatorics/Additive/DoublingConst.lean
@[to_additive (attr := simp)]
lemma divConst_empty_left (B : Finset G) : δₘ[∅, B] = 0

Proof state:
G : Type u_1
inst✝¹ : Group G
inst✝ : DecidableEq G
B : Finset G
⊢ δₘ[∅, B] = 0

Tactic:
simp [divConst]

Result:
no goals
-- Mathlib/Algebra/BigOperators/Finprod.lean
@[to_additive]
lemma finprod_mem_mulSupport (f : α → M) : ∏ᶠ a ∈ mulSupport f, f a = ∏ᶠ a, f a

Proof state:
α : Type u_1
M : Type u_5
inst✝ : CommMonoid M
f : α → M
⊢ ∏ᶠ (a : α) (_ : a ∈ mulSupport f), f a = ∏ᶠ (a : α), f a

Tactic:
rw [finprod_mem_def, mulIndicator_mulSupport]

Result:
no goals
-- Mathlib/CategoryTheory/Limits/Shapes/Equalizers.lean
theorem Fork.π_comp_hom {s t : Cofork f g} (f : s ⟶ t) : s.π ≫ f.hom = t.π

Proof state:
case mk.mk
C : Type u
inst✝ : Category.{v, u} C
X Y : C
f✝ g : X ⟶ Y
pt✝¹ : C
ι✝¹ : parallelPair f✝ g ⟶ (Functor.const WalkingParallelPair).obj pt✝¹
pt✝ : C
ι✝ : parallelPair f✝ g ⟶ (Functor.const WalkingParallelPair).obj pt✝
f : { pt := pt✝¹, ι := ι✝¹ } ⟶ { pt := pt✝, ι := ι✝ }
⊢ Cofork.π { pt := pt✝¹, ι := ι✝¹ } ≫ f.hom = Cofork.π { pt := pt✝, ι := ι✝ }

Tactic:
cases f

Result:
case mk.mk.mk
C : Type u
inst✝ : Category.{v, u} C
X Y : C
f g : X ⟶ Y
pt✝¹ : C
ι✝¹ : parallelPair f g ⟶ (Functor.const WalkingParallelPair).obj pt✝¹
pt✝ : C
ι✝ : parallelPair f g ⟶ (Functor.const WalkingParallelPair).obj pt✝
hom✝ : { pt := pt✝¹, ι := ι✝¹ }.pt ⟶ { pt := pt✝, ι := ι✝ }.pt
w✝ : ∀ (j : WalkingParallelPair), { pt := pt✝¹, ι := ι✝¹ }.ι.app j ≫ hom✝ = { pt := pt✝, ι := ι✝ }.ι.app j
⊢ Cofork.π { pt := pt✝¹, ι := ι✝¹ } ≫ { hom := hom✝, w := w✝ }.hom = Cofork.π { pt := pt✝, ι := ι✝ }

Proof state:
case mk.mk.mk
C : Type u
inst✝ : Category.{v, u} C
X Y : C
f g : X ⟶ Y
pt✝¹ : C
ι✝¹ : parallelPair f g ⟶ (Functor.const WalkingParallelPair).obj pt✝¹
pt✝ : C
ι✝ : parallelPair f g ⟶ (Functor.const WalkingParallelPair).obj pt✝
hom✝ : { pt := pt✝¹, ι := ι✝¹ }.pt ⟶ { pt := pt✝, ι := ι✝ }.pt
w✝ : ∀ (j : WalkingParallelPair), { pt := pt✝¹, ι := ι✝¹ }.ι.app j ≫ hom✝ = { pt := pt✝, ι := ι✝ }.ι.app j
⊢ Cofork.π { pt := pt✝¹, ι := ι✝¹ } ≫ { hom := hom✝, w := w✝ }.hom = Cofork.π { pt := pt✝, ι := ι✝ }

Tactic:
aesop

Result:
no goals

Proof state:
C : Type u
inst✝ : Category.{v, u} C
X Y : C
f✝ g : X ⟶ Y
s t : Cofork f✝ g
f : s ⟶ t
⊢ s.π ≫ f.hom = t.π

Tactic:
cases s

Result:
case mk
C : Type u
inst✝ : Category.{v, u} C
X Y : C
f✝ g : X ⟶ Y
t : Cofork f✝ g
pt✝ : C
ι✝ : parallelPair f✝ g ⟶ (Functor.const WalkingParallelPair).obj pt✝
f : { pt := pt✝, ι := ι✝ } ⟶ t
⊢ Cofork.π { pt := pt✝, ι := ι✝ } ≫ f.hom = t.π

Proof state:
case mk
C : Type u
inst✝ : Category.{v, u} C
X Y : C
f✝ g : X ⟶ Y
t : Cofork f✝ g
pt✝ : C
ι✝ : parallelPair f✝ g ⟶ (Functor.const WalkingParallelPair).obj pt✝
f : { pt := pt✝, ι := ι✝ } ⟶ t
⊢ Cofork.π { pt := pt✝, ι := ι✝ } ≫ f.hom = t.π

Tactic:
cases t

Result:
case mk.mk
C : Type u
inst✝ : Category.{v, u} C
X Y : C
f✝ g : X ⟶ Y
pt✝¹ : C
ι✝¹ : parallelPair f✝ g ⟶ (Functor.const WalkingParallelPair).obj pt✝¹
pt✝ : C
ι✝ : parallelPair f✝ g ⟶ (Functor.const WalkingParallelPair).obj pt✝
f : { pt := pt✝¹, ι := ι✝¹ } ⟶ { pt := pt✝, ι := ι✝ }
⊢ Cofork.π { pt := pt✝¹, ι := ι✝¹ } ≫ f.hom = Cofork.π { pt := pt✝, ι := ι✝ }
-- Mathlib/Algebra/Lie/Weights/Chain.lean
lemma genWeightSpaceChain_def' :
    genWeightSpaceChain M χ₁ χ₂ p q = ⨆ k ∈ Finset.Ioo p q, genWeightSpace M (k • χ₁ + χ₂)

Proof state:
R : Type u_1
L : Type u_2
inst✝⁷ : CommRing R
inst✝⁶ : LieRing L
inst✝⁵ : LieAlgebra R L
M : Type u_3
inst✝⁴ : AddCommGroup M
inst✝³ : Module R M
inst✝² : LieRingModule L M
inst✝¹ : LieModule R L M
inst✝ : LieRing.IsNilpotent L
χ₁ χ₂ : L → R
p q : ℤ
⊢ genWeightSpaceChain M χ₁ χ₂ p q = ⨆ k ∈ Finset.Ioo p q, genWeightSpace M (k • χ₁ + χ₂)

Tactic:
have : ∀ (k : ℤ), k ∈ Ioo p q ↔ k ∈ Finset.Ioo p q := by simp

Result:
R : Type u_1
L : Type u_2
inst✝⁷ : CommRing R
inst✝⁶ : LieRing L
inst✝⁵ : LieAlgebra R L
M : Type u_3
inst✝⁴ : AddCommGroup M
inst✝³ : Module R M
inst✝² : LieRingModule L M
inst✝¹ : LieModule R L M
inst✝ : LieRing.IsNilpotent L
χ₁ χ₂ : L → R
p q : ℤ
this : ∀ (k : ℤ), k ∈ Ioo p q ↔ k ∈ Finset.Ioo p q
⊢ genWeightSpaceChain M χ₁ χ₂ p q = ⨆ k ∈ Finset.Ioo p q, genWeightSpace M (k • χ₁ + χ₂)

Proof state:
R : Type u_1
L : Type u_2
inst✝⁷ : CommRing R
inst✝⁶ : LieRing L
inst✝⁵ : LieAlgebra R L
M : Type u_3
inst✝⁴ : AddCommGroup M
inst✝³ : Module R M
inst✝² : LieRingModule L M
inst✝¹ : LieModule R L M
inst✝ : LieRing.IsNilpotent L
χ₁ χ₂ : L → R
p q : ℤ
⊢ ∀ (k : ℤ), k ∈ Ioo p q ↔ k ∈ Finset.Ioo p q

Tactic:
simp

Result:
no goals

Proof state:
R : Type u_1
L : Type u_2
inst✝⁷ : CommRing R
inst✝⁶ : LieRing L
inst✝⁵ : LieAlgebra R L
M : Type u_3
inst✝⁴ : AddCommGroup M
inst✝³ : Module R M
inst✝² : LieRingModule L M
inst✝¹ : LieModule R L M
inst✝ : LieRing.IsNilpotent L
χ₁ χ₂ : L → R
p q : ℤ
this : ∀ (k : ℤ), k ∈ Ioo p q ↔ k ∈ Finset.Ioo p q
⊢ genWeightSpaceChain M χ₁ χ₂ p q = ⨆ k ∈ Finset.Ioo p q, genWeightSpace M (k • χ₁ + χ₂)

Tactic:
simp_rw [genWeightSpaceChain_def, this]

Result:
no goals
-- Mathlib/Algebra/Order/Group/Pointwise/Interval.lean
theorem image_mul_left_Ioo {a : α} (h : 0 < a) (b c : α) :
    (a * ·) '' Ioo b c = Ioo (a * b) (a * c)

Proof state:
α : Type u_1
inst✝ : LinearOrderedField α
a : α
h : 0 < a
b c : α
⊢ (fun x => a * x) '' Ioo b c = Ioo (a * b) (a * c)

Tactic:
convert image_mul_right_Ioo b c h using 1 <;> simp only [mul_comm _ a]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Int/DivModLemmas.lean
theorem natAbs_tdiv (a b : Int) : natAbs (a.tdiv b) = (natAbs a).div (natAbs b) :=
  match a, b, eq_nat_or_neg a, eq_nat_or_neg b with
  | _, _, ⟨_, .inl rfl⟩, ⟨_, .inl rfl⟩ => rfl
  | _, _, ⟨_, .inl rfl⟩, ⟨_, .inr rfl⟩ => by rw [Int.tdiv_neg, natAbs_neg, natAbs_neg]; rfl
  | _, _, ⟨_, .inr rfl⟩, ⟨_, .inl rfl⟩ => by rw [Int.neg_tdiv, natAbs_neg, natAbs_neg]; rfl
  | _, _, ⟨_, .inr rfl⟩, ⟨_, .inr rfl⟩ => by rw [Int.neg_tdiv_neg, natAbs_neg, natAbs_neg]; rfl

Proof state:
a b : Int
w✝¹ w✝ : Nat
⊢ ((-↑w✝¹).tdiv (-↑w✝)).natAbs = (-↑w✝¹).natAbs.div (-↑w✝).natAbs

Tactic:
rw [Int.neg_tdiv_neg, natAbs_neg, natAbs_neg]

Result:
a b : Int
w✝¹ w✝ : Nat
⊢ ((↑w✝¹).tdiv ↑w✝).natAbs = (↑w✝¹).natAbs.div (↑w✝).natAbs

Proof state:
a b : Int
w✝¹ w✝ : Nat
⊢ ((↑w✝¹).tdiv (-↑w✝)).natAbs = (↑w✝¹).natAbs.div (-↑w✝).natAbs

Tactic:
rw [Int.tdiv_neg, natAbs_neg, natAbs_neg]

Result:
a b : Int
w✝¹ w✝ : Nat
⊢ ((↑w✝¹).tdiv ↑w✝).natAbs = (↑w✝¹).natAbs.div (↑w✝).natAbs

Proof state:
a b : Int
w✝¹ w✝ : Nat
⊢ ((-↑w✝¹).tdiv ↑w✝).natAbs = (-↑w✝¹).natAbs.div (↑w✝).natAbs

Tactic:
rw [Int.neg_tdiv, natAbs_neg, natAbs_neg]

Result:
a b : Int
w✝¹ w✝ : Nat
⊢ ((↑w✝¹).tdiv ↑w✝).natAbs = (↑w✝¹).natAbs.div (↑w✝).natAbs

Proof state:
a b : Int
w✝¹ w✝ : Nat
⊢ ((↑w✝¹).tdiv ↑w✝).natAbs = (↑w✝¹).natAbs.div (↑w✝).natAbs

Tactic:
rfl

Result:
no goals
-- Mathlib/RingTheory/Polynomial/Vieta.lean
theorem prod_X_add_C_coeff' {σ} (s : Multiset σ) (r : σ → R) {k : ℕ} (h : k ≤ Multiset.card s) :
    (s.map fun i => X + C (r i)).prod.coeff k = (s.map r).esymm (Multiset.card s - k)

Proof state:
case h
R : Type u_1
inst✝ : CommSemiring R
σ : Type u_2
s : Multiset σ
r : σ → R
k : ℕ
h : k ≤ s.card
⊢ k ≤ s.card

Tactic:
assumption

Result:
no goals

Proof state:
R : Type u_1
inst✝ : CommSemiring R
σ : Type u_2
s : Multiset σ
r : σ → R
k : ℕ
h : k ≤ s.card
⊢ (map (fun i => X + C (r i)) s).prod.coeff k = (map r s).esymm (s.card - k)

Tactic:
erw [← map_map (fun r => X + C r) r, prod_X_add_C_coeff] <;> rw [s.card_map r]

Result:
case h
R : Type u_1
inst✝ : CommSemiring R
σ : Type u_2
s : Multiset σ
r : σ → R
k : ℕ
h : k ≤ s.card
⊢ k ≤ s.card
-- Mathlib/NumberTheory/Zsqrtd/Basic.lean
theorem norm_eq_of_associated {d : ℤ} (hd : d ≤ 0) {x y : ℤ√d} (h : Associated x y) :
    x.norm = y.norm

Proof state:
d : ℤ
hd : d ≤ 0
x y : ℤ√d
h : Associated x y
⊢ x.norm = y.norm

Tactic:
obtain ⟨u, rfl⟩ := h

Result:
case intro
d : ℤ
hd : d ≤ 0
x : ℤ√d
u : (ℤ√d)ˣ
⊢ x.norm = (x * ↑u).norm

Proof state:
case intro
d : ℤ
hd : d ≤ 0
x : ℤ√d
u : (ℤ√d)ˣ
⊢ x.norm = (x * ↑u).norm

Tactic:
rw [norm_mul, (norm_eq_one_iff' hd _).mpr u.isUnit, mul_one]

Result:
no goals
-- Mathlib/RingTheory/MvPolynomial/Ideal.lean
theorem mem_ideal_span_monomial_image {x : MvPolynomial σ R} {s : Set (σ →₀ ℕ)} :
    x ∈ Ideal.span ((fun s => monomial s (1 : R)) '' s) ↔ ∀ xi ∈ x.support, ∃ si ∈ s, si ≤ xi

Proof state:
σ : Type u_1
R : Type u_2
inst✝ : CommSemiring R
x : MvPolynomial σ R
s : Set (σ →₀ ℕ)
⊢ (∀ m ∈ x.support, ∃ m' ∈ s, ∃ d, m = d + m') ↔ ∀ xi ∈ x.support, ∃ si ∈ s, si ≤ xi

Tactic:
simp_rw [le_iff_exists_add, add_comm]

Result:
σ : Type u_1
R : Type u_2
inst✝ : CommSemiring R
x : MvPolynomial σ R
s : Set (σ →₀ ℕ)
⊢ (∀ m ∈ x.support, ∃ m' ∈ s, ∃ d, m = m' + d) ↔ ∀ xi ∈ x.support, ∃ si ∈ s, ∃ c, xi = si + c

Proof state:
σ : Type u_1
R : Type u_2
inst✝ : CommSemiring R
x : MvPolynomial σ R
s : Set (σ →₀ ℕ)
⊢ x ∈ Ideal.span ((fun s => (monomial s) 1) '' s) ↔ ∀ xi ∈ x.support, ∃ si ∈ s, si ≤ xi

Tactic:
refine AddMonoidAlgebra.mem_ideal_span_of'_image.trans ?_

Result:
σ : Type u_1
R : Type u_2
inst✝ : CommSemiring R
x : MvPolynomial σ R
s : Set (σ →₀ ℕ)
⊢ (∀ m ∈ x.support, ∃ m' ∈ s, ∃ d, m = d + m') ↔ ∀ xi ∈ x.support, ∃ si ∈ s, si ≤ xi

Proof state:
σ : Type u_1
R : Type u_2
inst✝ : CommSemiring R
x : MvPolynomial σ R
s : Set (σ →₀ ℕ)
⊢ (∀ m ∈ x.support, ∃ m' ∈ s, ∃ d, m = m' + d) ↔ ∀ xi ∈ x.support, ∃ si ∈ s, ∃ c, xi = si + c

Tactic:
rfl

Result:
no goals
-- Mathlib/Analysis/Fourier/FiniteAbelian/PontryaginDuality.lean
private lemma mkZModAux_injective {ι : Type} [DecidableEq ι] {n : ι → ℕ} [∀ i, NeZero (n i)] :
    Injective (mkZModAux n) :=
  AddChar.directSum_injective.comp fun f g h ↦ by simpa [funext_iff] using h

Proof state:
ι : Type
inst✝¹ : DecidableEq ι
n : ι → ℕ
inst✝ : ∀ (i : ι), NeZero (n i)
f g : (i : ι) → ZMod (n i)
h : (fun i => zmod (n i) (f i)) = fun i => zmod (n i) (g i)
⊢ f = g

Tactic:
simpa [funext_iff] using h

Result:
no goals
-- Mathlib/Dynamics/TopologicalEntropy/CoverEntropy.lean
lemma IsDynCoverOf.coverEntropyEntourage_le_log_card_div {T : X → X} {F : Set X}
    (F_inv : MapsTo T F F) {U : Set (X × X)} (U_symm : SymmetricRel U) {n : ℕ} (n_pos : 0 < n)
    {s : Finset X} (h : IsDynCoverOf T F U n s) :
    coverEntropyEntourage T F (U ○ U) ≤ log s.card / n

Proof state:
X : Type u_1
T : X → X
F : Set X
F_inv : MapsTo T F F
U : Set (X × X)
U_symm : SymmetricRel U
n : ℕ
n_pos : 0 < n
s : Finset X
h : IsDynCoverOf T F U n ↑s
⊢ ↑(coverMincard T F U n) ≤ ↑s.card

Tactic:
exact_mod_cast coverMincard_le_card h

Result:
no goals

Proof state:
X : Type u_1
T : X → X
F : Set X
F_inv : MapsTo T F F
U : Set (X × X)
U_symm : SymmetricRel U
n : ℕ
n_pos : 0 < n
s : Finset X
h : IsDynCoverOf T F U n ↑s
⊢ (↑(coverMincard T F U n)).log / ↑n ≤ (↑s.card).log / ↑n

Tactic:
apply monotone_div_right_of_nonneg (Nat.cast_nonneg' n) (log_monotone _)

Result:
X : Type u_1
T : X → X
F : Set X
F_inv : MapsTo T F F
U : Set (X × X)
U_symm : SymmetricRel U
n : ℕ
n_pos : 0 < n
s : Finset X
h : IsDynCoverOf T F U n ↑s
⊢ ↑(coverMincard T F U n) ≤ ↑s.card

Proof state:
X : Type u_1
T : X → X
F : Set X
F_inv : MapsTo T F F
U : Set (X × X)
U_symm : SymmetricRel U
n : ℕ
n_pos : 0 < n
s : Finset X
h : IsDynCoverOf T F U n ↑s
⊢ coverEntropyEntourage T F (U ○ U) ≤ (↑s.card).log / ↑n

Tactic:
apply (coverEntropyEntourage_le_log_coverMincard_div F_inv U_symm n_pos).trans

Result:
X : Type u_1
T : X → X
F : Set X
F_inv : MapsTo T F F
U : Set (X × X)
U_symm : SymmetricRel U
n : ℕ
n_pos : 0 < n
s : Finset X
h : IsDynCoverOf T F U n ↑s
⊢ (↑(coverMincard T F U n)).log / ↑n ≤ (↑s.card).log / ↑n
-- Mathlib/CategoryTheory/Subobject/Comma.lean
theorem unop_left_comp_ofMkLEMk_unop {A : CostructuredArrow S T} {P Q : (CostructuredArrow S T)ᵒᵖ}
    {f : P ⟶ op A} {g : Q ⟶ op A} [Mono f.unop.left.op] [Mono g.unop.left.op]
    (h : Subobject.mk f.unop.left.op ≤ Subobject.mk g.unop.left.op) :
    g.unop.left ≫ (Subobject.ofMkLEMk f.unop.left.op g.unop.left.op h).unop = f.unop.left

Proof state:
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
D : Type u₂
inst✝² : Category.{v₂, u₂} D
S : C ⥤ D
T : D
A : CostructuredArrow S T
P Q : (CostructuredArrow S T)ᵒᵖ
f : P ⟶ op A
g : Q ⟶ op A
inst✝¹ : Mono f.unop.left.op
inst✝ : Mono g.unop.left.op
h : Subobject.mk f.unop.left.op ≤ Subobject.mk g.unop.left.op
⊢ (Subobject.ofMkLEMk f.unop.left.op g.unop.left.op h ≫ g.unop.left.op).unop = f.unop.left

Tactic:
simp only [Subobject.ofMkLEMk_comp, Quiver.Hom.unop_op]

Result:
no goals

Proof state:
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
D : Type u₂
inst✝² : Category.{v₂, u₂} D
S : C ⥤ D
T : D
A : CostructuredArrow S T
P Q : (CostructuredArrow S T)ᵒᵖ
f : P ⟶ op A
g : Q ⟶ op A
inst✝¹ : Mono f.unop.left.op
inst✝ : Mono g.unop.left.op
h : Subobject.mk f.unop.left.op ≤ Subobject.mk g.unop.left.op
⊢ g.unop.left.op.unop ≫ (Subobject.ofMkLEMk f.unop.left.op g.unop.left.op h).unop = f.unop.left

Tactic:
rw [← unop_comp]

Result:
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
D : Type u₂
inst✝² : Category.{v₂, u₂} D
S : C ⥤ D
T : D
A : CostructuredArrow S T
P Q : (CostructuredArrow S T)ᵒᵖ
f : P ⟶ op A
g : Q ⟶ op A
inst✝¹ : Mono f.unop.left.op
inst✝ : Mono g.unop.left.op
h : Subobject.mk f.unop.left.op ≤ Subobject.mk g.unop.left.op
⊢ (Subobject.ofMkLEMk f.unop.left.op g.unop.left.op h ≫ g.unop.left.op).unop = f.unop.left

Proof state:
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
D : Type u₂
inst✝² : Category.{v₂, u₂} D
S : C ⥤ D
T : D
A : CostructuredArrow S T
P Q : (CostructuredArrow S T)ᵒᵖ
f : P ⟶ op A
g : Q ⟶ op A
inst✝¹ : Mono f.unop.left.op
inst✝ : Mono g.unop.left.op
h : Subobject.mk f.unop.left.op ≤ Subobject.mk g.unop.left.op
⊢ g.unop.left ≫ (Subobject.ofMkLEMk f.unop.left.op g.unop.left.op h).unop = f.unop.left

Tactic:
conv_lhs =>
  congr
  rw [← Quiver.Hom.unop_op g.unop.left]

Result:
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
D : Type u₂
inst✝² : Category.{v₂, u₂} D
S : C ⥤ D
T : D
A : CostructuredArrow S T
P Q : (CostructuredArrow S T)ᵒᵖ
f : P ⟶ op A
g : Q ⟶ op A
inst✝¹ : Mono f.unop.left.op
inst✝ : Mono g.unop.left.op
h : Subobject.mk f.unop.left.op ≤ Subobject.mk g.unop.left.op
⊢ g.unop.left.op.unop ≫ (Subobject.ofMkLEMk f.unop.left.op g.unop.left.op h).unop = f.unop.left
-- Mathlib/Order/SuccPred/Basic.lean
theorem succ_le_succ_iff : succ a ≤ succ b ↔ a ≤ b

Proof state:
α : Type u_1
inst✝² : LinearOrder α
inst✝¹ : SuccOrder α
a b : α
inst✝ : NoMaxOrder α
⊢ succ a ≤ succ b ↔ a ≤ b

Tactic:
simp

Result:
no goals
-- Mathlib/SetTheory/Cardinal/Basic.lean
theorem le_powerlt {b c : Cardinal.{u}} (a) (h : c < b) : (a^c) ≤ a ^< b

Proof state:
b c a : Cardinal.{u}
h : c < b
⊢ BddAbove (range fun y => a ^ ↑y)

Tactic:
rw [← image_eq_range]

Result:
b c a : Cardinal.{u}
h : c < b
⊢ BddAbove (HPow.hPow a '' Iio b)

Proof state:
b c a : Cardinal.{u}
h : c < b
⊢ a ^ c ≤ a ^< b

Tactic:
refine le_ciSup (f := fun y : Iio b => a ^ (y : Cardinal)) ?_ ⟨c, h⟩

Result:
b c a : Cardinal.{u}
h : c < b
⊢ BddAbove (range fun y => a ^ ↑y)

Proof state:
b c a : Cardinal.{u}
h : c < b
⊢ BddAbove (HPow.hPow a '' Iio b)

Tactic:
exact bddAbove_image.{u, u} _ bddAbove_Iio

Result:
no goals
-- Mathlib/Combinatorics/SimpleGraph/Basic.lean
theorem fromEdgeSet_sdiff (s t : Set (Sym2 V)) :
    fromEdgeSet (s \ t) = fromEdgeSet s \ fromEdgeSet t

Proof state:
case Adj.h.h.a
V : Type u
s t : Set (Sym2 V)
v w : V
⊢ (fromEdgeSet (s \ t)).Adj v w ↔ (fromEdgeSet s \ fromEdgeSet t).Adj v w

Tactic:
constructor <;> simp +contextual

Result:
no goals

Proof state:
V : Type u
s t : Set (Sym2 V)
⊢ fromEdgeSet (s \ t) = fromEdgeSet s \ fromEdgeSet t

Tactic:
ext v w

Result:
case Adj.h.h.a
V : Type u
s t : Set (Sym2 V)
v w : V
⊢ (fromEdgeSet (s \ t)).Adj v w ↔ (fromEdgeSet s \ fromEdgeSet t).Adj v w
-- Mathlib/Data/Matrix/Notation.lean
theorem cons_vecMul (x : α) (v : Fin n → α) (B : Fin n.succ → o' → α) :
    vecCons x v ᵥ* of B = x • vecHead B + v ᵥ* of (vecTail B)

Proof state:
α : Type u
n : ℕ
o' : Type uₒ
inst✝ : NonUnitalNonAssocSemiring α
x : α
v : Fin n → α
B : Fin n.succ → o' → α
⊢ vecCons x v ᵥ* of B = x • vecHead B + v ᵥ* of (vecTail B)

Tactic:
ext i

Result:
case h
α : Type u
n : ℕ
o' : Type uₒ
inst✝ : NonUnitalNonAssocSemiring α
x : α
v : Fin n → α
B : Fin n.succ → o' → α
i : o'
⊢ (vecCons x v ᵥ* of B) i = (x • vecHead B + v ᵥ* of (vecTail B)) i

Proof state:
case h
α : Type u
n : ℕ
o' : Type uₒ
inst✝ : NonUnitalNonAssocSemiring α
x : α
v : Fin n → α
B : Fin n.succ → o' → α
i : o'
⊢ (vecCons x v ᵥ* of B) i = (x • vecHead B + v ᵥ* of (vecTail B)) i

Tactic:
simp [vecMul]

Result:
no goals
-- Mathlib/Order/RelIso/Basic.lean
theorem toEmbedding_injective : Injective (toEmbedding : r ↪r s → (α ↪ β))

Proof state:
α : Type u_1
β : Type u_2
r : α → α → Prop
s : β → β → Prop
⊢ Injective toEmbedding

Tactic:
rintro ⟨f, -⟩ ⟨g, -⟩

Result:
case mk.mk
α : Type u_1
β : Type u_2
r : α → α → Prop
s : β → β → Prop
f : α ↪ β
map_rel_iff'✝¹ : ∀ {a b : α}, s (f a) (f b) ↔ r a b
g : α ↪ β
map_rel_iff'✝ : ∀ {a b : α}, s (g a) (g b) ↔ r a b
⊢ { toEmbedding := f, map_rel_iff' := map_rel_iff'✝¹ }.toEmbedding =
      { toEmbedding := g, map_rel_iff' := map_rel_iff'✝ }.toEmbedding →
    { toEmbedding := f, map_rel_iff' := map_rel_iff'✝¹ } = { toEmbedding := g, map_rel_iff' := map_rel_iff'✝ }

Proof state:
case mk.mk
α : Type u_1
β : Type u_2
r : α → α → Prop
s : β → β → Prop
f : α ↪ β
map_rel_iff'✝¹ : ∀ {a b : α}, s (f a) (f b) ↔ r a b
g : α ↪ β
map_rel_iff'✝ : ∀ {a b : α}, s (g a) (g b) ↔ r a b
⊢ { toEmbedding := f, map_rel_iff' := map_rel_iff'✝¹ }.toEmbedding =
      { toEmbedding := g, map_rel_iff' := map_rel_iff'✝ }.toEmbedding →
    { toEmbedding := f, map_rel_iff' := map_rel_iff'✝¹ } = { toEmbedding := g, map_rel_iff' := map_rel_iff'✝ }

Tactic:
simp

Result:
no goals
-- Mathlib/FieldTheory/KummerExtension.lean
lemma autEquivZmod_symm_apply_intCast [NeZero n] {ζ : K} (hζ : IsPrimitiveRoot ζ n) (m : ℤ) :
    (autEquivZmod H L hζ).symm (Multiplicative.ofAdd (m : ZMod n)) α = ζ ^ m • α

Proof state:
K : Type u
inst✝⁴ : Field K
n : ℕ
a : K
H : Irreducible (X ^ n - C a)
L : Type u_1
inst✝³ : Field L
inst✝² : Algebra K L
inst✝¹ : IsSplittingField K L (X ^ n - C a)
α : L
hα : α ^ n = (algebraMap K L) a
inst✝ : NeZero n
ζ : K
hζ : IsPrimitiveRoot ζ n
m : ℤ
⊢ ((autEquivZmod H L hζ).symm (Multiplicative.ofAdd ↑m)) α = ζ ^ m • α

Tactic:
have hn := Nat.pos_iff_ne_zero.mpr (ne_zero_of_irreducible_X_pow_sub_C H)

Result:
K : Type u
inst✝⁴ : Field K
n : ℕ
a : K
H : Irreducible (X ^ n - C a)
L : Type u_1
inst✝³ : Field L
inst✝² : Algebra K L
inst✝¹ : IsSplittingField K L (X ^ n - C a)
α : L
hα : α ^ n = (algebraMap K L) a
inst✝ : NeZero n
ζ : K
hζ : IsPrimitiveRoot ζ n
m : ℤ
hn : 0 < n
⊢ ((autEquivZmod H L hζ).symm (Multiplicative.ofAdd ↑m)) α = ζ ^ m • α

Proof state:
K : Type u
inst✝⁴ : Field K
n : ℕ
a : K
H : Irreducible (X ^ n - C a)
L : Type u_1
inst✝³ : Field L
inst✝² : Algebra K L
inst✝¹ : IsSplittingField K L (X ^ n - C a)
α : L
hα : α ^ n = (algebraMap K L) a
inst✝ : NeZero n
ζ : K
hζ : IsPrimitiveRoot ζ n
m : ℤ
hn : 0 < n
⊢ ((autEquivZmod H L hζ).symm (Multiplicative.ofAdd ↑m)) α = ζ ^ m • α

Tactic:
rw [← autEquivRootsOfUnity_smul ⟨ζ, (mem_primitiveRoots hn).mpr hζ⟩ H L hα]

Result:
K : Type u
inst✝⁴ : Field K
n : ℕ
a : K
H : Irreducible (X ^ n - C a)
L : Type u_1
inst✝³ : Field L
inst✝² : Algebra K L
inst✝¹ : IsSplittingField K L (X ^ n - C a)
α : L
hα : α ^ n = (algebraMap K L) a
inst✝ : NeZero n
ζ : K
hζ : IsPrimitiveRoot ζ n
m : ℤ
hn : 0 < n
⊢ (autEquivRootsOfUnity ⋯ H L) ((autEquivZmod H L hζ).symm (Multiplicative.ofAdd ↑m)) • α = ζ ^ m • α

Proof state:
K : Type u
inst✝⁴ : Field K
n : ℕ
a : K
H : Irreducible (X ^ n - C a)
L : Type u_1
inst✝³ : Field L
inst✝² : Algebra K L
inst✝¹ : IsSplittingField K L (X ^ n - C a)
α : L
hα : α ^ n = (algebraMap K L) a
inst✝ : NeZero n
ζ : K
hζ : IsPrimitiveRoot ζ n
m : ℤ
hn : 0 < n
⊢ (autEquivRootsOfUnity ⋯ H L) ((autEquivZmod H L hζ).symm (Multiplicative.ofAdd ↑m)) • α = ζ ^ m • α

Tactic:
simp [MulEquiv.subgroupCongr_symm_apply, Subgroup.smul_def, Units.smul_def, autEquivZmod]

Result:
no goals
-- Mathlib/Algebra/Polynomial/Splits.lean
theorem adjoin_rootSet_eq_range [Algebra R K] [Algebra R L] {p : R[X]}
    (h : p.Splits (algebraMap R K)) (f : K →ₐ[R] L) :
    Algebra.adjoin R (p.rootSet L) = f.range ↔ Algebra.adjoin R (p.rootSet K) = ⊤

Proof state:
R : Type u_1
K : Type v
L : Type w
inst✝⁴ : CommRing R
inst✝³ : Field K
inst✝² : Field L
inst✝¹ : Algebra R K
inst✝ : Algebra R L
p : R[X]
h : Splits (algebraMap R K) p
f : K →ₐ[R] L
⊢ Algebra.adjoin R (p.rootSet L) = f.range ↔ Algebra.adjoin R (p.rootSet K) = ⊤

Tactic:
rw [← image_rootSet h f, Algebra.adjoin_image, ← Algebra.map_top]

Result:
R : Type u_1
K : Type v
L : Type w
inst✝⁴ : CommRing R
inst✝³ : Field K
inst✝² : Field L
inst✝¹ : Algebra R K
inst✝ : Algebra R L
p : R[X]
h : Splits (algebraMap R K) p
f : K →ₐ[R] L
⊢ Subalgebra.map f (Algebra.adjoin R (p.rootSet K)) = Subalgebra.map f ⊤ ↔ Algebra.adjoin R (p.rootSet K) = ⊤

Proof state:
R : Type u_1
K : Type v
L : Type w
inst✝⁴ : CommRing R
inst✝³ : Field K
inst✝² : Field L
inst✝¹ : Algebra R K
inst✝ : Algebra R L
p : R[X]
h : Splits (algebraMap R K) p
f : K →ₐ[R] L
⊢ Subalgebra.map f (Algebra.adjoin R (p.rootSet K)) = Subalgebra.map f ⊤ ↔ Algebra.adjoin R (p.rootSet K) = ⊤

Tactic:
exact (Subalgebra.map_injective f.toRingHom.injective).eq_iff

Result:
no goals