harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/SetTheory/Cardinal/Basic.lean
theorem mk_preimage_of_subset_range_lift {α : Type u} {β : Type v} (f : α → β) (s : Set β)
    (h : s ⊆ range f) : lift.{u} #s ≤ lift.{v} #(f ⁻¹' s)

Proof state:
α : Type u
β : Type v
f : α → β
s : Set β
h : f '' (f ⁻¹' s) = s
⊢ lift.{u, v} #↑s ≤ lift.{v, u} #↑(f ⁻¹' s)

Tactic:
nth_rewrite 1 [← h]

Result:
α : Type u
β : Type v
f : α → β
s : Set β
h : f '' (f ⁻¹' s) = s
⊢ lift.{u, v} #↑(f '' (f ⁻¹' s)) ≤ lift.{v, u} #↑(f ⁻¹' s)

Proof state:
α : Type u
β : Type v
f : α → β
s : Set β
h : f '' (f ⁻¹' s) = s
⊢ lift.{u, v} #↑(f '' (f ⁻¹' s)) ≤ lift.{v, u} #↑(f ⁻¹' s)

Tactic:
apply mk_image_le_lift

Result:
no goals

Proof state:
α : Type u
β : Type v
f : α → β
s : Set β
h : s ⊆ range f
⊢ lift.{u, v} #↑s ≤ lift.{v, u} #↑(f ⁻¹' s)

Tactic:
rw [← image_preimage_eq_iff] at h

Result:
α : Type u
β : Type v
f : α → β
s : Set β
h : f '' (f ⁻¹' s) = s
⊢ lift.{u, v} #↑s ≤ lift.{v, u} #↑(f ⁻¹' s)
-- Mathlib/Analysis/Asymptotics/Lemmas.lean
theorem isLittleO_pow_pow {m n : ℕ} (h : m < n) : (fun x : 𝕜 => x ^ n) =o[𝓝 0] fun x => x ^ m

Proof state:
𝕜 : Type u_15
inst✝ : NormedDivisionRing 𝕜
m p : ℕ
hp0 : 0 < p
h : m < m + p
this : (fun x => x ^ m * x ^ p) =o[𝓝 0] fun x => x ^ m * 1 ^ p
⊢ (fun x => x ^ (m + p)) =o[𝓝 0] fun x => x ^ m

Tactic:
simpa only [pow_add, one_pow, mul_one]

Result:
no goals

Proof state:
𝕜 : Type u_15
inst✝ : NormedDivisionRing 𝕜
m n : ℕ
h : m < n
⊢ (fun x => x ^ n) =o[𝓝 0] fun x => x ^ m

Tactic:
rcases lt_iff_exists_add.1 h with ⟨p, hp0 : 0 < p, rfl⟩

Result:
case intro.intro
𝕜 : Type u_15
inst✝ : NormedDivisionRing 𝕜
m p : ℕ
hp0 : 0 < p
h : m < m + p
⊢ (fun x => x ^ (m + p)) =o[𝓝 0] fun x => x ^ m

Proof state:
case intro.intro
𝕜 : Type u_15
inst✝ : NormedDivisionRing 𝕜
m p : ℕ
hp0 : 0 < p
h : m < m + p
⊢ (fun x => x ^ (m + p)) =o[𝓝 0] fun x => x ^ m

Tactic:
suffices (fun x : 𝕜 => x ^ m * x ^ p) =o[𝓝 0] fun x => x ^ m * 1 ^ p by
  simpa only [pow_add, one_pow, mul_one]

Result:
case intro.intro
𝕜 : Type u_15
inst✝ : NormedDivisionRing 𝕜
m p : ℕ
hp0 : 0 < p
h : m < m + p
⊢ (fun x => x ^ m * x ^ p) =o[𝓝 0] fun x => x ^ m * 1 ^ p

Proof state:
case intro.intro
𝕜 : Type u_15
inst✝ : NormedDivisionRing 𝕜
m p : ℕ
hp0 : 0 < p
h : m < m + p
⊢ (fun x => x ^ m * x ^ p) =o[𝓝 0] fun x => x ^ m * 1 ^ p

Tactic:
exact IsBigO.mul_isLittleO (isBigO_refl _ _)
  (IsLittleO.pow ((isLittleO_one_iff _).2 tendsto_id) hp0)

Result:
no goals
-- Mathlib/Algebra/Order/Group/Pointwise/Interval.lean
theorem preimage_const_mul_uIcc (ha : a ≠ 0) (b c : α) :
    (a * ·) ⁻¹' [[b, c]] = [[b / a, c / a]]

Proof state:
α : Type u_1
inst✝ : LinearOrderedField α
a : α
ha : a ≠ 0
b c : α
⊢ (fun x => a * x) ⁻¹' [[b, c]] = [[b / a, c / a]]

Tactic:
simp only [← preimage_mul_const_uIcc ha, mul_comm]

Result:
no goals
-- Mathlib/AlgebraicGeometry/Morphisms/UniversallyClosed.lean
lemma UniversallyClosed.of_comp_surjective {X Y Z : Scheme} (f : X ⟶ Y) (g : Y ⟶ Z)
    [UniversallyClosed (f ≫ g)] [Surjective f] : UniversallyClosed g

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

Tactic:
constructor

Result:
case out
X Y Z : Scheme
f : X ⟶ Y
g : Y ⟶ Z
inst✝¹ : UniversallyClosed (f ≫ g)
inst✝ : Surjective f
⊢ (topologically @IsClosedMap).universally g

Proof state:
case out
X Y Z : Scheme
f : X ⟶ Y
g : Y ⟶ Z
inst✝¹ : UniversallyClosed (f ≫ g)
inst✝ : Surjective f
X' Y' : Scheme
i₁ : X' ⟶ Y
i₂ : Y' ⟶ Z
f' : X' ⟶ Y'
H : IsPullback f' i₁ i₂ g
⊢ topologically (@IsClosedMap) f'

Tactic:
have := UniversallyClosed.out _ _ _ ((IsPullback.of_hasPullback i₁ f).paste_horiz H)

Result:
case out
X Y Z : Scheme
f : X ⟶ Y
g : Y ⟶ Z
inst✝¹ : UniversallyClosed (f ≫ g)
inst✝ : Surjective f
X' Y' : Scheme
i₁ : X' ⟶ Y
i₂ : Y' ⟶ Z
f' : X' ⟶ Y'
H : IsPullback f' i₁ i₂ g
this : topologically (@IsClosedMap) (pullback.fst i₁ f ≫ f')
⊢ topologically (@IsClosedMap) f'

Proof state:
case out
X Y Z : Scheme
f : X ⟶ Y
g : Y ⟶ Z
inst✝¹ : UniversallyClosed (f ≫ g)
inst✝ : Surjective f
⊢ (topologically @IsClosedMap).universally g

Tactic:
intro X' Y' i₁ i₂ f' H

Result:
case out
X Y Z : Scheme
f : X ⟶ Y
g : Y ⟶ Z
inst✝¹ : UniversallyClosed (f ≫ g)
inst✝ : Surjective f
X' Y' : Scheme
i₁ : X' ⟶ Y
i₂ : Y' ⟶ Z
f' : X' ⟶ Y'
H : IsPullback f' i₁ i₂ g
⊢ topologically (@IsClosedMap) f'

Proof state:
case out
X Y Z : Scheme
f : X ⟶ Y
g : Y ⟶ Z
inst✝¹ : UniversallyClosed (f ≫ g)
inst✝ : Surjective f
X' Y' : Scheme
i₁ : X' ⟶ Y
i₂ : Y' ⟶ Z
f' : X' ⟶ Y'
H : IsPullback f' i₁ i₂ g
this : topologically (@IsClosedMap) (pullback.fst i₁ f ≫ f')
⊢ topologically (@IsClosedMap) f'

Tactic:
exact IsClosedMap.of_comp_surjective (MorphismProperty.pullback_fst (P := @Surjective) _ _ ‹_›).1
  (Scheme.Hom.continuous _) this

Result:
no goals
-- Mathlib/Data/List/Basic.lean
theorem map_injective_iff {f : α → β} : Injective (map f) ↔ Injective f

Proof state:
α : Type u
β : Type v
f : α → β
h : Injective (map f)
x y : α
hxy : f x = f y
⊢ [x] = [y]

Tactic:
apply h

Result:
case a
α : Type u
β : Type v
f : α → β
h : Injective (map f)
x y : α
hxy : f x = f y
⊢ map f [x] = map f [y]

Proof state:
α : Type u
β : Type v
f : α → β
h : Injective (map f)
x y : α
hxy : f x = f y
this : [x] = [y]
⊢ x = y

Tactic:
simpa using this

Result:
no goals

Proof state:
case a
α : Type u
β : Type v
f : α → β
h : Injective (map f)
x y : α
hxy : f x = f y
⊢ map f [x] = map f [y]

Tactic:
simp [hxy]

Result:
no goals

Proof state:
α : Type u
β : Type v
f : α → β
h : Injective (map f)
x y : α
hxy : f x = f y
⊢ x = y

Tactic:
suffices [x] = [y] by simpa using this

Result:
α : Type u
β : Type v
f : α → β
h : Injective (map f)
x y : α
hxy : f x = f y
⊢ [x] = [y]
-- Mathlib/NumberTheory/FactorisationProperties.lean
theorem abundant_twelve : Abundant 12

Proof state:
⊢ properDivisors 12 = {1, 2, 3, 4, 6}

Tactic:
rfl

Result:
no goals

Proof state:
⊢ Abundant 12

Tactic:
rw [Abundant, show properDivisors 12 = {1,2,3,4,6} by rfl]

Result:
⊢ 12 < ∑ i ∈ {1, 2, 3, 4, 6}, i

Proof state:
⊢ 12 < ∑ i ∈ {1, 2, 3, 4, 6}, i

Tactic:
norm_num

Result:
no goals
-- Mathlib/Data/Nat/Squarefree.lean
lemma primeFactors_div_gcd (hm : Squarefree m) (hn : n ≠ 0) :
    primeFactors (m / m.gcd n) = primeFactors m \ primeFactors n

Proof state:
case h
m n : ℕ
hm : Squarefree m
hn : n ≠ 0
p : ℕ
this : m / m.gcd n ≠ 0
hp : (Prime p ∧ p ∣ m) ∧ (Prime p → ¬p ∣ n)
⊢ (m.gcd n).Coprime p

Tactic:
rw [coprime_comm, hp.1.1.coprime_iff_not_dvd]

Result:
case h
m n : ℕ
hm : Squarefree m
hn : n ≠ 0
p : ℕ
this : m / m.gcd n ≠ 0
hp : (Prime p ∧ p ∣ m) ∧ (Prime p → ¬p ∣ n)
⊢ ¬p ∣ m.gcd n

Proof state:
case h
m n : ℕ
hm : Squarefree m
hn : n ≠ 0
p : ℕ
⊢ p ∈ (m / m.gcd n).primeFactors ↔ p ∈ m.primeFactors \ n.primeFactors

Tactic:
have : m / m.gcd n ≠ 0 := by simp [gcd_ne_zero_right hn, gcd_le_left _ hm.ne_zero.bot_lt]

Result:
case h
m n : ℕ
hm : Squarefree m
hn : n ≠ 0
p : ℕ
this : m / m.gcd n ≠ 0
⊢ p ∈ (m / m.gcd n).primeFactors ↔ p ∈ m.primeFactors \ n.primeFactors

Proof state:
m n : ℕ
hm : Squarefree m
hn : n ≠ 0
p : ℕ
⊢ m / m.gcd n ≠ 0

Tactic:
simp [gcd_ne_zero_right hn, gcd_le_left _ hm.ne_zero.bot_lt]

Result:
no goals

Proof state:
m n : ℕ
hm : Squarefree m
hn : n ≠ 0
⊢ (m / m.gcd n).primeFactors = m.primeFactors \ n.primeFactors

Tactic:
ext p

Result:
case h
m n : ℕ
hm : Squarefree m
hn : n ≠ 0
p : ℕ
⊢ p ∈ (m / m.gcd n).primeFactors ↔ p ∈ m.primeFactors \ n.primeFactors

Proof state:
case h
m n : ℕ
hm : Squarefree m
hn : n ≠ 0
p : ℕ
this : m / m.gcd n ≠ 0
⊢ p ∈ (m / m.gcd n).primeFactors ↔ p ∈ m.primeFactors \ n.primeFactors

Tactic:
simp only [mem_primeFactors, ne_eq, this, not_false_eq_true, and_true, not_and, mem_sdiff,
  hm.ne_zero, hn, dvd_div_iff_mul_dvd (gcd_dvd_left _ _)]

Result:
case h
m n : ℕ
hm : Squarefree m
hn : n ≠ 0
p : ℕ
this : m / m.gcd n ≠ 0
⊢ Prime p ∧ m.gcd n * p ∣ m ↔ (Prime p ∧ p ∣ m) ∧ (Prime p → ¬p ∣ n)

Proof state:
case h
m n : ℕ
hm : Squarefree m
hn : n ≠ 0
p : ℕ
this : m / m.gcd n ≠ 0
hp : (Prime p ∧ p ∣ m) ∧ (Prime p → ¬p ∣ n)
⊢ ¬p ∣ m.gcd n

Tactic:
exact fun hpn ↦ hp.2 hp.1.1 <| hpn.trans <| gcd_dvd_right _ _

Result:
no goals

Proof state:
case h
m n : ℕ
hm : Squarefree m
hn : n ≠ 0
p : ℕ
this : m / m.gcd n ≠ 0
⊢ Prime p ∧ m.gcd n * p ∣ m ↔ (Prime p ∧ p ∣ m) ∧ (Prime p → ¬p ∣ n)

Tactic:
refine ⟨fun hp ↦ ⟨⟨hp.1, dvd_of_mul_left_dvd hp.2⟩, fun _ hpn ↦ hp.1.not_unit <| hm _ <|
  (mul_dvd_mul_right (dvd_gcd (dvd_of_mul_left_dvd hp.2) hpn) _).trans hp.2⟩, fun hp ↦
    ⟨hp.1.1, Coprime.mul_dvd_of_dvd_of_dvd ?_ (gcd_dvd_left _ _) hp.1.2⟩⟩

Result:
case h
m n : ℕ
hm : Squarefree m
hn : n ≠ 0
p : ℕ
this : m / m.gcd n ≠ 0
hp : (Prime p ∧ p ∣ m) ∧ (Prime p → ¬p ∣ n)
⊢ (m.gcd n).Coprime p
-- Mathlib/.lake/packages/lean4/src/lean/Std/Data/DHashMap/Internal/RawLemmas.lean
theorem getD_eq_fallback [LawfulBEq α] (h : m.1.WF) {a : α} {fallback : β a} :
    m.contains a = false → m.getD a fallback = fallback

Proof state:
α : Type u
β : α → Type v
m : Raw₀ α β
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : LawfulBEq α
h : m.val.WF
a : α
fallback : β a
⊢ m.contains a = false → m.getD a fallback = fallback

Tactic:
simp_to_model using List.getValueCastD_eq_fallback

Result:
no goals
-- Mathlib/Algebra/Homology/HomotopyCategory/HomComplexShift.lean
@[simp]
lemma leftShift_units_smul (a n' : ℤ) (hn' : n + a = n') (x : Rˣ) :
    (x • γ).leftShift a n' hn' = x • γ.leftShift a n' hn'

Proof state:
C : Type u
inst✝³ : Category.{v, u} C
inst✝² : Preadditive C
R : Type u_1
inst✝¹ : Ring R
inst✝ : Linear R C
K L : CochainComplex C ℤ
n : ℤ
γ : Cochain K L n
a n' : ℤ
hn' : n + a = n'
x : Rˣ
⊢ (x • γ).leftShift a n' hn' = x • γ.leftShift a n' hn'

Tactic:
apply leftShift_smul

Result:
no goals
-- Mathlib/CategoryTheory/Limits/MonoCoprod.lean
theorem binaryCofan_inr {A B : C} [MonoCoprod C] (c : BinaryCofan A B) (hc : IsColimit c) :
    Mono c.inr

Proof state:
C : Type u_1
inst✝¹ : Category.{u_2, u_1} C
A B : C
inst✝ : MonoCoprod C
c : BinaryCofan A B
hc : IsColimit c
T✝ : C
f₁ : (pair A B).obj { as := WalkingPair.right } ⟶ T✝
f₂ : (pair A B).obj { as := WalkingPair.left } ⟶ T✝
m : (BinaryCofan.mk c.inr c.inl).pt ⟶ T✝
h₁ : (BinaryCofan.mk c.inr c.inl).inl ≫ m = f₁
h₂ : (BinaryCofan.mk c.inr c.inl).inr ≫ m = f₂
⊢ c.inl ≫ m = c.inl ≫ (fun {T} f₁ f₂ => hc.desc (BinaryCofan.mk f₂ f₁)) f₁ f₂

Tactic:
aesop_cat

Result:
no goals

Proof state:
C : Type u_1
inst✝¹ : Category.{u_2, u_1} C
A B : C
inst✝ : MonoCoprod C
c : BinaryCofan A B
hc : IsColimit c
hc' : IsColimit (BinaryCofan.mk c.inr c.inl)
⊢ Mono c.inr

Tactic:
exact binaryCofan_inl _ hc'

Result:
no goals

Proof state:
C : Type u_1
inst✝¹ : Category.{u_2, u_1} C
A B : C
inst✝ : MonoCoprod C
c : BinaryCofan A B
hc : IsColimit c
⊢ ∀ {T : C} (f : (pair A B).obj { as := WalkingPair.right } ⟶ T) (g : (pair A B).obj { as := WalkingPair.left } ⟶ T),
    (BinaryCofan.mk c.inr c.inl).inr ≫ (fun {T} f₁ f₂ => hc.desc (BinaryCofan.mk f₂ f₁)) f g = g

Tactic:
simp

Result:
no goals

Proof state:
C : Type u_1
inst✝¹ : Category.{u_2, u_1} C
A B : C
inst✝ : MonoCoprod C
c : BinaryCofan A B
hc : IsColimit c
⊢ Mono c.inr

Tactic:
haveI hc' : IsColimit (BinaryCofan.mk c.inr c.inl) :=
  BinaryCofan.IsColimit.mk _ (fun f₁ f₂ => hc.desc (BinaryCofan.mk f₂ f₁))
    (by simp) (by simp)
    (fun f₁ f₂ m h₁ h₂ => BinaryCofan.IsColimit.hom_ext hc (by aesop_cat) (by aesop_cat))

Result:
C : Type u_1
inst✝¹ : Category.{u_2, u_1} C
A B : C
inst✝ : MonoCoprod C
c : BinaryCofan A B
hc : IsColimit c
hc' : IsColimit (BinaryCofan.mk c.inr c.inl)
⊢ Mono c.inr

Proof state:
C : Type u_1
inst✝¹ : Category.{u_2, u_1} C
A B : C
inst✝ : MonoCoprod C
c : BinaryCofan A B
hc : IsColimit c
⊢ ∀ {T : C} (f : (pair A B).obj { as := WalkingPair.right } ⟶ T) (g : (pair A B).obj { as := WalkingPair.left } ⟶ T),
    (BinaryCofan.mk c.inr c.inl).inl ≫ (fun {T} f₁ f₂ => hc.desc (BinaryCofan.mk f₂ f₁)) f g = f

Tactic:
simp

Result:
no goals

Proof state:
C : Type u_1
inst✝¹ : Category.{u_2, u_1} C
A B : C
inst✝ : MonoCoprod C
c : BinaryCofan A B
hc : IsColimit c
T✝ : C
f₁ : (pair A B).obj { as := WalkingPair.right } ⟶ T✝
f₂ : (pair A B).obj { as := WalkingPair.left } ⟶ T✝
m : (BinaryCofan.mk c.inr c.inl).pt ⟶ T✝
h₁ : (BinaryCofan.mk c.inr c.inl).inl ≫ m = f₁
h₂ : (BinaryCofan.mk c.inr c.inl).inr ≫ m = f₂
⊢ c.inr ≫ m = c.inr ≫ (fun {T} f₁ f₂ => hc.desc (BinaryCofan.mk f₂ f₁)) f₁ f₂

Tactic:
aesop_cat

Result:
no goals
-- Mathlib/Algebra/MonoidAlgebra/ToDirectSum.lean
theorem AddMonoidAlgebra.toDirectSum_pow [DecidableEq ι] [AddMonoid ι] [Semiring M]
    (f : AddMonoidAlgebra M ι) (n : ℕ) :
    (f ^ n).toDirectSum = f.toDirectSum ^ n

Proof state:
ι : Type u_1
M : Type u_3
inst✝² : DecidableEq ι
inst✝¹ : AddMonoid ι
inst✝ : Semiring M
f : M[ι]
n : ℕ
⊢ (f ^ n).toDirectSum = f.toDirectSum ^ n

Tactic:
exact map_pow addMonoidAlgebraRingEquivDirectSum f n

Result:
no goals

Proof state:
ι : Type u_1
M : Type u_3
inst✝² : DecidableEq ι
inst✝¹ : AddMonoid ι
inst✝ : Semiring M
f : M[ι]
n : ℕ
⊢ (f ^ n).toDirectSum = f.toDirectSum ^ n

Tactic:
classical exact map_pow addMonoidAlgebraRingEquivDirectSum f n

Result:
no goals
-- Mathlib/Data/List/NatAntidiagonal.lean
theorem antidiagonal_succ_succ' {n : ℕ} :
    antidiagonal (n + 2) =
      (0, n + 2) :: (antidiagonal n).map (Prod.map Nat.succ Nat.succ) ++ [(n + 2, 0)]

Proof state:
n : ℕ
⊢ antidiagonal (n + 2) = (0, n + 2) :: map (Prod.map succ succ) (antidiagonal n) ++ [(n + 2, 0)]

Tactic:
rw [antidiagonal_succ']

Result:
n : ℕ
⊢ map (Prod.map id succ) (antidiagonal (n + 1)) ++ [(n + 1 + 1, 0)] =
    (0, n + 2) :: map (Prod.map succ succ) (antidiagonal n) ++ [(n + 2, 0)]

Proof state:
n : ℕ
⊢ map (Prod.map id succ) (antidiagonal (n + 1)) ++ [(n + 1 + 1, 0)] =
    (0, n + 2) :: map (Prod.map succ succ) (antidiagonal n) ++ [(n + 2, 0)]

Tactic:
simp only [antidiagonal_succ, map_cons, Prod.map_apply, id_eq, map_map, cons_append, cons.injEq,
  append_cancel_right_eq, true_and]

Result:
n : ℕ
⊢ map (Prod.map id succ ∘ Prod.map succ id) (antidiagonal n) = map (Prod.map succ succ) (antidiagonal n)

Proof state:
case h.a
n i✝ : ℕ
a✝ : ℕ × ℕ
⊢ a✝ ∈ (map (Prod.map id succ ∘ Prod.map succ id) (antidiagonal n))[i✝]? ↔
    a✝ ∈ (map (Prod.map succ succ) (antidiagonal n))[i✝]?

Tactic:
simp

Result:
no goals

Proof state:
n : ℕ
⊢ map (Prod.map id succ ∘ Prod.map succ id) (antidiagonal n) = map (Prod.map succ succ) (antidiagonal n)

Tactic:
ext

Result:
case h.a
n i✝ : ℕ
a✝ : ℕ × ℕ
⊢ a✝ ∈ (map (Prod.map id succ ∘ Prod.map succ id) (antidiagonal n))[i✝]? ↔
    a✝ ∈ (map (Prod.map succ succ) (antidiagonal n))[i✝]?
-- Mathlib/SetTheory/Ordinal/Notation.lean
theorem NFBelow.lt {e n a b} (h : NFBelow (ONote.oadd e n a) b) : repr e < b

Proof state:
e : ONote
n : ℕ+
a : ONote
b : Ordinal.{0}
h : (e.oadd n a).NFBelow b
⊢ e.repr < b

Tactic:
obtain - | ⟨h₁, h₂, h₃⟩ := h

Result:
case oadd'
e : ONote
n : ℕ+
a : ONote
b eb✝ : Ordinal.{0}
h₁ : e.NFBelow eb✝
h₂ : a.NFBelow e.repr
h₃ : e.repr < b
⊢ e.repr < b

Proof state:
case oadd'
e : ONote
n : ℕ+
a : ONote
b eb✝ : Ordinal.{0}
h₁ : e.NFBelow eb✝
h₂ : a.NFBelow e.repr
h₃ : e.repr < b
⊢ e.repr < b

Tactic:
exact h₃

Result:
no goals
-- Mathlib/FieldTheory/IntermediateField/Adjoin/Basic.lean
theorem adjoin.finrank {x : L} (hx : IsIntegral K x) :
    Module.finrank K K⟮x⟯ = (minpoly K x).natDegree

Proof state:
K : Type u
inst✝² : Field K
L : Type u_3
inst✝¹ : Field L
inst✝ : Algebra K L
x : L
hx : IsIntegral K x
⊢ (powerBasis hx).dim = (minpoly K x).natDegree

Tactic:
rfl

Result:
no goals

Proof state:
K : Type u
inst✝² : Field K
L : Type u_3
inst✝¹ : Field L
inst✝ : Algebra K L
x : L
hx : IsIntegral K x
⊢ Module.finrank K ↥K⟮x⟯ = (minpoly K x).natDegree

Tactic:
rw [PowerBasis.finrank (adjoin.powerBasis hx :)]

Result:
K : Type u
inst✝² : Field K
L : Type u_3
inst✝¹ : Field L
inst✝ : Algebra K L
x : L
hx : IsIntegral K x
⊢ (powerBasis hx).dim = (minpoly K x).natDegree
-- Mathlib/Data/Nat/ModEq.lean
/-- A common factor that's coprime with the modulus can be cancelled from a `ModEq` -/
lemma cancel_right_of_coprime (hmc : gcd m c = 1) (h : a * c ≡ b * c [MOD m]) : a ≡ b [MOD m] :=
  cancel_left_of_coprime hmc <| by simpa [mul_comm] using h

Proof state:
m a b c : ℕ
hmc : m.gcd c = 1
h : a * c ≡ b * c [MOD m]
⊢ c * a ≡ c * b [MOD m]

Tactic:
simpa [mul_comm] using h

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Std/Data/DHashMap/RawLemmas.lean
theorem get?_eq_some_get!_of_contains [LawfulBEq α] (h : m.WF) {a : α} [Inhabited (β a)] :
    m.contains a = true → m.get? a = some (m.get! a)

Proof state:
α : Type u
β : α → Type v
m : Raw α β
inst✝³ : BEq α
inst✝² : Hashable α
inst✝¹ : LawfulBEq α
h : m.WF
a : α
inst✝ : Inhabited (β a)
⊢ m.contains a = true → m.get? a = some (m.get! a)

Tactic:
simp_to_raw using Raw₀.get?_eq_some_get!

Result:
no goals
-- Mathlib/Combinatorics/Additive/FreimanHom.lean
@[to_additive] lemma isMulFreimanHom_id (hA : A₁ ⊆ A₂) : IsMulFreimanHom n A₁ A₂ id where
  mapsTo := hA
  map_prod_eq_map_prod s t _ _ _ _ h

Proof state:
α : Type u_2
inst✝ : CommMonoid α
A₁ A₂ : Set α
n : ℕ
hA : A₁ ⊆ A₂
s t : Multiset α
x✝³ : ∀ ⦃x : α⦄, x ∈ s → x ∈ A₁
x✝² : ∀ ⦃x : α⦄, x ∈ t → x ∈ A₁
x✝¹ : s.card = n
x✝ : t.card = n
h : s.prod = t.prod
⊢ (map id s).prod = (map id t).prod

Tactic:
simpa using h

Result:
no goals
-- Mathlib/NumberTheory/ModularForms/SlashActions.lean
theorem is_invariant_const (A : SL(2, ℤ)) (x : ℂ) :
    Function.const ℍ x ∣[(0 : ℤ)] A = Function.const ℍ x

Proof state:
case h
A : SL(2, ℤ)
x : ℂ
x✝ : ℍ
⊢ (Function.const ℍ x ∣[0] A) x✝ = Function.const ℍ x x✝

Tactic:
simp only [SL_slash, slash_def, slash, Function.const_apply, det_coe, ofReal_one, zero_sub,
  zpow_neg, zpow_one, inv_one, mul_one, neg_zero, zpow_zero]

Result:
no goals

Proof state:
A : SL(2, ℤ)
x : ℂ
⊢ Function.const ℍ x ∣[0] A = Function.const ℍ x

Tactic:
funext

Result:
case h
A : SL(2, ℤ)
x : ℂ
x✝ : ℍ
⊢ (Function.const ℍ x ∣[0] A) x✝ = Function.const ℍ x x✝
-- Mathlib/Data/Fin/Basic.lean
protected lemma eq_or_lt_of_le : a ≤ b → a = b ∨ a < b

Proof state:
n : ℕ
a b : Fin n
⊢ a ≤ b → ↑a = ↑b ∨ a < b

Tactic:
exact Nat.eq_or_lt_of_le

Result:
no goals

Proof state:
n : ℕ
a b : Fin n
⊢ a ≤ b → a = b ∨ a < b

Tactic:
rw [Fin.ext_iff]

Result:
n : ℕ
a b : Fin n
⊢ a ≤ b → ↑a = ↑b ∨ a < b
-- Mathlib/Order/Interval/Finset/Basic.lean
theorem Ioc_erase_right (a b : α) : (Ioc a b).erase b = Ioo a b

Proof state:
α : Type u_2
inst✝² : PartialOrder α
inst✝¹ : LocallyFiniteOrder α
inst✝ : DecidableEq α
a b : α
⊢ (Ioc a b).erase b = Ioo a b

Tactic:
simp [← coe_inj]

Result:
no goals
-- Mathlib/MeasureTheory/Integral/Average.lean
theorem lintegral_laverage (μ : Measure α) [IsFiniteMeasure μ] (f : α → ℝ≥0∞) :
    ∫⁻ _x, ⨍⁻ a, f a ∂μ ∂μ = ∫⁻ x, f x ∂μ

Proof state:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
inst✝ : IsFiniteMeasure μ
f : α → ℝ≥0∞
⊢ ∫⁻ (_x : α), ⨍⁻ (a : α), f a ∂μ ∂μ = ∫⁻ (x : α), f x ∂μ

Tactic:
simp

Result:
no goals
-- Mathlib/GroupTheory/FreeGroup/Reduce.lean
theorem reduce_toWord : ∀ x : FreeGroup α, reduce (toWord x) = toWord x

Proof state:
α : Type u_1
inst✝ : DecidableEq α
⊢ ∀ (x : FreeGroup α), reduce x.toWord = x.toWord

Tactic:
rintro ⟨L⟩

Result:
case mk
α : Type u_1
inst✝ : DecidableEq α
x✝ : FreeGroup α
L : List (α × Bool)
⊢ reduce (toWord (Quot.mk Red.Step L)) = toWord (Quot.mk Red.Step L)

Proof state:
case mk
α : Type u_1
inst✝ : DecidableEq α
x✝ : FreeGroup α
L : List (α × Bool)
⊢ reduce (toWord (Quot.mk Red.Step L)) = toWord (Quot.mk Red.Step L)

Tactic:
exact reduce.idem

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/BitVec/Bitblast.lean
theorem getLsbD_add {i : Nat} (i_lt : i < w) (x y : BitVec w) :
    getLsbD (x + y) i =
      (getLsbD x i ^^ (getLsbD y i ^^ carry i x y false))

Proof state:
w i : Nat
i_lt : i < w
x y : BitVec w
⊢ (x + y).getLsbD i = (x.getLsbD i ^^ (y.getLsbD i ^^ carry i x y false))

Tactic:
simpa using getLsbD_add_add_bool i_lt x y false

Result:
no goals
-- Mathlib/MeasureTheory/Function/LpSpace/Basic.lean
theorem norm_indicatorConstLp' (hp_pos : p ≠ 0) (hμs_pos : μ s ≠ 0) :
    ‖indicatorConstLp p hs hμs c‖ = ‖c‖ * (μ s).toReal ^ (1 / p.toReal)

Proof state:
α : Type u_1
E : Type u_4
m0 : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
inst✝ : NormedAddCommGroup E
s : Set α
hs : MeasurableSet s
hμs : μ s ≠ ⊤
c : E
hp_pos : p ≠ 0
hμs_pos : μ s ≠ 0
⊢ ‖indicatorConstLp p hs hμs c‖ = ‖c‖ * (μ s).toReal ^ (1 / p.toReal)

Tactic:
by_cases hp_top : p = ∞

Result:
case pos
α : Type u_1
E : Type u_4
m0 : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
inst✝ : NormedAddCommGroup E
s : Set α
hs : MeasurableSet s
hμs : μ s ≠ ⊤
c : E
hp_pos : p ≠ 0
hμs_pos : μ s ≠ 0
hp_top : p = ⊤
⊢ ‖indicatorConstLp p hs hμs c‖ = ‖c‖ * (μ s).toReal ^ (1 / p.toReal)

case neg
α : Type u_1
E : Type u_4
m0 : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
inst✝ : NormedAddCommGroup E
s : Set α
hs : MeasurableSet s
hμs : μ s ≠ ⊤
c : E
hp_pos : p ≠ 0
hμs_pos : μ s ≠ 0
hp_top : ¬p = ⊤
⊢ ‖indicatorConstLp p hs hμs c‖ = ‖c‖ * (μ s).toReal ^ (1 / p.toReal)

Proof state:
case pos
α : Type u_1
E : Type u_4
m0 : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
inst✝ : NormedAddCommGroup E
s : Set α
hs : MeasurableSet s
hμs : μ s ≠ ⊤
c : E
hp_pos : p ≠ 0
hμs_pos : μ s ≠ 0
hp_top : p = ⊤
⊢ ‖indicatorConstLp p hs hμs c‖ = ‖c‖ * (μ s).toReal ^ (1 / p.toReal)

Tactic:
rw [hp_top, ENNReal.top_toReal, _root_.div_zero, Real.rpow_zero, mul_one]

Result:
case pos
α : Type u_1
E : Type u_4
m0 : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
inst✝ : NormedAddCommGroup E
s : Set α
hs : MeasurableSet s
hμs : μ s ≠ ⊤
c : E
hp_pos : p ≠ 0
hμs_pos : μ s ≠ 0
hp_top : p = ⊤
⊢ ‖indicatorConstLp ⊤ hs hμs c‖ = ‖c‖

Proof state:
case pos
α : Type u_1
E : Type u_4
m0 : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
inst✝ : NormedAddCommGroup E
s : Set α
hs : MeasurableSet s
hμs : μ s ≠ ⊤
c : E
hp_pos : p ≠ 0
hμs_pos : μ s ≠ 0
hp_top : p = ⊤
⊢ ‖indicatorConstLp ⊤ hs hμs c‖ = ‖c‖

Tactic:
exact norm_indicatorConstLp_top hμs_pos

Result:
no goals

Proof state:
case neg
α : Type u_1
E : Type u_4
m0 : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
inst✝ : NormedAddCommGroup E
s : Set α
hs : MeasurableSet s
hμs : μ s ≠ ⊤
c : E
hp_pos : p ≠ 0
hμs_pos : μ s ≠ 0
hp_top : ¬p = ⊤
⊢ ‖indicatorConstLp p hs hμs c‖ = ‖c‖ * (μ s).toReal ^ (1 / p.toReal)

Tactic:
exact norm_indicatorConstLp hp_pos hp_top

Result:
no goals
-- Mathlib/Order/Hom/Lattice.lean
theorem Codisjoint.map [OrderTop α] [OrderTop β] [TopHomClass F α β] [SupHomClass F α β] {a b : α}
    (f : F) (h : Codisjoint a b) : Codisjoint (f a) (f b)

Proof state:
F : Type u_1
α : Type u_3
β : Type u_4
inst✝⁶ : Lattice α
inst✝⁵ : Lattice β
inst✝⁴ : FunLike F α β
inst✝³ : OrderTop α
inst✝² : OrderTop β
inst✝¹ : TopHomClass F α β
inst✝ : SupHomClass F α β
a b : α
f : F
h : Codisjoint a b
⊢ Codisjoint (f a) (f b)

Tactic:
rw [codisjoint_iff, ← map_sup, h.eq_top, map_top]

Result:
no goals