harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/RingTheory/Frobenius.lean
lemma comap_eq [Q.IsPrime] : Q.comap φ = Q

Proof state:
R : Type u_1
S : Type u_2
inst✝³ : CommRing R
inst✝² : CommRing S
inst✝¹ : Algebra R S
φ : S →ₐ[R] S
Q : Ideal S
H : φ.IsArithFrobAt Q
inst✝ : Q.IsPrime
x : S
hx : x ∈ Ideal.comap φ Q
⊢ x ∈ Q

Tactic:
rwa [← Ideal.Quotient.eq_zero_iff_mem, ← H.restrict_injective.eq_iff, map_zero, restrict_mk,
  Ideal.Quotient.eq_zero_iff_mem, ← Ideal.mem_comap]

Result:
no goals

Proof state:
R : Type u_1
S : Type u_2
inst✝³ : CommRing R
inst✝² : CommRing S
inst✝¹ : Algebra R S
φ : S →ₐ[R] S
Q : Ideal S
H : φ.IsArithFrobAt Q
inst✝ : Q.IsPrime
⊢ Ideal.comap φ Q = Q

Tactic:
refine le_antisymm (fun x hx ↦ ?_) H.le_comap

Result:
R : Type u_1
S : Type u_2
inst✝³ : CommRing R
inst✝² : CommRing S
inst✝¹ : Algebra R S
φ : S →ₐ[R] S
Q : Ideal S
H : φ.IsArithFrobAt Q
inst✝ : Q.IsPrime
x : S
hx : x ∈ Ideal.comap φ Q
⊢ x ∈ Q
-- Mathlib/GroupTheory/MonoidLocalization/Basic.lean
theorem mul_inv_right {f : M →* N} (h : ∀ y : S, IsUnit (f y)) (y : S) (w z : N) :
    z = w * (IsUnit.liftRight (f.restrict S) h y)⁻¹ ↔ z * f y = w

Proof state:
M : Type u_1
inst✝¹ : CommMonoid M
S : Submonoid M
N : Type u_2
inst✝ : CommMonoid N
f : M →* N
h : ∀ (y : ↥S), IsUnit (f ↑y)
y : ↥S
w z : N
⊢ z = w * ↑((IsUnit.liftRight (f.restrict S) h) y)⁻¹ ↔ z * f ↑y = w

Tactic:
rw [eq_comm, mul_inv_left h, mul_comm, eq_comm]

Result:
no goals
-- Mathlib/Algebra/Order/Monoid/Unbundled/Defs.lean
theorem contravariant_flip_iff [h : Std.Commutative mu] :
    Contravariant N N (flip mu) r ↔ Contravariant N N mu r

Proof state:
N : Type u_2
r : N → N → Prop
mu : N → N → N
h : Std.Commutative mu
⊢ Contravariant N N (fun b a => mu a b) r ↔ Contravariant N N mu r

Tactic:
simp_rw [h.comm]

Result:
no goals

Proof state:
N : Type u_2
r : N → N → Prop
mu : N → N → N
h : Std.Commutative mu
⊢ Contravariant N N (flip mu) r ↔ Contravariant N N mu r

Tactic:
unfold flip

Result:
N : Type u_2
r : N → N → Prop
mu : N → N → N
h : Std.Commutative mu
⊢ Contravariant N N (fun b a => mu a b) r ↔ Contravariant N N mu r
-- Mathlib/RingTheory/Ideal/Basis.lean
theorem constr_basisSpanSingleton {N : Type*} [Semiring N] [Module N S] [SMulCommClass R N S]
    (b : Basis ι R S) {x : S} (hx : x ≠ 0) :
    (b.constr N).toFun (((↑) : _ → S) ∘ (basisSpanSingleton b hx)) = Algebra.lmul R S x :=
  b.ext fun i => by simp

Proof state:
ι : Type u_1
R : Type u_2
S : Type u_3
inst✝⁶ : CommSemiring R
inst✝⁵ : CommRing S
inst✝⁴ : IsDomain S
inst✝³ : Algebra R S
N : Type u_4
inst✝² : Semiring N
inst✝¹ : Module N S
inst✝ : SMulCommClass R N S
b : Basis ι R S
x : S
hx : x ≠ 0
i : ι
⊢ ((↑(b.constr N)).toFun (Subtype.val ∘ ⇑(basisSpanSingleton b hx))) (b i) = ((Algebra.lmul R S) x) (b i)

Tactic:
simp

Result:
no goals
-- Mathlib/Data/Nat/Bits.lean
theorem bodd_eq_bits_head (n : ℕ) : n.bodd = n.bits.headI

Proof state:
case z

⊢ bodd 0 = (bits 0).headI

Tactic:
simp

Result:
no goals

Proof state:
case f
b✝ : Bool
n✝ : ℕ
h : n✝ = 0 → b✝ = true
a✝ : n✝.bodd = n✝.bits.headI
⊢ (bit b✝ n✝).bodd = (bit b✝ n✝).bits.headI

Tactic:
simp [bodd_bit, bits_append_bit _ _ h]

Result:
no goals

Proof state:
n : ℕ
⊢ n.bodd = n.bits.headI

