harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/FieldTheory/Normal/Defs.lean
theorem Normal.of_algEquiv [h : Normal F E] (f : E ≃ₐ[F] E') : Normal F E'

Proof state:
F : Type u_1
inst✝⁴ : Field F
E : Type u_3
inst✝³ : Field E
inst✝² : Algebra F E
E' : Type u_4
inst✝¹ : Field E'
inst✝ : Algebra F E'
h : ∀ (x : E), IsIntegral F x ∧ Splits (algebraMap F E) (minpoly F x)
f : E ≃ₐ[F] E'
⊢ ∀ (x : E'), IsIntegral F x ∧ Splits (algebraMap F E') (minpoly F x)

Tactic:
intro x

Result:
F : Type u_1
inst✝⁴ : Field F
E : Type u_3
inst✝³ : Field E
inst✝² : Algebra F E
E' : Type u_4
inst✝¹ : Field E'
inst✝ : Algebra F E'
h : ∀ (x : E), IsIntegral F x ∧ Splits (algebraMap F E) (minpoly F x)
f : E ≃ₐ[F] E'
x : E'
⊢ IsIntegral F x ∧ Splits (algebraMap F E') (minpoly F x)

Proof state:
F : Type u_1
inst✝⁴ : Field F
E : Type u_3
inst✝³ : Field E
inst✝² : Algebra F E
E' : Type u_4
inst✝¹ : Field E'
inst✝ : Algebra F E'
h : ∀ (x : E), IsIntegral F x ∧ Splits (algebraMap F E) (minpoly F x)
f : E ≃ₐ[F] E'
x : E'
⊢ IsIntegral F x ∧ Splits (algebraMap F E') (minpoly F x)

Tactic:
specialize h (f.symm x)

Result:
F : Type u_1
inst✝⁴ : Field F
E : Type u_3
inst✝³ : Field E
inst✝² : Algebra F E
E' : Type u_4
inst✝¹ : Field E'
inst✝ : Algebra F E'
f : E ≃ₐ[F] E'
x : E'
h : IsIntegral F (f.symm x) ∧ Splits (algebraMap F E) (minpoly F (f.symm x))
⊢ IsIntegral F x ∧ Splits (algebraMap F E') (minpoly F x)

Proof state:
F : Type u_1
inst✝⁴ : Field F
E : Type u_3
inst✝³ : Field E
inst✝² : Algebra F E
E' : Type u_4
inst✝¹ : Field E'
inst✝ : Algebra F E'
h : Normal F E
f : E ≃ₐ[F] E'
⊢ Normal F E'

Tactic:
rw [normal_iff] at h ⊢

Result:
F : Type u_1
inst✝⁴ : Field F
E : Type u_3
inst✝³ : Field E
inst✝² : Algebra F E
E' : Type u_4
inst✝¹ : Field E'
inst✝ : Algebra F E'
h : ∀ (x : E), IsIntegral F x ∧ Splits (algebraMap F E) (minpoly F x)
f : E ≃ₐ[F] E'
⊢ ∀ (x : E'), IsIntegral F x ∧ Splits (algebraMap F E') (minpoly F x)

Proof state:
F : Type u_1
inst✝⁴ : Field F
E : Type u_3
inst✝³ : Field E
inst✝² : Algebra F E
E' : Type u_4
inst✝¹ : Field E'
inst✝ : Algebra F E'
f : E ≃ₐ[F] E'
x : E'
h : IsIntegral F (f.symm x) ∧ Splits (algebraMap F E) (minpoly F (f.symm x))
⊢ IsIntegral F x ∧ Splits (algebraMap F E') (minpoly F x)

Tactic:
rw [← f.apply_symm_apply x, minpoly.algEquiv_eq, ← f.toAlgHom.comp_algebraMap]

Result:
F : Type u_1
inst✝⁴ : Field F
E : Type u_3
inst✝³ : Field E
inst✝² : Algebra F E
E' : Type u_4
inst✝¹ : Field E'
inst✝ : Algebra F E'
f : E ≃ₐ[F] E'
x : E'
h : IsIntegral F (f.symm x) ∧ Splits (algebraMap F E) (minpoly F (f.symm x))
⊢ IsIntegral F (f (f.symm x)) ∧ Splits ((↑↑f).comp (algebraMap F E)) (minpoly F (f.symm x))

Proof state:
F : Type u_1
inst✝⁴ : Field F
E : Type u_3
inst✝³ : Field E
inst✝² : Algebra F E
E' : Type u_4
inst✝¹ : Field E'
inst✝ : Algebra F E'
f : E ≃ₐ[F] E'
x : E'
h : IsIntegral F (f.symm x) ∧ Splits (algebraMap F E) (minpoly F (f.symm x))
⊢ IsIntegral F (f (f.symm x)) ∧ Splits ((↑↑f).comp (algebraMap F E)) (minpoly F (f.symm x))

Tactic:
exact ⟨h.1.map f, splits_comp_of_splits _ _ h.2⟩

Result:
no goals
-- Mathlib/Algebra/Lie/Character.lean
theorem lieCharacter_apply_lie (χ : LieCharacter R L) (x y : L) : χ ⁅x, y⁆ = 0

Proof state:
R : Type u
L : Type v
inst✝² : CommRing R
inst✝¹ : LieRing L
inst✝ : LieAlgebra R L
χ : LieCharacter R L
x y : L
⊢ χ ⁅x, y⁆ = 0

Tactic:
rw [LieHom.map_lie, LieRing.of_associative_ring_bracket, mul_comm, sub_self]

Result:
no goals
-- Mathlib/Algebra/Algebra/NonUnitalSubalgebra.lean
theorem mem_sup_left {S T : NonUnitalSubalgebra R A} : ∀ {x : A}, x ∈ S → x ∈ S ⊔ T

Proof state:
R : Type u
A : Type v
inst✝⁴ : CommSemiring R
inst✝³ : NonUnitalNonAssocSemiring A
inst✝² : Module R A
inst✝¹ : IsScalarTower R A A
inst✝ : SMulCommClass R A A
S T : NonUnitalSubalgebra R A
⊢ S ≤ S ⊔ T

Tactic:
exact le_sup_left

Result:
no goals

Proof state:
R : Type u
A : Type v
inst✝⁴ : CommSemiring R
inst✝³ : NonUnitalNonAssocSemiring A
inst✝² : Module R A
inst✝¹ : IsScalarTower R A A
inst✝ : SMulCommClass R A A
S T : NonUnitalSubalgebra R A
⊢ ∀ {x : A}, x ∈ S → x ∈ S ⊔ T

Tactic:
rw [← SetLike.le_def]

Result:
R : Type u
A : Type v
inst✝⁴ : CommSemiring R
inst✝³ : NonUnitalNonAssocSemiring A
inst✝² : Module R A
inst✝¹ : IsScalarTower R A A
inst✝ : SMulCommClass R A A
S T : NonUnitalSubalgebra R A
⊢ S ≤ S ⊔ T
-- Mathlib/.lake/packages/lean4/src/lean/Std/Data/DHashMap/Internal/Raw.lean
theorem getD_eq [BEq α] [Hashable α] [LawfulBEq α] {m : Raw α β} (h : m.WF) {a : α}
    {fallback : β a} : m.getD a fallback = Raw₀.getD ⟨m, h.size_buckets_pos⟩ a fallback

Proof state:
α : Type u
β : α → Type v
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : LawfulBEq α
m : Raw α β
h : m.WF
a : α
fallback : β a
⊢ m.getD a fallback = Raw₀.getD ⟨m, ⋯⟩ a fallback

Tactic:
simp [Raw.getD, h.size_buckets_pos]

Result:
no goals
-- Mathlib/Topology/Path.lean
theorem trans_pi_eq_pi_trans (γ₀ : ∀ i, Path (as i) (bs i)) (γ₁ : ∀ i, Path (bs i) (cs i)) :
    (Path.pi γ₀).trans (Path.pi γ₁) = Path.pi fun i => (γ₀ i).trans (γ₁ i)

Proof state:
case a.h.h
ι : Type u_3
χ : ι → Type u_4
inst✝ : (i : ι) → TopologicalSpace (χ i)
as bs cs : (i : ι) → χ i
γ₀ : (i : ι) → Path (as i) (bs i)
γ₁ : (i : ι) → Path (bs i) (cs i)
t : ↑I
i : ι
⊢ (if ↑t ≤ 1 / 2 then (Path.pi γ₀).extend (2 * ↑t) else (Path.pi γ₁).extend (2 * ↑t - 1)) i =
    if ↑t ≤ 1 / 2 then (γ₀ i).extend (2 * ↑t) else (γ₁ i).extend (2 * ↑t - 1)

Tactic:
split_ifs <;> rfl

Result:
no goals

Proof state:
case a.h.h
ι : Type u_3
χ : ι → Type u_4
inst✝ : (i : ι) → TopologicalSpace (χ i)
as bs cs : (i : ι) → χ i
γ₀ : (i : ι) → Path (as i) (bs i)
γ₁ : (i : ι) → Path (bs i) (cs i)
t : ↑I
i : ι
⊢ ((Path.pi γ₀).trans (Path.pi γ₁)) t i = (Path.pi fun i => (γ₀ i).trans (γ₁ i)) t i

Tactic:
unfold Path.trans

Result:
case a.h.h
ι : Type u_3
χ : ι → Type u_4
inst✝ : (i : ι) → TopologicalSpace (χ i)
as bs cs : (i : ι) → χ i
γ₀ : (i : ι) → Path (as i) (bs i)
γ₁ : (i : ι) → Path (bs i) (cs i)
t : ↑I
i : ι
⊢ {
        toFun :=
          (fun t => if t ≤ 1 / 2 then (Path.pi γ₀).extend (2 * t) else (Path.pi γ₁).extend (2 * t - 1)) ∘ Subtype.val,
        continuous_toFun := ⋯, source' := ⋯, target' := ⋯ }
      t i =
    (Path.pi fun i =>
        { toFun := (fun t => if t ≤ 1 / 2 then (γ₀ i).extend (2 * t) else (γ₁ i).extend (2 * t - 1)) ∘ Subtype.val,
          continuous_toFun := ⋯, source' := ⋯, target' := ⋯ })
      t i

Proof state:
ι : Type u_3
χ : ι → Type u_4
inst✝ : (i : ι) → TopologicalSpace (χ i)
as bs cs : (i : ι) → χ i
γ₀ : (i : ι) → Path (as i) (bs i)
γ₁ : (i : ι) → Path (bs i) (cs i)
⊢ (Path.pi γ₀).trans (Path.pi γ₁) = Path.pi fun i => (γ₀ i).trans (γ₁ i)

Tactic:
ext t i

Result:
case a.h.h
ι : Type u_3
χ : ι → Type u_4
inst✝ : (i : ι) → TopologicalSpace (χ i)
as bs cs : (i : ι) → χ i
γ₀ : (i : ι) → Path (as i) (bs i)
γ₁ : (i : ι) → Path (bs i) (cs i)
t : ↑I
i : ι
⊢ ((Path.pi γ₀).trans (Path.pi γ₁)) t i = (Path.pi fun i => (γ₀ i).trans (γ₁ i)) t i

Proof state:
case a.h.h
ι : Type u_3
χ : ι → Type u_4
inst✝ : (i : ι) → TopologicalSpace (χ i)
as bs cs : (i : ι) → χ i
γ₀ : (i : ι) → Path (as i) (bs i)
γ₁ : (i : ι) → Path (bs i) (cs i)
t : ↑I
i : ι
⊢ {
        toFun :=
          (fun t => if t ≤ 1 / 2 then (Path.pi γ₀).extend (2 * t) else (Path.pi γ₁).extend (2 * t - 1)) ∘ Subtype.val,
        continuous_toFun := ⋯, source' := ⋯, target' := ⋯ }
      t i =
    (Path.pi fun i =>
        { toFun := (fun t => if t ≤ 1 / 2 then (γ₀ i).extend (2 * t) else (γ₁ i).extend (2 * t - 1)) ∘ Subtype.val,
          continuous_toFun := ⋯, source' := ⋯, target' := ⋯ })
      t i

Tactic:
simp only [Path.coe_mk_mk, Function.comp_apply, pi_coe]

Result:
case a.h.h
ι : Type u_3
χ : ι → Type u_4
inst✝ : (i : ι) → TopologicalSpace (χ i)
as bs cs : (i : ι) → χ i
γ₀ : (i : ι) → Path (as i) (bs i)
γ₁ : (i : ι) → Path (bs i) (cs i)
t : ↑I
i : ι
⊢ (if ↑t ≤ 1 / 2 then (Path.pi γ₀).extend (2 * ↑t) else (Path.pi γ₁).extend (2 * ↑t - 1)) i =
    if ↑t ≤ 1 / 2 then (γ₀ i).extend (2 * ↑t) else (γ₁ i).extend (2 * ↑t - 1)
-- Mathlib/Geometry/Manifold/Algebra/Monoid.lean
theorem contMDiff_pow : ∀ i : ℕ, ContMDiff I I n fun a : G => a ^ i
  | 0 => by simp only [pow_zero]; exact contMDiff_const
  | k + 1 => by simpa [pow_succ] using (contMDiff_pow _).mul contMDiff_id

Proof state:
𝕜 : Type u_1
inst✝⁷ : NontriviallyNormedField 𝕜
n : WithTop ℕ∞
H : Type u_2
inst✝⁶ : TopologicalSpace H
E : Type u_3
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace 𝕜 E
I : ModelWithCorners 𝕜 E H
G : Type u_4
inst✝³ : Monoid G
inst✝² : TopologicalSpace G
inst✝¹ : ChartedSpace H G
inst✝ : ContMDiffMul I n G
⊢ ContMDiff I I n fun a => 1

Tactic:
exact contMDiff_const

Result:
no goals

Proof state:
𝕜 : Type u_1
inst✝⁷ : NontriviallyNormedField 𝕜
n : WithTop ℕ∞
H : Type u_2
inst✝⁶ : TopologicalSpace H
E : Type u_3
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace 𝕜 E
I : ModelWithCorners 𝕜 E H
G : Type u_4
inst✝³ : Monoid G
inst✝² : TopologicalSpace G
inst✝¹ : ChartedSpace H G
inst✝ : ContMDiffMul I n G
k : ℕ
⊢ ContMDiff I I n fun a => a ^ (k + 1)

Tactic:
simpa [pow_succ] using (contMDiff_pow _).mul contMDiff_id

Result:
no goals

Proof state:
𝕜 : Type u_1
inst✝⁷ : NontriviallyNormedField 𝕜
n : WithTop ℕ∞
H : Type u_2
inst✝⁶ : TopologicalSpace H
E : Type u_3
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace 𝕜 E
I : ModelWithCorners 𝕜 E H
G : Type u_4
inst✝³ : Monoid G
inst✝² : TopologicalSpace G
inst✝¹ : ChartedSpace H G
inst✝ : ContMDiffMul I n G
⊢ ContMDiff I I n fun a => a ^ 0

Tactic:
simp only [pow_zero]

Result:
𝕜 : Type u_1
inst✝⁷ : NontriviallyNormedField 𝕜
n : WithTop ℕ∞
H : Type u_2
inst✝⁶ : TopologicalSpace H
E : Type u_3
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace 𝕜 E
I : ModelWithCorners 𝕜 E H
G : Type u_4
inst✝³ : Monoid G
inst✝² : TopologicalSpace G
inst✝¹ : ChartedSpace H G
inst✝ : ContMDiffMul I n G
⊢ ContMDiff I I n fun a => 1
-- Mathlib/Tactic/ComputeDegree.lean
theorem coeff_intCast_ite {n : ℕ} {a : ℤ} : (Int.cast a : R[X]).coeff n = ite (n = 0) a 0

Proof state:
R : Type u_1
inst✝ : Ring R
n : ℕ
a : ℤ
⊢ (↑a).coeff n = ↑(if n = 0 then a else 0)

Tactic:
simp only [← C_eq_intCast, coeff_C, Int.cast_ite, Int.cast_zero]

Result:
no goals
-- Mathlib/Data/Set/Card.lean
theorem encard_le_one_iff_subsingleton : s.encard ≤ 1 ↔ s.Subsingleton

Proof state:
α : Type u_1
s : Set α
⊢ (∀ (a b : α), a ∈ s → b ∈ s → a = b) ↔ ∀ ⦃x : α⦄, x ∈ s → ∀ ⦃y : α⦄, y ∈ s → x = y

Tactic:
tauto

Result:
no goals

Proof state:
α : Type u_1
s : Set α
⊢ s.encard ≤ 1 ↔ s.Subsingleton

Tactic:
rw [encard_le_one_iff, Set.Subsingleton]

Result:
α : Type u_1
s : Set α
⊢ (∀ (a b : α), a ∈ s → b ∈ s → a = b) ↔ ∀ ⦃x : α⦄, x ∈ s → ∀ ⦃y : α⦄, y ∈ s → x = y
-- Mathlib/Data/Nat/Size.lean
theorem lt_size_self (n : ℕ) : n < 2 ^ size n

Proof state:
n : ℕ
this : ∀ {n : ℕ}, n = 0 → n < 1 <<< n.size
⊢ n < 1 <<< n.size

Tactic:
refine binaryRec ?_ ?_ n

Result:
case refine_1
n : ℕ
this : ∀ {n : ℕ}, n = 0 → n < 1 <<< n.size
⊢ 0 < 1 <<< size 0

case refine_2
n : ℕ
this : ∀ {n : ℕ}, n = 0 → n < 1 <<< n.size
⊢ ∀ (b : Bool) (n : ℕ), n < 1 <<< n.size → bit b n < 1 <<< (bit b n).size

Proof state:
case refine_2
n✝ : ℕ
this : ∀ {n : ℕ}, n = 0 → n < 1 <<< n.size
b : Bool
n : ℕ
IH : n < 1 <<< n.size
⊢ bit b n < 1 <<< (bit b n).size

Tactic:
by_cases h : bit b n = 0

Result:
case pos
n✝ : ℕ
this : ∀ {n : ℕ}, n = 0 → n < 1 <<< n.size
b : Bool
n : ℕ
IH : n < 1 <<< n.size
h : bit b n = 0
⊢ bit b n < 1 <<< (bit b n).size

case neg
n✝ : ℕ
this : ∀ {n : ℕ}, n = 0 → n < 1 <<< n.size
b : Bool
n : ℕ
IH : n < 1 <<< n.size
h : ¬bit b n = 0
⊢ bit b n < 1 <<< (bit b n).size

Proof state:
case refine_1
n : ℕ
this : ∀ {n : ℕ}, n = 0 → n < 1 <<< n.size
⊢ 0 < 1 <<< size 0

Tactic:
apply this rfl

Result:
no goals

Proof state:
n : ℕ
⊢ n < 1 <<< n.size

Tactic:
have : ∀ {n}, n = 0 → n < 1 <<< (size n) := by simp

Result:
n : ℕ
this : ∀ {n : ℕ}, n = 0 → n < 1 <<< n.size
⊢ n < 1 <<< n.size

Proof state:
n : ℕ
⊢ ∀ {n : ℕ}, n = 0 → n < 1 <<< n.size

Tactic:
simp

Result:
no goals

Proof state:
case neg
n✝ : ℕ
this : ∀ {n : ℕ}, n = 0 → n < 1 <<< n.size
b : Bool
n : ℕ
IH : n < 1 <<< n.size
h : ¬bit b n = 0
⊢ bit b n < 1 <<< (bit b n).size

Tactic:
rw [size_bit h, shiftLeft_succ, shiftLeft_eq, one_mul]

Result:
case neg
n✝ : ℕ
this : ∀ {n : ℕ}, n = 0 → n < 1 <<< n.size
b : Bool
n : ℕ
IH : n < 1 <<< n.size
h : ¬bit b n = 0
⊢ bit b n < 2 * 2 ^ n.size

Proof state:
case neg
n✝ : ℕ
this : ∀ {n : ℕ}, n = 0 → n < 1 <<< n.size
b : Bool
n : ℕ
IH : n < 1 <<< n.size
h : ¬bit b n = 0
⊢ bit b n < 2 * 2 ^ n.size

Tactic:
cases b <;> dsimp [bit] <;> omega

Result:
no goals

Proof state:
n : ℕ
⊢ n < 2 ^ n.size

Tactic:
rw [← one_shiftLeft]

Result:
n : ℕ
⊢ n < 1 <<< n.size

Proof state:
case refine_2
n : ℕ
this : ∀ {n : ℕ}, n = 0 → n < 1 <<< n.size
⊢ ∀ (b : Bool) (n : ℕ), n < 1 <<< n.size → bit b n < 1 <<< (bit b n).size

Tactic:
intro b n IH

Result:
case refine_2
n✝ : ℕ
this : ∀ {n : ℕ}, n = 0 → n < 1 <<< n.size
b : Bool
n : ℕ
IH : n < 1 <<< n.size
⊢ bit b n < 1 <<< (bit b n).size

Proof state:
case pos
n✝ : ℕ
this : ∀ {n : ℕ}, n = 0 → n < 1 <<< n.size
b : Bool
n : ℕ
IH : n < 1 <<< n.size
h : bit b n = 0
⊢ bit b n < 1 <<< (bit b n).size

Tactic:
apply this h

Result:
no goals
-- Mathlib/Algebra/BigOperators/Finsupp.lean
theorem prod_embDomain [Zero M] [CommMonoid N] {v : α →₀ M} {f : α ↪ β} {g : β → M → N} :
    (v.embDomain f).prod g = v.prod fun a b => g (f a) b

Proof state:
α : Type u_1
β : Type u_7
M : Type u_8
N : Type u_10
inst✝¹ : Zero M
inst✝ : CommMonoid N
v : α →₀ M
f : α ↪ β
g : β → M → N
⊢ (embDomain f v).prod g = v.prod fun a b => g (f a) b

Tactic:
rw [prod, prod, support_embDomain, Finset.prod_map]

Result:
α : Type u_1
β : Type u_7
M : Type u_8
N : Type u_10
inst✝¹ : Zero M
inst✝ : CommMonoid N
v : α →₀ M
f : α ↪ β
g : β → M → N
⊢ ∏ x ∈ v.support, g (f x) ((embDomain f v) (f x)) = ∏ a ∈ v.support, g (f a) (v a)

Proof state:
α : Type u_1
β : Type u_7
M : Type u_8
N : Type u_10
inst✝¹ : Zero M
inst✝ : CommMonoid N
v : α →₀ M
f : α ↪ β
g : β → M → N
⊢ ∏ x ∈ v.support, g (f x) ((embDomain f v) (f x)) = ∏ a ∈ v.support, g (f a) (v a)

Tactic:
simp_rw [embDomain_apply]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Std/Data/DHashMap/Internal/List/Associative.lean
theorem getKeyD_insertListConst_of_mem [BEq α] [EquivBEq α]
    {l : List ((_ : α) × β)} {toInsert : List (α × β)}
    {k k' fallback : α} (k_beq : k == k')
    (distinct_l : DistinctKeys l)
    (distinct_toInsert : toInsert.Pairwise (fun a b => (a.1 == b.1) = false))
    (mem : k ∈ toInsert.map Prod.fst) :
    getKeyD k' (insertListConst l toInsert) fallback = k

Proof state:
α : Type u
β : Type v
inst✝¹ : BEq α
inst✝ : EquivBEq α
l : List ((_ : α) × β)
toInsert : List (α × β)
k k' fallback : α
k_beq : (k == k') = true
distinct_l : DistinctKeys l
distinct_toInsert : List.Pairwise (fun a b => (a.fst == b.fst) = false) toInsert
mem : k ∈ List.map Prod.fst toInsert
⊢ getKeyD k' (insertListConst l toInsert) fallback = k

Tactic:
rw [getKeyD_eq_getKey?, getKey?_insertListConst_of_mem k_beq distinct_l distinct_toInsert mem,
  Option.getD_some]

Result:
no goals
-- Mathlib/CategoryTheory/HomCongr.lean
theorem homCongr_refl {X Y : C} (f : X ⟶ Y) : (Iso.refl X).homCongr (Iso.refl Y) f = f

Proof state:
C : Type u
inst✝ : Category.{v, u} C
X Y : C
f : X ⟶ Y
⊢ ((refl X).homCongr (refl Y)) f = f

Tactic:
simp

Result:
no goals
-- Mathlib/Topology/ContinuousOn.lean
theorem ContinuousAt.congr_of_eventuallyEq (h : ContinuousAt f x) (hg : g =ᶠ[𝓝 x] f) :
    ContinuousAt g x

Proof state:
α : Type u_1
β : Type u_2
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
f g : α → β
x : α
hg : g =ᶠ[𝓝 x] f
h : ContinuousWithinAt f univ x
⊢ ContinuousWithinAt g univ x

Tactic:
exact h.congr_of_eventuallyEq_of_mem (by rwa [nhdsWithin_univ]) (mem_univ x)

Result:
no goals

Proof state:
α : Type u_1
β : Type u_2
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
f g : α → β
x : α
h : ContinuousAt f x
hg : g =ᶠ[𝓝 x] f
⊢ ContinuousAt g x

Tactic:
simp only [← continuousWithinAt_univ] at h ⊢

Result:
α : Type u_1
β : Type u_2
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
f g : α → β
x : α
hg : g =ᶠ[𝓝 x] f
h : ContinuousWithinAt f univ x
⊢ ContinuousWithinAt g univ x

Proof state:
α : Type u_1
β : Type u_2
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
f g : α → β
x : α
hg : g =ᶠ[𝓝 x] f
h : ContinuousWithinAt f univ x
⊢ g =ᶠ[𝓝[univ] x] f

Tactic:
rwa [nhdsWithin_univ]

Result:
no goals
-- Mathlib/LinearAlgebra/Prod.lean
theorem snd_map_fst : (Submodule.snd R M M₂).map (LinearMap.fst R M M₂) = ⊥

Proof state:
R : Type u
M : Type v
M₂ : Type w
inst✝⁴ : Semiring R
inst✝³ : AddCommMonoid M
inst✝² : AddCommMonoid M₂
inst✝¹ : Module R M
inst✝ : Module R M₂
⊢ map (LinearMap.fst R M M₂) (snd R M M₂) ≤ ⊥

Tactic:
intro x

Result:
R : Type u
M : Type v
M₂ : Type w
inst✝⁴ : Semiring R
inst✝³ : AddCommMonoid M
inst✝² : AddCommMonoid M₂
inst✝¹ : Module R M
inst✝ : Module R M₂
x : M
⊢ x ∈ map (LinearMap.fst R M M₂) (snd R M M₂) → x ∈ ⊥

Proof state:
R : Type u
M : Type v
M₂ : Type w
inst✝⁴ : Semiring R
inst✝³ : AddCommMonoid M
inst✝² : AddCommMonoid M₂
inst✝¹ : Module R M
inst✝ : Module R M₂
x : M
⊢ x ∈ map (LinearMap.fst R M M₂) (snd R M M₂) → x ∈ ⊥

Tactic:
simp only [snd, comap_bot, mem_map, mem_ker, fst_apply, eq_comm, Prod.exists, exists_eq_left,
  exists_const, mem_bot, imp_self]

Result:
no goals

Proof state:
R : Type u
M : Type v
M₂ : Type w
inst✝⁴ : Semiring R
inst✝³ : AddCommMonoid M
inst✝² : AddCommMonoid M₂
inst✝¹ : Module R M
inst✝ : Module R M₂
⊢ map (LinearMap.fst R M M₂) (snd R M M₂) = ⊥

Tactic:
rw [eq_bot_iff]

Result:
R : Type u
M : Type v
M₂ : Type w
inst✝⁴ : Semiring R
inst✝³ : AddCommMonoid M
inst✝² : AddCommMonoid M₂
inst✝¹ : Module R M
inst✝ : Module R M₂
⊢ map (LinearMap.fst R M M₂) (snd R M M₂) ≤ ⊥
-- Mathlib/Data/Matroid/Dual.lean
theorem IsBase.compl_isBase_dual (h : M.IsBase B) : M✶.IsBase (M.E \ B)

Proof state:
α : Type u_1
M : Matroid α
B : Set α
h : M.IsBase B
⊢ M✶.IsBase (M.E \ B)

Tactic:
rwa [dual_isBase_iff, diff_diff_cancel_left h.subset_ground]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Std/Data/DHashMap/Internal/List/Associative.lean
theorem getKey?_insertListIfNewUnit_of_contains [BEq α] [EquivBEq α]
    {l : List ((_ : α) × Unit)} {toInsert : List α}
    {k : α}
    (h : containsKey k l = true):
    getKey? k (insertListIfNewUnit l toInsert) = getKey? k l

Proof state:
α : Type u
inst✝¹ : BEq α
inst✝ : EquivBEq α
l : List ((_ : α) × Unit)
toInsert : List α
k : α
h : (getEntry? k l).isSome = true
⊢ getKey? k (insertListIfNewUnit l toInsert) = getKey? k l

Tactic:
simp [getKey?_eq_getEntry?, getEntry?_insertListIfNewUnit, Option.or_of_isSome h]

Result:
no goals

Proof state:
α : Type u
inst✝¹ : BEq α
inst✝ : EquivBEq α
l : List ((_ : α) × Unit)
toInsert : List α
k : α
h : containsKey k l = true
⊢ getKey? k (insertListIfNewUnit l toInsert) = getKey? k l

Tactic:
rw [containsKey_eq_isSome_getEntry?] at h

Result:
α : Type u
inst✝¹ : BEq α
inst✝ : EquivBEq α
l : List ((_ : α) × Unit)
toInsert : List α
k : α
h : (getEntry? k l).isSome = true
⊢ getKey? k (insertListIfNewUnit l toInsert) = getKey? k l
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Int/DivModLemmas.lean
theorem add_mul_emod_self_left (a b c : Int) : (a + b * c) % b = a % b

Proof state:
a b c : Int
⊢ (a + b * c) % b = a % b

Tactic:
rw [Int.mul_comm, Int.add_mul_emod_self]

Result:
no goals
-- Mathlib/ModelTheory/Satisfiability.lean
theorem ModelsBoundedFormula.realize_formula {φ : L.Formula α} (h : T ⊨ᵇ φ) (M : Type*)
    [L.Structure M] [M ⊨ T] [Nonempty M] {v : α → M} : φ.Realize v

Proof state:
L : Language
T : L.Theory
α : Type w
φ : L.Formula α
h : (L.lhomWithConstants α).onTheory T ⊨ᵇ Formula.equivSentence φ
M : Type u_1
inst✝² : L.Structure M
inst✝¹ : M ⊨ T
inst✝ : Nonempty M
v : α → M
this : (constantsOn α).Structure M := constantsOn.structure v
⊢ φ.Realize v

Tactic:
have : M ⊨ (L.lhomWithConstants α).onTheory T := (LHom.onTheory_model _ _).2 inferInstance

Result:
L : Language
T : L.Theory
α : Type w
φ : L.Formula α
h : (L.lhomWithConstants α).onTheory T ⊨ᵇ Formula.equivSentence φ
M : Type u_1
inst✝² : L.Structure M
inst✝¹ : M ⊨ T
inst✝ : Nonempty M
v : α → M
this✝ : (constantsOn α).Structure M := constantsOn.structure v
this : M ⊨ (L.lhomWithConstants α).onTheory T
⊢ φ.Realize v

Proof state:
L : Language
T : L.Theory
α : Type w
φ : L.Formula α
h : (L.lhomWithConstants α).onTheory T ⊨ᵇ Formula.equivSentence φ
M : Type u_1
inst✝² : L.Structure M
inst✝¹ : M ⊨ T
inst✝ : Nonempty M
v : α → M
this✝ : (constantsOn α).Structure M := constantsOn.structure v
this : M ⊨ (L.lhomWithConstants α).onTheory T
⊢ φ.Realize v

Tactic:
exact (Formula.realize_equivSentence _ _).1 (h.realize_sentence M)

Result:
no goals

Proof state:
L : Language
T : L.Theory
α : Type w
φ : L.Formula α
h : T ⊨ᵇ φ
M : Type u_1
inst✝² : L.Structure M
inst✝¹ : M ⊨ T
inst✝ : Nonempty M
v : α → M
⊢ φ.Realize v

Tactic:
rw [models_formula_iff_onTheory_models_equivSentence] at h

Result:
L : Language
T : L.Theory
α : Type w
φ : L.Formula α
h : (L.lhomWithConstants α).onTheory T ⊨ᵇ Formula.equivSentence φ
M : Type u_1
inst✝² : L.Structure M
inst✝¹ : M ⊨ T
inst✝ : Nonempty M
v : α → M
⊢ φ.Realize v

Proof state:
L : Language
T : L.Theory
α : Type w
φ : L.Formula α
h : (L.lhomWithConstants α).onTheory T ⊨ᵇ Formula.equivSentence φ
M : Type u_1
inst✝² : L.Structure M
inst✝¹ : M ⊨ T
inst✝ : Nonempty M
v : α → M
⊢ φ.Realize v

Tactic:
letI : (constantsOn α).Structure M := constantsOn.structure v

Result:
L : Language
T : L.Theory
α : Type w
φ : L.Formula α
h : (L.lhomWithConstants α).onTheory T ⊨ᵇ Formula.equivSentence φ
M : Type u_1
inst✝² : L.Structure M
inst✝¹ : M ⊨ T
inst✝ : Nonempty M
v : α → M
this : (constantsOn α).Structure M := constantsOn.structure v
⊢ φ.Realize v
-- Mathlib/GroupTheory/Finiteness.lean
theorem Group.rank_le_of_surjective [Group.FG G] [Group.FG G'] (f : G →* G')
    (hf : Function.Surjective f) : Group.rank G' ≤ Group.rank G

Proof state:
case intro.intro
G : Type u_3
inst✝³ : Group G
G' : Type u_5
inst✝² : Group G'
inst✝¹ : FG G
inst✝ : FG G'
f : G →* G'
hf : Function.Surjective ⇑f
S : Finset G
hS1 : S.card = rank G
hS2 : Subgroup.closure ↑S = ⊤
⊢ rank G' ≤ rank G

Tactic:
trans (S.image f).card

Result:
G : Type u_3
inst✝³ : Group G
G' : Type u_5
inst✝² : Group G'
inst✝¹ : FG G
inst✝ : FG G'
f : G →* G'
hf : Function.Surjective ⇑f
S : Finset G
hS1 : S.card = rank G
hS2 : Subgroup.closure ↑S = ⊤
⊢ rank G' ≤ (Finset.image (⇑f) S).card

G : Type u_3
inst✝³ : Group G
G' : Type u_5
inst✝² : Group G'
inst✝¹ : FG G
inst✝ : FG G'
f : G →* G'
hf : Function.Surjective ⇑f
S : Finset G
hS1 : S.card = rank G
hS2 : Subgroup.closure ↑S = ⊤
⊢ (Finset.image (⇑f) S).card ≤ rank G

Proof state:
G : Type u_3
inst✝³ : Group G
G' : Type u_5
inst✝² : Group G'
inst✝¹ : FG G
inst✝ : FG G'
f : G →* G'
hf : Function.Surjective ⇑f
S : Finset G
hS1 : S.card = rank G
hS2 : Subgroup.closure ↑S = ⊤
⊢ rank G' ≤ (Finset.image (⇑f) S).card

Tactic:
apply Group.rank_le

Result:
case hS
G : Type u_3
inst✝³ : Group G
G' : Type u_5
inst✝² : Group G'
inst✝¹ : FG G
inst✝ : FG G'
f : G →* G'
hf : Function.Surjective ⇑f
S : Finset G
hS1 : S.card = rank G
hS2 : Subgroup.closure ↑S = ⊤
⊢ Subgroup.closure ↑(Finset.image (⇑f) S) = ⊤

Proof state:
G : Type u_3
inst✝³ : Group G
G' : Type u_5
inst✝² : Group G'
inst✝¹ : FG G
inst✝ : FG G'
f : G →* G'
hf : Function.Surjective ⇑f
⊢ rank G' ≤ rank G

Tactic:
obtain ⟨S, hS1, hS2⟩ := Group.rank_spec G

Result:
case intro.intro
G : Type u_3
inst✝³ : Group G
G' : Type u_5
inst✝² : Group G'
inst✝¹ : FG G
inst✝ : FG G'
f : G →* G'
hf : Function.Surjective ⇑f
S : Finset G
hS1 : S.card = rank G
hS2 : Subgroup.closure ↑S = ⊤
⊢ rank G' ≤ rank G

Proof state:
G : Type u_3
inst✝³ : Group G
G' : Type u_5
inst✝² : Group G'
inst✝¹ : FG G
inst✝ : FG G'
f : G →* G'
hf : Function.Surjective ⇑f
S : Finset G
hS1 : S.card = rank G
hS2 : Subgroup.closure ↑S = ⊤
⊢ (Finset.image (⇑f) S).card ≤ rank G

Tactic:
exact Finset.card_image_le.trans_eq hS1

Result:
no goals

Proof state:
case hS
G : Type u_3
inst✝³ : Group G
G' : Type u_5
inst✝² : Group G'
inst✝¹ : FG G
inst✝ : FG G'
f : G →* G'
hf : Function.Surjective ⇑f
S : Finset G
hS1 : S.card = rank G
hS2 : Subgroup.closure ↑S = ⊤
⊢ Subgroup.closure ↑(Finset.image (⇑f) S) = ⊤

Tactic:
rw [Finset.coe_image, ← MonoidHom.map_closure, hS2, Subgroup.map_top_of_surjective f hf]

Result:
no goals