Tactic:
induction n using Nat.binaryRec' with
| z => simp
| f _ _ h _ => simp [bodd_bit, bits_append_bit _ _ h]

Result:
no goals
-- Mathlib/Data/List/Nodup.lean
theorem Nodup.product {l₂ : List β} (d₁ : l₁.Nodup) (d₂ : l₂.Nodup) :
    (l₁ ×ˢ l₂).Nodup :=
  nodup_flatMap.2
    ⟨fun a _ => d₂.map <| LeftInverse.injective fun b => (rfl : (a, b).2 = b),
      d₁.imp fun {a₁ a₂} n x h₁ h₂ => by
        rcases mem_map.1 h₁ with ⟨b₁, _, rfl⟩
        rcases mem_map.1 h₂ with ⟨b₂, mb₂, ⟨⟩⟩
        exact n rfl⟩

Proof state:
case intro.intro.intro.intro.refl
α : Type u
β : Type v
l₁ : List α
l₂ : List β
d₁ : l₁.Nodup
d₂ : l₂.Nodup
a₁ : α
b₁ : β
left✝ : b₁ ∈ l₂
h₁ : (a₁, b₁) ∈ (fun a => map (Prod.mk a) l₂) a₁
n : a₁ ≠ a₁
h₂ : (a₁, b₁) ∈ (fun a => map (Prod.mk a) l₂) a₁
mb₂ : b₁ ∈ l₂
⊢ False

Tactic:
exact n rfl

Result:
no goals

Proof state:
α : Type u
β : Type v
l₁ : List α
l₂ : List β
d₁ : l₁.Nodup
d₂ : l₂.Nodup
a₁ a₂ : α
n : a₁ ≠ a₂
x : α × β
h₁ : x ∈ (fun a => map (Prod.mk a) l₂) a₁
h₂ : x ∈ (fun a => map (Prod.mk a) l₂) a₂
⊢ False

Tactic:
rcases mem_map.1 h₁ with ⟨b₁, _, rfl⟩

Result:
case intro.intro
α : Type u
β : Type v
l₁ : List α
l₂ : List β
d₁ : l₁.Nodup
d₂ : l₂.Nodup
a₁ a₂ : α
n : a₁ ≠ a₂
b₁ : β
left✝ : b₁ ∈ l₂
h₁ : (a₁, b₁) ∈ (fun a => map (Prod.mk a) l₂) a₁
h₂ : (a₁, b₁) ∈ (fun a => map (Prod.mk a) l₂) a₂
⊢ False

Proof state:
case intro.intro
α : Type u
β : Type v
l₁ : List α
l₂ : List β
d₁ : l₁.Nodup
d₂ : l₂.Nodup
a₁ a₂ : α
n : a₁ ≠ a₂
b₁ : β
left✝ : b₁ ∈ l₂
h₁ : (a₁, b₁) ∈ (fun a => map (Prod.mk a) l₂) a₁
h₂ : (a₁, b₁) ∈ (fun a => map (Prod.mk a) l₂) a₂
⊢ False

Tactic:
rcases mem_map.1 h₂ with ⟨b₂, mb₂, ⟨⟩⟩

Result:
case intro.intro.intro.intro.refl
α : Type u
β : Type v
l₁ : List α
l₂ : List β
d₁ : l₁.Nodup
d₂ : l₂.Nodup
a₁ : α
b₁ : β
left✝ : b₁ ∈ l₂
h₁ : (a₁, b₁) ∈ (fun a => map (Prod.mk a) l₂) a₁
n : a₁ ≠ a₁
h₂ : (a₁, b₁) ∈ (fun a => map (Prod.mk a) l₂) a₁
mb₂ : b₁ ∈ l₂
⊢ False
-- Mathlib/Analysis/Asymptotics/Defs.lean
theorem isBigOWith_norm_right : (IsBigOWith c l f fun x => ‖g' x‖) ↔ IsBigOWith c l f g'

Proof state:
α : Type u_1
E : Type u_3
F' : Type u_7
inst✝¹ : Norm E
inst✝ : SeminormedAddCommGroup F'
c : ℝ
f : α → E
g' : α → F'
l : Filter α
⊢ (IsBigOWith c l f fun x => ‖g' x‖) ↔ IsBigOWith c l f g'

Tactic:
simp only [IsBigOWith_def, norm_norm]

Result:
no goals
-- Mathlib/Analysis/SpecialFunctions/Pow/NNReal.lean
theorem prod_rpow_of_nonneg {ι} {s : Finset ι} {f : ι → ℝ≥0∞} {r : ℝ} (hr : 0 ≤ r) :
    ∏ i ∈ s, f i ^ r = (∏ i ∈ s, f i) ^ r

Proof state:
ι : Type u_1
s : Finset ι
f : ι → ℝ≥0∞
r : ℝ
hr : 0 ≤ r
⊢ ∏ i ∈ s, f i ^ r = (∏ i ∈ s, f i) ^ r

Tactic:
classical
induction s using Finset.induction with
| empty => simp
| insert hi ih => simp_rw [prod_insert hi, ih, ← mul_rpow_of_nonneg _ _ hr]

Result:
no goals

Proof state:
ι : Type u_1
s : Finset ι
f : ι → ℝ≥0∞
r : ℝ
hr : 0 ≤ r
⊢ ∏ i ∈ s, f i ^ r = (∏ i ∈ s, f i) ^ r

Tactic:
induction s using Finset.induction with
| empty => simp
| insert hi ih => simp_rw [prod_insert hi, ih, ← mul_rpow_of_nonneg _ _ hr]

Result:
no goals

Proof state:
case insert
ι : Type u_1
f : ι → ℝ≥0∞
r : ℝ
hr : 0 ≤ r
a✝ : ι
s✝ : Finset ι
hi : a✝ ∉ s✝
ih : ∏ i ∈ s✝, f i ^ r = (∏ i ∈ s✝, f i) ^ r
⊢ ∏ i ∈ insert a✝ s✝, f i ^ r = (∏ i ∈ insert a✝ s✝, f i) ^ r

Tactic:
simp_rw [prod_insert hi, ih, ← mul_rpow_of_nonneg _ _ hr]

Result:
no goals

Proof state:
case empty
ι : Type u_1
f : ι → ℝ≥0∞
r : ℝ
hr : 0 ≤ r
⊢ ∏ i ∈ ∅, f i ^ r = (∏ i ∈ ∅, f i) ^ r

Tactic:
simp

Result:
no goals
-- Mathlib/Algebra/Polynomial/Lifts.lean
theorem lifts_and_natDegree_eq_and_monic {p : S[X]} (hlifts : p ∈ lifts f) (hp : p.Monic) :
    ∃ q : R[X], map f q = p ∧ q.natDegree = p.natDegree ∧ q.Monic

Proof state:
R : Type u
inst✝¹ : Semiring R
S : Type v
inst✝ : Semiring S
f : R →+* S
hR : Subsingleton S
hlifts : 1 ∈ lifts f
hp : Monic 1
⊢ Monic 1

Tactic:
simp

Result:
no goals

Proof state:
case inl
R : Type u
inst✝¹ : Semiring R
S : Type v
inst✝ : Semiring S
f : R →+* S
hR : Subsingleton S
hlifts : 1 ∈ lifts f
hp : Monic 1
⊢ ∃ q, map f q = 1 ∧ q.natDegree = natDegree 1 ∧ q.Monic

Tactic:
exact ⟨1, Subsingleton.elim _ _, by simp, by simp⟩

Result:
no goals

Proof state:
R : Type u
inst✝¹ : Semiring R
S : Type v
inst✝ : Semiring S
f : R →+* S
hR : Subsingleton S
hlifts : 1 ∈ lifts f
hp : Monic 1
⊢ natDegree 1 = natDegree 1

Tactic:
simp

Result:
no goals

Proof state:
case inl
R : Type u
inst✝¹ : Semiring R
S : Type v
inst✝ : Semiring S
f : R →+* S
p : S[X]
hlifts : p ∈ lifts f
hp : p.Monic
hR : Subsingleton S
⊢ ∃ q, map f q = p ∧ q.natDegree = p.natDegree ∧ q.Monic

Tactic:
obtain rfl : p = 1 := Subsingleton.elim _ _

Result:
case inl
R : Type u
inst✝¹ : Semiring R
S : Type v
inst✝ : Semiring S
f : R →+* S
hR : Subsingleton S
hlifts : 1 ∈ lifts f
hp : Monic 1
⊢ ∃ q, map f q = 1 ∧ q.natDegree = natDegree 1 ∧ q.Monic

Proof state:
case inr.intro.intro.intro
R : Type u
inst✝¹ : Semiring R
S : Type v
inst✝ : Semiring S
f : R →+* S
p : S[X]
hlifts : p ∈ lifts f
hp : p.Monic
hR : Nontrivial S
p' : R[X]
h₁ : map f p' = p
h₂ : p'.degree = p.degree
h₃ : p'.Monic
⊢ ∃ q, map f q = p ∧ q.natDegree = p.natDegree ∧ q.Monic

Tactic:
exact ⟨p', h₁, natDegree_eq_of_degree_eq h₂, h₃⟩

Result:
no goals

Proof state:
case inr
R : Type u
inst✝¹ : Semiring R
S : Type v
inst✝ : Semiring S
f : R →+* S
p : S[X]
hlifts : p ∈ lifts f
hp : p.Monic
hR : Nontrivial S
⊢ ∃ q, map f q = p ∧ q.natDegree = p.natDegree ∧ q.Monic

Tactic:
obtain ⟨p', h₁, h₂, h₃⟩ := lifts_and_degree_eq_and_monic hlifts hp

Result:
case inr.intro.intro.intro
R : Type u
inst✝¹ : Semiring R
S : Type v
inst✝ : Semiring S
f : R →+* S
p : S[X]
hlifts : p ∈ lifts f
hp : p.Monic
hR : Nontrivial S
p' : R[X]
h₁ : map f p' = p
h₂ : p'.degree = p.degree
h₃ : p'.Monic
⊢ ∃ q, map f q = p ∧ q.natDegree = p.natDegree ∧ q.Monic

Proof state:
R : Type u
inst✝¹ : Semiring R
S : Type v
inst✝ : Semiring S
f : R →+* S
p : S[X]
hlifts : p ∈ lifts f
hp : p.Monic
⊢ ∃ q, map f q = p ∧ q.natDegree = p.natDegree ∧ q.Monic

Tactic:
rcases subsingleton_or_nontrivial S with hR | hR

Result:
case inl
R : Type u
inst✝¹ : Semiring R
S : Type v
inst✝ : Semiring S
f : R →+* S
p : S[X]
hlifts : p ∈ lifts f
hp : p.Monic
hR : Subsingleton S
⊢ ∃ q, map f q = p ∧ q.natDegree = p.natDegree ∧ q.Monic

case inr
R : Type u
inst✝¹ : Semiring R
S : Type v
inst✝ : Semiring S
f : R →+* S
p : S[X]
hlifts : p ∈ lifts f
hp : p.Monic
hR : Nontrivial S
⊢ ∃ q, map f q = p ∧ q.natDegree = p.natDegree ∧ q.Monic
-- Mathlib/Algebra/Group/Pi/Basic.lean
theorem mulSingle_comm [One β] (i : I) (x : β) (i' : I) :
    (mulSingle i x : I → β) i' = (mulSingle i' x : I → β) i

Proof state:
I : Type u
β : Type u_2
inst✝¹ : DecidableEq I
inst✝ : One β
i : I
x : β
i' : I
⊢ mulSingle i x i' = mulSingle i' x i

Tactic:
simp [mulSingle_apply, eq_comm]

Result:
no goals
-- Mathlib/Analysis/Calculus/TangentCone.lean
theorem UniqueDiffWithinAt.pi (ι : Type*) [Finite ι] (E : ι → Type*)
    [∀ i, NormedAddCommGroup (E i)] [∀ i, NormedSpace 𝕜 (E i)] (s : ∀ i, Set (E i)) (x : ∀ i, E i)
    (I : Set ι) (h : ∀ i ∈ I, UniqueDiffWithinAt 𝕜 (s i) (x i)) :
    UniqueDiffWithinAt 𝕜 (Set.pi I s) x

Proof state:
𝕜 : Type u_1
inst✝³ : NontriviallyNormedField 𝕜
ι : Type u_5
inst✝² : Finite ι
E : ι → Type u_6
inst✝¹ : (i : ι) → NormedAddCommGroup (E i)
inst✝ : (i : ι) → NormedSpace 𝕜 (E i)
s : (i : ι) → Set (E i)
x : (i : ι) → E i
I : Set ι
h : ∀ i ∈ I, UniqueDiffWithinAt 𝕜 (s i) (x i)
⊢ UniqueDiffWithinAt 𝕜 (I.pi s) x

Tactic:
classical
rw [← Set.univ_pi_piecewise_univ]
refine UniqueDiffWithinAt.univ_pi ι E _ _ fun i => ?_
by_cases hi : i ∈ I <;> simp [*, uniqueDiffWithinAt_univ]

Result:
no goals

Proof state:
𝕜 : Type u_1
inst✝³ : NontriviallyNormedField 𝕜
ι : Type u_5
inst✝² : Finite ι
E : ι → Type u_6
inst✝¹ : (i : ι) → NormedAddCommGroup (E i)
inst✝ : (i : ι) → NormedSpace 𝕜 (E i)
s : (i : ι) → Set (E i)
x : (i : ι) → E i
I : Set ι
h : ∀ i ∈ I, UniqueDiffWithinAt 𝕜 (s i) (x i)
⊢ UniqueDiffWithinAt 𝕜 (I.pi s) x

Tactic:
rw [← Set.univ_pi_piecewise_univ]

Result:
𝕜 : Type u_1
inst✝³ : NontriviallyNormedField 𝕜
ι : Type u_5
inst✝² : Finite ι
E : ι → Type u_6
inst✝¹ : (i : ι) → NormedAddCommGroup (E i)
inst✝ : (i : ι) → NormedSpace 𝕜 (E i)
s : (i : ι) → Set (E i)
x : (i : ι) → E i
I : Set ι
h : ∀ i ∈ I, UniqueDiffWithinAt 𝕜 (s i) (x i)
⊢ UniqueDiffWithinAt 𝕜 (univ.pi (I.piecewise s fun x => univ)) x

Proof state:
𝕜 : Type u_1
inst✝³ : NontriviallyNormedField 𝕜
ι : Type u_5
inst✝² : Finite ι
E : ι → Type u_6
inst✝¹ : (i : ι) → NormedAddCommGroup (E i)
inst✝ : (i : ι) → NormedSpace 𝕜 (E i)
s : (i : ι) → Set (E i)
x : (i : ι) → E i
I : Set ι
h : ∀ i ∈ I, UniqueDiffWithinAt 𝕜 (s i) (x i)
⊢ UniqueDiffWithinAt 𝕜 (univ.pi (I.piecewise s fun x => univ)) x

Tactic:
refine UniqueDiffWithinAt.univ_pi ι E _ _ fun i => ?_

Result:
𝕜 : Type u_1
inst✝³ : NontriviallyNormedField 𝕜
ι : Type u_5
inst✝² : Finite ι
E : ι → Type u_6
inst✝¹ : (i : ι) → NormedAddCommGroup (E i)
inst✝ : (i : ι) → NormedSpace 𝕜 (E i)
s : (i : ι) → Set (E i)
x : (i : ι) → E i
I : Set ι
h : ∀ i ∈ I, UniqueDiffWithinAt 𝕜 (s i) (x i)
i : ι
⊢ UniqueDiffWithinAt 𝕜 (I.piecewise s (fun x => univ) i) (x i)

Proof state:
𝕜 : Type u_1
inst✝³ : NontriviallyNormedField 𝕜
ι : Type u_5
inst✝² : Finite ι
E : ι → Type u_6
inst✝¹ : (i : ι) → NormedAddCommGroup (E i)
inst✝ : (i : ι) → NormedSpace 𝕜 (E i)
s : (i : ι) → Set (E i)
x : (i : ι) → E i
I : Set ι
h : ∀ i ∈ I, UniqueDiffWithinAt 𝕜 (s i) (x i)
i : ι
⊢ UniqueDiffWithinAt 𝕜 (I.piecewise s (fun x => univ) i) (x i)

Tactic:
by_cases hi : i ∈ I <;> simp [*, uniqueDiffWithinAt_univ]

Result:
no goals
-- Mathlib/Data/Matroid/Dual.lean
theorem eq_dual_comm {M₁ M₂ : Matroid α} : M₁ = M₂✶ ↔ M₂ = M₁✶

Proof state:
α : Type u_1
M₁ M₂ : Matroid α
⊢ M₁ = M₂✶ ↔ M₂ = M₁✶

Tactic:
rw [← dual_inj, dual_dual, eq_comm]

Result:
no goals
-- Mathlib/Algebra/Group/Commute/Defs.lean
theorem inv (hab : Commute a b) : (a * b)⁻¹ = a⁻¹ * b⁻¹

Proof state:
G : Type u_1
inst✝ : DivisionMonoid G
a b : G
hab : Commute a b
⊢ (a * b)⁻¹ = a⁻¹ * b⁻¹

Tactic:
rw [hab.eq, mul_inv_rev]

Result:
no goals
-- Mathlib/Topology/Separation/Basic.lean
theorem isClosedMap_const {X Y} [TopologicalSpace X] [TopologicalSpace Y] [T1Space Y] {y : Y} :
    IsClosedMap (Function.const X y) :=
  IsClosedMap.of_nonempty fun s _ h2s => by simp_rw [const, h2s.image_const, isClosed_singleton]

Proof state:
X : Type u_3
Y : Type u_4
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
inst✝ : T1Space Y
y : Y
s : Set X
x✝ : IsClosed s
h2s : s.Nonempty
⊢ IsClosed (const X y '' s)

Tactic:
simp_rw [const, h2s.image_const, isClosed_singleton]

Result:
no goals
-- Mathlib/FieldTheory/Normal/Defs.lean
theorem AlgEquiv.restrictNormalHom_id (F K : Type*)
    [Field F] [Field K] [Algebra F K] [Normal F K] :
    AlgEquiv.restrictNormalHom K = MonoidHom.id (K ≃ₐ[F] K)

Proof state:
case h.h
F : Type u_6
K : Type u_7
inst✝³ : Field F
inst✝² : Field K
inst✝¹ : Algebra F K
inst✝ : Normal F K
f : K ≃ₐ[F] K
x : K
⊢ (f.restrictNormal K) x = f x

Tactic:
apply (algebraMap K K).injective

Result:
case h.h.a
F : Type u_6
K : Type u_7
inst✝³ : Field F
inst✝² : Field K
inst✝¹ : Algebra F K
inst✝ : Normal F K
f : K ≃ₐ[F] K
x : K
⊢ (algebraMap K K) ((f.restrictNormal K) x) = (algebraMap K K) (f x)

Proof state:
case h.h.a
F : Type u_6
K : Type u_7
inst✝³ : Field F
inst✝² : Field K
inst✝¹ : Algebra F K
inst✝ : Normal F K
f : K ≃ₐ[F] K
x : K
⊢ f ((algebraMap K K) x) = (algebraMap K K) (f x)

Tactic:
simp only [Algebra.id.map_eq_id, RingHom.id_apply]

Result:
no goals

Proof state:
case h.h.a
F : Type u_6
K : Type u_7
inst✝³ : Field F
inst✝² : Field K
inst✝¹ : Algebra F K
inst✝ : Normal F K
f : K ≃ₐ[F] K
x : K
⊢ (algebraMap K K) ((f.restrictNormal K) x) = (algebraMap K K) (f x)

Tactic:
rw [AlgEquiv.restrictNormal_commutes]

Result:
case h.h.a
F : Type u_6
K : Type u_7
inst✝³ : Field F
inst✝² : Field K
inst✝¹ : Algebra F K
inst✝ : Normal F K
f : K ≃ₐ[F] K
x : K
⊢ f ((algebraMap K K) x) = (algebraMap K K) (f x)

Proof state:
F : Type u_6
K : Type u_7
inst✝³ : Field F
inst✝² : Field K
inst✝¹ : Algebra F K
inst✝ : Normal F K
⊢ restrictNormalHom K = MonoidHom.id (K ≃ₐ[F] K)

Tactic:
ext f x

Result:
case h.h
F : Type u_6
K : Type u_7
inst✝³ : Field F
inst✝² : Field K
inst✝¹ : Algebra F K
inst✝ : Normal F K
f : K ≃ₐ[F] K
x : K
⊢ ((restrictNormalHom K) f) x = ((MonoidHom.id (K ≃ₐ[F] K)) f) x

Proof state:
case h.h
F : Type u_6
K : Type u_7
inst✝³ : Field F
inst✝² : Field K
inst✝¹ : Algebra F K
inst✝ : Normal F K
f : K ≃ₐ[F] K
x : K
⊢ ((restrictNormalHom K) f) x = ((MonoidHom.id (K ≃ₐ[F] K)) f) x

Tactic:
dsimp only [restrictNormalHom, MonoidHom.mk'_apply, MonoidHom.id_apply]

Result:
case h.h
F : Type u_6
K : Type u_7
inst✝³ : Field F
inst✝² : Field K
inst✝¹ : Algebra F K
inst✝ : Normal F K
f : K ≃ₐ[F] K
x : K
⊢ (f.restrictNormal K) x = f x
-- Mathlib/CategoryTheory/Adjunction/Mates.lean
theorem mateEquiv_counit_symm (α : TwoSquare R₁ H G R₂) (d : D) :
    L₂.map (α.app _) ≫ adj₂.counit.app _ =
      ((mateEquiv adj₁ adj₂).symm α).app _ ≫ H.map (adj₁.counit.app d)

Proof state:
C : Type u₁
D : Type u₂
E : Type u₃
F : Type u₄
inst✝³ : Category.{v₁, u₁} C
inst✝² : Category.{v₂, u₂} D
inst✝¹ : Category.{v₃, u₃} E
inst✝ : Category.{v₄, u₄} F
G : C ⥤ E
H : D ⥤ F
L₁ : C ⥤ D
R₁ : D ⥤ C
L₂ : E ⥤ F
R₂ : F ⥤ E
adj₁ : L₁ ⊣ R₁
adj₂ : L₂ ⊣ R₂
α : TwoSquare R₁ H G R₂
d : D
⊢ L₂.map (α.app d) ≫ adj₂.counit.app (H.obj d) =
    ((mateEquiv adj₁ adj₂).symm α).app (R₁.obj d) ≫ H.map (adj₁.counit.app d)

Tactic:
conv_lhs => rw [← (mateEquiv adj₁ adj₂).right_inv α]

Result:
C : Type u₁
D : Type u₂
E : Type u₃
F : Type u₄
inst✝³ : Category.{v₁, u₁} C
inst✝² : Category.{v₂, u₂} D
inst✝¹ : Category.{v₃, u₃} E
inst✝ : Category.{v₄, u₄} F
G : C ⥤ E
H : D ⥤ F
L₁ : C ⥤ D
R₁ : D ⥤ C
L₂ : E ⥤ F
R₂ : F ⥤ E
adj₁ : L₁ ⊣ R₁
adj₂ : L₂ ⊣ R₂
α : TwoSquare R₁ H G R₂
d : D
⊢ L₂.map (((mateEquiv adj₁ adj₂).toFun ((mateEquiv adj₁ adj₂).invFun α)).app d) ≫ adj₂.counit.app (H.obj d) =
    ((mateEquiv adj₁ adj₂).symm α).app (R₁.obj d) ≫ H.map (adj₁.counit.app d)

Proof state:
C : Type u₁
D : Type u₂
E : Type u₃
F : Type u₄
inst✝³ : Category.{v₁, u₁} C
inst✝² : Category.{v₂, u₂} D
inst✝¹ : Category.{v₃, u₃} E
inst✝ : Category.{v₄, u₄} F
G : C ⥤ E
H : D ⥤ F
L₁ : C ⥤ D
R₁ : D ⥤ C
L₂ : E ⥤ F
R₂ : F ⥤ E
adj₁ : L₁ ⊣ R₁
adj₂ : L₂ ⊣ R₂
α : TwoSquare R₁ H G R₂
d : D
⊢ L₂.map (((mateEquiv adj₁ adj₂).toFun ((mateEquiv adj₁ adj₂).invFun α)).app d) ≫ adj₂.counit.app (H.obj d) =
    ((mateEquiv adj₁ adj₂).symm α).app (R₁.obj d) ≫ H.map (adj₁.counit.app d)

Tactic:
exact (mateEquiv_counit adj₁ adj₂ ((mateEquiv adj₁ adj₂).symm α) d)

Result:
no goals
-- Mathlib/ModelTheory/Equivalence.lean
theorem imp {φ ψ φ' ψ' : L.BoundedFormula α n} (h : φ ⇔[T] ψ) (h' : φ' ⇔[T] ψ') :
    (φ.imp φ') ⇔[T] (ψ.imp ψ')

Proof state:
L : Language
T : L.Theory
α : Type w
n : ℕ
φ ψ φ' ψ' : L.BoundedFormula α n
h : φ ⇔[T] ψ
h' : φ' ⇔[T] ψ'
⊢ φ ⟹ φ' ⇔[T] ψ ⟹ ψ'

Tactic:
simp_rw [Theory.Iff, ModelsBoundedFormula, BoundedFormula.realize_iff,
  BoundedFormula.realize_imp]

Result:
L : Language
T : L.Theory
α : Type w
n : ℕ
φ ψ φ' ψ' : L.BoundedFormula α n
h : φ ⇔[T] ψ
h' : φ' ⇔[T] ψ'
⊢ ∀ (M : T.ModelType) (v : α → ↑M) (xs : Fin n → ↑M),
    φ.Realize v xs → φ'.Realize v xs ↔ ψ.Realize v xs → ψ'.Realize v xs

Proof state:
L : Language
T : L.Theory
α : Type w
n : ℕ
φ ψ φ' ψ' : L.BoundedFormula α n
h : φ ⇔[T] ψ
h' : φ' ⇔[T] ψ'
⊢ ∀ (M : T.ModelType) (v : α → ↑M) (xs : Fin n → ↑M),
    φ.Realize v xs → φ'.Realize v xs ↔ ψ.Realize v xs → ψ'.Realize v xs

Tactic:
exact fun M v xs => imp_congr h.realize_bd_iff h'.realize_bd_iff

Result:
no goals
-- Mathlib/Algebra/Order/Group/Lattice.lean
@[to_additive]
lemma inf_mul_sup [MulLeftMono α] (a b : α) : (a ⊓ b) * (a ⊔ b) = a * b :=
  calc
    (a ⊓ b) * (a ⊔ b) = (a ⊓ b) * (a * b * (b⁻¹ ⊔ a⁻¹))

Proof state:
α : Type u_1
inst✝² : Lattice α
inst✝¹ : CommGroup α
inst✝ : MulLeftMono α
a b : α
⊢ (a ⊓ b) * (a * b * (a ⊓ b)⁻¹) = a * b

Tactic:
rw [mul_comm, inv_mul_cancel_right]

Result:
no goals

Proof state:
α : Type u_1
inst✝² : Lattice α
inst✝¹ : CommGroup α
inst✝ : MulLeftMono α
a b : α
⊢ (a ⊓ b) * (a ⊔ b) = (a ⊓ b) * (a * b * (b⁻¹ ⊔ a⁻¹))

Tactic:
rw [mul_sup b⁻¹ a⁻¹ (a * b), mul_inv_cancel_right, mul_inv_cancel_comm]

Result:
no goals

Proof state:
α : Type u_1
inst✝² : Lattice α
inst✝¹ : CommGroup α
inst✝ : MulLeftMono α
a b : α
⊢ (a ⊓ b) * (a * b * (b⁻¹ ⊔ a⁻¹)) = (a ⊓ b) * (a * b * (a ⊓ b)⁻¹)

Tactic:
rw [inv_inf, sup_comm]

Result:
no goals
-- Mathlib/Analysis/InnerProductSpace/PiL2.lean
theorem Complex.coe_orthonormalBasisOneI :
    (Complex.orthonormalBasisOneI : Fin 2 → ℂ) = ![1, I]

Proof state:
⊢ ⇑orthonormalBasisOneI = ![1, I]

Tactic:
simp [Complex.orthonormalBasisOneI]

Result:
no goals
-- Mathlib/Algebra/Order/Ring/Abs.lean
@[simp]
lemma abs_mul_self (a : α) : |a * a| = a * a

Proof state:
α : Type u_1
inst✝ : LinearOrderedRing α
a : α
⊢ |a * a| = a * a

Tactic:
rw [abs_mul, abs_mul_abs_self]

Result:
no goals
-- Mathlib/Topology/Compactness/SigmaCompact.lean
/-- Countable unions of compact sets are σ-compact. -/
lemma isSigmaCompact_iUnion_of_isCompact [hι : Countable ι] (s : ι → Set X)
    (hcomp : ∀ i, IsCompact (s i)) : IsSigmaCompact (⋃ i, s i)

Proof state:
X : Type u_1
ι : Type u_3
inst✝ : TopologicalSpace X
hι : Countable ι
s : ι → Set X
hcomp : ∀ (i : ι), IsCompact (s i)
⊢ IsSigmaCompact (⋃ i, s i)

Tactic:
rcases isEmpty_or_nonempty ι

Result:
case inl
X : Type u_1
ι : Type u_3
inst✝ : TopologicalSpace X
hι : Countable ι
s : ι → Set X
hcomp : ∀ (i : ι), IsCompact (s i)
h✝ : IsEmpty ι
⊢ IsSigmaCompact (⋃ i, s i)

case inr
X : Type u_1
ι : Type u_3
inst✝ : TopologicalSpace X
hι : Countable ι
s : ι → Set X
hcomp : ∀ (i : ι), IsCompact (s i)
h✝ : Nonempty ι
⊢ IsSigmaCompact (⋃ i, s i)

Proof state:
case inl
X : Type u_1
ι : Type u_3
inst✝ : TopologicalSpace X
hι : Countable ι
s : ι → Set X
hcomp : ∀ (i : ι), IsCompact (s i)
h✝ : IsEmpty ι
⊢ IsSigmaCompact (⋃ i, s i)

Tactic:
simp only [iUnion_of_empty, isSigmaCompact_empty]

Result:
no goals

Proof state:
case inr.intro
X : Type u_1
ι : Type u_3
inst✝ : TopologicalSpace X
hι : Countable ι
s : ι → Set X
hcomp : ∀ (i : ι), IsCompact (s i)
h✝ : Nonempty ι
f : ℕ → ι
hf : Function.Surjective f
⊢ IsSigmaCompact (⋃ i, s i)

Tactic:
exact ⟨s ∘ f, fun n ↦ hcomp (f n), Function.Surjective.iUnion_comp hf _⟩

Result:
no goals

Proof state:
case inr
X : Type u_1
ι : Type u_3
inst✝ : TopologicalSpace X
hι : Countable ι
s : ι → Set X
hcomp : ∀ (i : ι), IsCompact (s i)
h✝ : Nonempty ι
⊢ IsSigmaCompact (⋃ i, s i)

Tactic:
obtain ⟨f, hf⟩ := countable_iff_exists_surjective.mp hι

Result:
case inr.intro
X : Type u_1
ι : Type u_3
inst✝ : TopologicalSpace X
hι : Countable ι
s : ι → Set X
hcomp : ∀ (i : ι), IsCompact (s i)
h✝ : Nonempty ι
f : ℕ → ι
hf : Function.Surjective f
⊢ IsSigmaCompact (⋃ i, s i)
-- Mathlib/.lake/packages/lean4/src/lean/Std/Data/DHashMap/Internal/RawLemmas.lean
theorem getKey!_eq_getKeyD_default [EquivBEq α] [LawfulHashable α] [Inhabited α] (h : m.1.WF)
    {a : α} :
    m.getKey! a = m.getKeyD a default

Proof state:
α : Type u
β : α → Type v
m : Raw₀ α β
inst✝⁴ : BEq α
inst✝³ : Hashable α
inst✝² : EquivBEq α
inst✝¹ : LawfulHashable α
inst✝ : Inhabited α
h : m.val.WF
a : α
⊢ m.getKey! a = m.getKeyD a default

Tactic:
simp_to_model using List.getKey!_eq_getKeyD_default

Result:
no goals
-- Mathlib/Algebra/MvPolynomial/Eval.lean
theorem eval₂_X (n) : (X n).eval₂ f g = g n

Proof state:
R : Type u
S₁ : Type v
σ : Type u_1
inst✝¹ : CommSemiring R
inst✝ : CommSemiring S₁
f : R →+* S₁
g : σ → S₁
n : σ
⊢ eval₂ f g (X n) = g n

Tactic:
simp [eval₂_monomial, f.map_one, X, prod_single_index, pow_one]

Result:
no goals
-- Mathlib/NumberTheory/NumberField/Embeddings.lean
lemma IsUnramifiedAtInfinitePlaces.bot [h₁ : IsUnramifiedAtInfinitePlaces k F]
    [Algebra.IsAlgebraic K F] :
    IsUnramifiedAtInfinitePlaces k K where
  isUnramified w

Proof state:
case intro
k : Type u_1
inst✝⁷ : Field k
K : Type u_2
inst✝⁶ : Field K
F : Type u_3
inst✝⁵ : Field F
inst✝⁴ : Algebra k K
inst✝³ : Algebra k F
inst✝² : Algebra K F
inst✝¹ : IsScalarTower k K F
h₁ : IsUnramifiedAtInfinitePlaces k F
inst✝ : Algebra.IsAlgebraic K F
w : InfinitePlace F
⊢ InfinitePlace.IsUnramified k ((fun x => x.comap (algebraMap K F)) w)

Tactic:
exact (h₁.1 w).comap K

Result:
no goals

Proof state:
k : Type u_1
inst✝⁷ : Field k
K : Type u_2
inst✝⁶ : Field K
F : Type u_3
inst✝⁵ : Field F
inst✝⁴ : Algebra k K
inst✝³ : Algebra k F
inst✝² : Algebra K F
inst✝¹ : IsScalarTower k K F
h₁ : IsUnramifiedAtInfinitePlaces k F
inst✝ : Algebra.IsAlgebraic K F
w : InfinitePlace K
⊢ InfinitePlace.IsUnramified k w

Tactic:
obtain ⟨w, rfl⟩ := InfinitePlace.comap_surjective (K := F) w

Result:
case intro
k : Type u_1
inst✝⁷ : Field k
K : Type u_2
inst✝⁶ : Field K
F : Type u_3
inst✝⁵ : Field F
inst✝⁴ : Algebra k K
inst✝³ : Algebra k F
inst✝² : Algebra K F
inst✝¹ : IsScalarTower k K F
h₁ : IsUnramifiedAtInfinitePlaces k F
inst✝ : Algebra.IsAlgebraic K F
w : InfinitePlace F
⊢ InfinitePlace.IsUnramified k ((fun x => x.comap (algebraMap K F)) w)