harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/Geometry/Euclidean/Angle/Oriented/Rotation.lean
theorem rotation_eq_self_iff (x : V) (θ : Real.Angle) : o.rotation θ x = x ↔ x = 0 ∨ θ = 0

Proof state:
V : Type u_1
inst✝² : NormedAddCommGroup V
inst✝¹ : InnerProductSpace ℝ V
inst✝ : Fact (finrank ℝ V = 2)
o : Orientation ℝ V (Fin 2)
x : V
θ : Real.Angle
⊢ (o.rotation θ) x = x ↔ x = 0 ∨ θ = 0

Tactic:
by_cases h : x = 0 <;> simp [h]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/BitVec/Lemmas.lean
theorem toInt_mul (x y : BitVec w) :
  (x * y).toInt = (x.toInt * y.toInt).bmod (2^w)

Proof state:
w : Nat
x y : BitVec w
⊢ (x * y).toInt = (x.toInt * y.toInt).bmod (2 ^ w)

Tactic:
simp [toInt_eq_toNat_bmod]

Result:
no goals
-- Mathlib/NumberTheory/LegendreSymbol/ZModChar.lean
theorem χ₈'_int_eq_χ₄_mul_χ₈ (a : ℤ) : χ₈' a = χ₄ a * χ₈ a

Proof state:
a : ℤ
⊢ 4 ∣ 8

Tactic:
omega

Result:
no goals

Proof state:
a : ℤ
⊢ χ₈' ↑a = χ₄ (↑a).cast * χ₈ ↑a

Tactic:
exact χ₈'_eq_χ₄_mul_χ₈ a

Result:
no goals

Proof state:
a : ℤ
⊢ χ₈' ↑a = χ₄ ↑a * χ₈ ↑a

Tactic:
rw [← @cast_intCast 8 (ZMod 4) _ 4 _ (by omega) a]

Result:
a : ℤ
⊢ χ₈' ↑a = χ₄ (↑a).cast * χ₈ ↑a
-- Mathlib/Analysis/Normed/Lp/lpSpace.lean
theorem memℓp_gen_iff (hp : 0 < p.toReal) {f : ∀ i, E i} :
    Memℓp f p ↔ Summable fun i => ‖f i‖ ^ p.toReal

Proof state:
α : Type u_3
E : α → Type u_4
p : ℝ≥0∞
inst✝ : (i : α) → NormedAddCommGroup (E i)
hp : 0 < p ∧ p < ⊤
f : (i : α) → E i
⊢ Memℓp f p ↔ Summable fun i => ‖f i‖ ^ p.toReal

Tactic:
dsimp [Memℓp]

Result:
α : Type u_3
E : α → Type u_4
p : ℝ≥0∞
inst✝ : (i : α) → NormedAddCommGroup (E i)
hp : 0 < p ∧ p < ⊤
f : (i : α) → E i
⊢ (if p = 0 then {i | ¬f i = 0}.Finite
    else if p = ⊤ then BddAbove (Set.range fun i => ‖f i‖) else Summable fun i => ‖f i‖ ^ p.toReal) ↔
    Summable fun i => ‖f i‖ ^ p.toReal

Proof state:
α : Type u_3
E : α → Type u_4
p : ℝ≥0∞
inst✝ : (i : α) → NormedAddCommGroup (E i)
hp : 0 < p.toReal
f : (i : α) → E i
⊢ Memℓp f p ↔ Summable fun i => ‖f i‖ ^ p.toReal

Tactic:
rw [ENNReal.toReal_pos_iff] at hp

Result:
α : Type u_3
E : α → Type u_4
p : ℝ≥0∞
inst✝ : (i : α) → NormedAddCommGroup (E i)
hp : 0 < p ∧ p < ⊤
f : (i : α) → E i
⊢ Memℓp f p ↔ Summable fun i => ‖f i‖ ^ p.toReal

Proof state:
α : Type u_3
E : α → Type u_4
p : ℝ≥0∞
inst✝ : (i : α) → NormedAddCommGroup (E i)
hp : 0 < p ∧ p < ⊤
f : (i : α) → E i
⊢ (if p = 0 then {i | ¬f i = 0}.Finite
    else if p = ⊤ then BddAbove (Set.range fun i => ‖f i‖) else Summable fun i => ‖f i‖ ^ p.toReal) ↔
    Summable fun i => ‖f i‖ ^ p.toReal

Tactic:
rw [if_neg hp.1.ne', if_neg hp.2.ne]

Result:
no goals
-- Mathlib/Algebra/Module/Injective.lean
theorem ExtensionOfMaxAdjoin.extendIdealTo_eq (h : Module.Baer R Q) {y : N} (r : R)
    (hr : r • y ∈ (extensionOfMax i f).domain) : ExtensionOfMaxAdjoin.extendIdealTo i f h y r =
    (extensionOfMax i f).toLinearPMap ⟨r • y, hr⟩

Proof state:
R : Type u
inst✝⁷ : Ring R
Q : Type v
inst✝⁶ : AddCommGroup Q
inst✝⁵ : Module R Q
M : Type u_1
N : Type u_2
inst✝⁴ : AddCommGroup M
inst✝³ : AddCommGroup N
inst✝² : Module R M
inst✝¹ : Module R N
i : M →ₗ[R] N
f : M →ₗ[R] Q
inst✝ : Fact (Function.Injective ⇑i)
h : Baer R Q
y : N
r : R
hr : r • y ∈ (extensionOfMax i f).domain
⊢ (extendIdealTo i f h y) r = ↑(extensionOfMax i f).toLinearPMap ⟨r • y, hr⟩

Tactic:
simp only [ExtensionOfMaxAdjoin.extendIdealTo_is_extension i f h _ _ hr,
  ExtensionOfMaxAdjoin.idealTo, LinearMap.coe_mk, Subtype.coe_mk, AddHom.coe_mk]

Result:
no goals
-- Mathlib/Algebra/Polynomial/Basic.lean
theorem sum_add' {S : Type*} [AddCommMonoid S] (p : R[X]) (f g : ℕ → R → S) :
    p.sum (f + g) = p.sum f + p.sum g

Proof state:
R : Type u
inst✝¹ : Semiring R
S : Type u_1
inst✝ : AddCommMonoid S
p : R[X]
f g : ℕ → R → S
⊢ p.sum (f + g) = p.sum f + p.sum g

Tactic:
simp [sum_def, Finset.sum_add_distrib]

Result:
no goals
-- Mathlib/SetTheory/Cardinal/Cofinality.lean
theorem le_cof_iff_blsub {b : Ordinal} {a : Cardinal} :
    a ≤ cof b ↔ ∀ {o} (f : ∀ a < o, Ordinal), blsub.{u, u} o f = b → a ≤ o.card :=
  le_cof_iff_lsub.trans
    ⟨fun H o f hf => by simpa using H _ hf, fun H ι f hf => by
      rcases Cardinal.ord_eq ι with ⟨r, hr, hι'⟩
      rw [← @blsub_eq_lsub' ι r hr] at hf
      simpa using H _ hf⟩

Proof state:
b : Ordinal.{u}
a : Cardinal.{u}
H : ∀ {o : Ordinal.{u}} (f : (a : Ordinal.{u}) → a < o → Ordinal.{u}), o.blsub f = b → a ≤ o.card
ι : Type u
f : ι → Ordinal.{u}
hf : lsub f = b
⊢ a ≤ #ι

Tactic:
rcases Cardinal.ord_eq ι with ⟨r, hr, hι'⟩

Result:
case intro.intro
b : Ordinal.{u}
a : Cardinal.{u}
H : ∀ {o : Ordinal.{u}} (f : (a : Ordinal.{u}) → a < o → Ordinal.{u}), o.blsub f = b → a ≤ o.card
ι : Type u
f : ι → Ordinal.{u}
hf : lsub f = b
r : ι → ι → Prop
hr : IsWellOrder ι r
hι' : (#ι).ord = type r
⊢ a ≤ #ι

Proof state:
b : Ordinal.{u}
a : Cardinal.{u}
H : ∀ {ι : Type u} (f : ι → Ordinal.{u}), lsub f = b → a ≤ #ι
o : Ordinal.{u}
f : (a : Ordinal.{u}) → a < o → Ordinal.{u}
hf : o.blsub f = b
⊢ a ≤ o.card

Tactic:
simpa using H _ hf

Result:
no goals

Proof state:
case intro.intro
b : Ordinal.{u}
a : Cardinal.{u}
H : ∀ {o : Ordinal.{u}} (f : (a : Ordinal.{u}) → a < o → Ordinal.{u}), o.blsub f = b → a ≤ o.card
ι : Type u
f : ι → Ordinal.{u}
r : ι → ι → Prop
hr : IsWellOrder ι r
hf : (type r).blsub (bfamilyOfFamily' r f) = b
hι' : (#ι).ord = type r
⊢ a ≤ #ι

Tactic:
simpa using H _ hf

Result:
no goals

Proof state:
case intro.intro
b : Ordinal.{u}
a : Cardinal.{u}
H : ∀ {o : Ordinal.{u}} (f : (a : Ordinal.{u}) → a < o → Ordinal.{u}), o.blsub f = b → a ≤ o.card
ι : Type u
f : ι → Ordinal.{u}
hf : lsub f = b
r : ι → ι → Prop
hr : IsWellOrder ι r
hι' : (#ι).ord = type r
⊢ a ≤ #ι

Tactic:
rw [← @blsub_eq_lsub' ι r hr] at hf

Result:
case intro.intro
b : Ordinal.{u}
a : Cardinal.{u}
H : ∀ {o : Ordinal.{u}} (f : (a : Ordinal.{u}) → a < o → Ordinal.{u}), o.blsub f = b → a ≤ o.card
ι : Type u
f : ι → Ordinal.{u}
r : ι → ι → Prop
hr : IsWellOrder ι r
hf : (type r).blsub (bfamilyOfFamily' r f) = b
hι' : (#ι).ord = type r
⊢ a ≤ #ι
-- Mathlib/Algebra/Group/Action/Pi.lean
/-- If `α i` has a faithful scalar action for a given `i`, then so does `Π i, α i`. This is
not an instance as `i` cannot be inferred. -/
@[to_additive
"If `α i` has a faithful additive action for a given `i`, then
so does `Π i, α i`. This is not an instance as `i` cannot be inferred"]
lemma faithfulSMul_at [∀ i, SMul M (α i)] [∀ i, Nonempty (α i)] (i : ι) [FaithfulSMul M (α i)] :
    FaithfulSMul M (∀ i, α i) where
  eq_of_smul_eq_smul h := eq_of_smul_eq_smul fun a : α i => by
    classical
    simpa using
      congr_fun (h <| Function.update (fun j => Classical.choice (‹∀ i, Nonempty (α i)› j)) i a) i

Proof state:
ι : Type u_1
M : Type u_2
α : ι → Type u_4
inst✝² : (i : ι) → SMul M (α i)
inst✝¹ : ∀ (i : ι), Nonempty (α i)
i : ι
inst✝ : FaithfulSMul M (α i)
m₁✝ m₂✝ : M
h : ∀ (a : (i : ι) → α i), m₁✝ • a = m₂✝ • a
a : α i
⊢ m₁✝ • a = m₂✝ • a

Tactic:
classical
simpa using
  congr_fun (h <| Function.update (fun j => Classical.choice (‹∀ i, Nonempty (α i)› j)) i a) i

Result:
no goals

Proof state:
ι : Type u_1
M : Type u_2
α : ι → Type u_4
inst✝² : (i : ι) → SMul M (α i)
inst✝¹ : ∀ (i : ι), Nonempty (α i)
i : ι
inst✝ : FaithfulSMul M (α i)
m₁✝ m₂✝ : M
h : ∀ (a : (i : ι) → α i), m₁✝ • a = m₂✝ • a
a : α i
⊢ m₁✝ • a = m₂✝ • a

Tactic:
simpa using
  congr_fun (h <| Function.update (fun j => Classical.choice (‹∀ i, Nonempty (α i)› j)) i a) i

Result:
no goals
-- Mathlib/Combinatorics/Colex.lean
theorem lt_geomSum_of_mem {a : ℕ} (hn : 2 ≤ n) (hi : a ∈ s) : a < ∑ i ∈ s, n ^ i :=
  (a.lt_pow_self hn).trans_le <| single_le_sum (by simp) hi

Proof state:
s : Finset ℕ
n a : ℕ
hn : 2 ≤ n
hi : a ∈ s
⊢ ∀ i ∈ s, 0 ≤ n ^ i

Tactic:
simp

Result:
no goals
-- Mathlib/Algebra/Divisibility/Basic.lean
theorem Dvd.intro_left (c : α) (h : c * a = b) : a ∣ b :=
  Dvd.intro c (by rw [mul_comm] at h; apply h)

Proof state:
α : Type u_1
inst✝ : CommSemigroup α
a b c : α
h : a * c = b
⊢ a * c = b

Tactic:
apply h

Result:
no goals

Proof state:
α : Type u_1
inst✝ : CommSemigroup α
a b c : α
h : c * a = b
⊢ a * c = b

Tactic:
rw [mul_comm] at h

Result:
α : Type u_1
inst✝ : CommSemigroup α
a b c : α
h : a * c = b
⊢ a * c = b
-- Mathlib/Data/Finset/SDiff.lean
theorem insert_sdiff_of_mem (s : Finset α) {x : α} (h : x ∈ t) : insert x s \ t = s \ t

Proof state:
α : Type u_1
inst✝ : DecidableEq α
t s : Finset α
x : α
h : x ∈ t
⊢ insert x ↑s \ ↑t = ↑s \ ↑t

Tactic:
exact Set.insert_diff_of_mem _ h

Result:
no goals

Proof state:
α : Type u_1
inst✝ : DecidableEq α
t s : Finset α
x : α
h : x ∈ t
⊢ insert x s \ t = s \ t

Tactic:
rw [← coe_inj, coe_sdiff, coe_sdiff, coe_insert]

Result:
α : Type u_1
inst✝ : DecidableEq α
t s : Finset α
x : α
h : x ∈ t
⊢ insert x ↑s \ ↑t = ↑s \ ↑t
-- Mathlib/RingTheory/UniqueFactorizationDomain/Basic.lean
theorem factors_pos (x : α) (hx : x ≠ 0) : 0 < factors x ↔ ¬IsUnit x

Proof state:
α : Type u_1
inst✝¹ : CancelCommMonoidWithZero α
inst✝ : UniqueFactorizationMonoid α
x : α
hx : x ≠ 0
⊢ 0 < factors x ↔ ¬IsUnit x

Tactic:
constructor

Result:
case mp
α : Type u_1
inst✝¹ : CancelCommMonoidWithZero α
inst✝ : UniqueFactorizationMonoid α
x : α
hx : x ≠ 0
⊢ 0 < factors x → ¬IsUnit x

case mpr
α : Type u_1
inst✝¹ : CancelCommMonoidWithZero α
inst✝ : UniqueFactorizationMonoid α
x : α
hx : x ≠ 0
⊢ ¬IsUnit x → 0 < factors x

Proof state:
case mp
α : Type u_1
inst✝¹ : CancelCommMonoidWithZero α
inst✝ : UniqueFactorizationMonoid α
x : α
hx : x ≠ 0
⊢ 0 < factors x → ¬IsUnit x

Tactic:
intro h hx

Result:
case mp
α : Type u_1
inst✝¹ : CancelCommMonoidWithZero α
inst✝ : UniqueFactorizationMonoid α
x : α
hx✝ : x ≠ 0
h : 0 < factors x
hx : IsUnit x
⊢ False

Proof state:
case mpr
α : Type u_1
inst✝¹ : CancelCommMonoidWithZero α
inst✝ : UniqueFactorizationMonoid α
x : α
hx : x ≠ 0
⊢ ¬IsUnit x → 0 < factors x

Tactic:
intro h

Result:
case mpr
α : Type u_1
inst✝¹ : CancelCommMonoidWithZero α
inst✝ : UniqueFactorizationMonoid α
x : α
hx : x ≠ 0
h : ¬IsUnit x
⊢ 0 < factors x

Proof state:
case mpr.intro
α : Type u_1
inst✝¹ : CancelCommMonoidWithZero α
inst✝ : UniqueFactorizationMonoid α
x : α
hx : x ≠ 0
h : ¬IsUnit x
p : α
hp : p ∈ factors x
⊢ 0 < factors x

Tactic:
exact
  bot_lt_iff_ne_bot.mpr
    (mt Multiset.eq_zero_iff_forall_not_mem.mp (not_forall.mpr ⟨p, not_not.mpr hp⟩))

Result:
no goals

Proof state:
case mpr
α : Type u_1
inst✝¹ : CancelCommMonoidWithZero α
inst✝ : UniqueFactorizationMonoid α
x : α
hx : x ≠ 0
h : ¬IsUnit x
⊢ 0 < factors x

Tactic:
obtain ⟨p, hp⟩ := exists_mem_factors hx h

Result:
case mpr.intro
α : Type u_1
inst✝¹ : CancelCommMonoidWithZero α
inst✝ : UniqueFactorizationMonoid α
x : α
hx : x ≠ 0
h : ¬IsUnit x
p : α
hp : p ∈ factors x
⊢ 0 < factors x

Proof state:
case mp
α : Type u_1
inst✝¹ : CancelCommMonoidWithZero α
inst✝ : UniqueFactorizationMonoid α
x : α
hx✝ : x ≠ 0
h : 0 < factors x
hx : IsUnit x
⊢ False

Tactic:
obtain ⟨p, hp⟩ := Multiset.exists_mem_of_ne_zero h.ne'

Result:
case mp.intro
α : Type u_1
inst✝¹ : CancelCommMonoidWithZero α
inst✝ : UniqueFactorizationMonoid α
x : α
hx✝ : x ≠ 0
h : 0 < factors x
hx : IsUnit x
p : α
hp : p ∈ factors x
⊢ False

Proof state:
case mp.intro
α : Type u_1
inst✝¹ : CancelCommMonoidWithZero α
inst✝ : UniqueFactorizationMonoid α
x : α
hx✝ : x ≠ 0
h : 0 < factors x
hx : IsUnit x
p : α
hp : p ∈ factors x
⊢ False

Tactic:
exact (prime_of_factor _ hp).not_unit (isUnit_of_dvd_unit (dvd_of_mem_factors hp) hx)

Result:
no goals
-- Mathlib/CategoryTheory/Limits/Indization/ParallelPair.lean
theorem hf : f = IsColimit.map (isColimit₁ f g P₁ P₂)
    (Cocone.mk B (ι₂ f g P₁ P₂)) (whiskerRight (ϕ f g P₁ P₂) yoneda)

Proof state:
C : Type u₁
inst✝ : Category.{v₁, u₁} C
A B : Cᵒᵖ ⥤ Type v₁
f g : A ⟶ B
P₁ : IndObjectPresentation A
P₂ : IndObjectPresentation B
i : K f g P₁ P₂
⊢ { pt := A, ι := ι₁ f g P₁ P₂ }.ι.app i ≫ f =
    { pt := A, ι := ι₁ f g P₁ P₂ }.ι.app i ≫
      (isColimit₁ f g P₁ P₂).map { pt := B, ι := ι₂ f g P₁ P₂ } (whiskerRight (ϕ f g P₁ P₂) yoneda)

Tactic:
rw [IsColimit.ι_map]

Result:
C : Type u₁
inst✝ : Category.{v₁, u₁} C
A B : Cᵒᵖ ⥤ Type v₁
f g : A ⟶ B
P₁ : IndObjectPresentation A
P₂ : IndObjectPresentation B
i : K f g P₁ P₂
⊢ { pt := A, ι := ι₁ f g P₁ P₂ }.ι.app i ≫ f =
    (whiskerRight (ϕ f g P₁ P₂) yoneda).app i ≫ { pt := B, ι := ι₂ f g P₁ P₂ }.ι.app i

Proof state:
C : Type u₁
inst✝ : Category.{v₁, u₁} C
A B : Cᵒᵖ ⥤ Type v₁
f g : A ⟶ B
P₁ : IndObjectPresentation A
P₂ : IndObjectPresentation B
i : K f g P₁ P₂
⊢ { pt := A, ι := ι₁ f g P₁ P₂ }.ι.app i ≫ f =
    (whiskerRight (ϕ f g P₁ P₂) yoneda).app i ≫ { pt := B, ι := ι₂ f g P₁ P₂ }.ι.app i

Tactic:
simpa using i.hom.1.w.symm

Result:
no goals

Proof state:
C : Type u₁
inst✝ : Category.{v₁, u₁} C
A B : Cᵒᵖ ⥤ Type v₁
f g : A ⟶ B
P₁ : IndObjectPresentation A
P₂ : IndObjectPresentation B
⊢ f = (isColimit₁ f g P₁ P₂).map { pt := B, ι := ι₂ f g P₁ P₂ } (whiskerRight (ϕ f g P₁ P₂) yoneda)

Tactic:
refine (isColimit₁ f g P₁ P₂).hom_ext (fun i => ?_)

Result:
C : Type u₁
inst✝ : Category.{v₁, u₁} C
A B : Cᵒᵖ ⥤ Type v₁
f g : A ⟶ B
P₁ : IndObjectPresentation A
P₂ : IndObjectPresentation B
i : K f g P₁ P₂
⊢ { pt := A, ι := ι₁ f g P₁ P₂ }.ι.app i ≫ f =
    { pt := A, ι := ι₁ f g P₁ P₂ }.ι.app i ≫
      (isColimit₁ f g P₁ P₂).map { pt := B, ι := ι₂ f g P₁ P₂ } (whiskerRight (ϕ f g P₁ P₂) yoneda)
-- Mathlib/Algebra/Ring/Subsemiring/Basic.lean
theorem map_iInf {ι : Sort*} [Nonempty ι] (f : R →+* S) (hf : Function.Injective f)
    (s : ι → Subsemiring R) : (iInf s).map f = ⨅ i, (s i).map f

Proof state:
R : Type u
S : Type v
inst✝² : NonAssocSemiring R
inst✝¹ : NonAssocSemiring S
ι : Sort u_1
inst✝ : Nonempty ι
f : R →+* S
hf : Function.Injective ⇑f
s : ι → Subsemiring R
⊢ map f (iInf s) = ⨅ i, map f (s i)

Tactic:
apply SetLike.coe_injective

Result:
case a
R : Type u
S : Type v
inst✝² : NonAssocSemiring R
inst✝¹ : NonAssocSemiring S
ι : Sort u_1
inst✝ : Nonempty ι
f : R →+* S
hf : Function.Injective ⇑f
s : ι → Subsemiring R
⊢ ↑(map f (iInf s)) = ↑(⨅ i, map f (s i))

Proof state:
case a
R : Type u
S : Type v
inst✝² : NonAssocSemiring R
inst✝¹ : NonAssocSemiring S
ι : Sort u_1
inst✝ : Nonempty ι
f : R →+* S
hf : Function.Injective ⇑f
s : ι → Subsemiring R
⊢ ↑(map f (iInf s)) = ↑(⨅ i, map f (s i))

Tactic:
simpa using (Set.injOn_of_injective hf).image_iInter_eq (s := SetLike.coe ∘ s)

Result:
no goals
-- Mathlib/Probability/Kernel/Disintegration/MeasurableStieltjes.lean
lemma isMeasurableRatCDF_toRatCDF (hf : Measurable f) :
    IsMeasurableRatCDF (toRatCDF f) where
  isRatStieltjesPoint a

Proof state:
α : Type u_1
f : α → ℚ → ℝ
inst✝ : MeasurableSpace α
hf : Measurable f
a : α
⊢ IsRatStieltjesPoint (toRatCDF f) a

Tactic:
classical
exact IsRatStieltjesPoint.ite (IsRatStieltjesPoint f) id
  (fun _ ↦ isRatStieltjesPoint_defaultRatCDF a)

Result:
no goals

Proof state:
α : Type u_1
f : α → ℚ → ℝ
inst✝ : MeasurableSpace α
hf : Measurable f
a : α
⊢ IsRatStieltjesPoint (toRatCDF f) a

Tactic:
exact IsRatStieltjesPoint.ite (IsRatStieltjesPoint f) id
  (fun _ ↦ isRatStieltjesPoint_defaultRatCDF a)

Result:
no goals
-- Mathlib/CategoryTheory/Closed/Monoidal.lean
theorem pre_id (A : C) [Closed A] : pre (𝟙 A) = 𝟙 _

Proof state:
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : MonoidalCategory C
A : C
inst✝ : Closed A
⊢ pre (𝟙 A) = 𝟙 (ihom A)

Tactic:
rw [pre, Functor.map_id]

Result:
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : MonoidalCategory C
A : C
inst✝ : Closed A
⊢ (conjugateEquiv (ihom.adjunction A) (ihom.adjunction A)) (𝟙 ((tensoringLeft C).obj A)) = 𝟙 (ihom A)

Proof state:
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : MonoidalCategory C
A : C
inst✝ : Closed A
⊢ (conjugateEquiv (ihom.adjunction A) (ihom.adjunction A)) (𝟙 ((tensoringLeft C).obj A)) = 𝟙 (ihom A)

Tactic:
apply conjugateEquiv_id

Result:
no goals
-- Mathlib/RingTheory/Idempotents.lean
lemma mem_corner_iff_mul_left (hc : IsMulCentral e) {r : R} : r ∈ corner e ↔ e * r = r

Proof state:
R : Type u_1
e : R
inst✝ : Semigroup R
idem : IsIdempotentElem e
hc : IsMulCentral e
r : R
a✝ : e * r = r
⊢ r * e = r

Tactic:
rwa [← hc.comm]

Result:
no goals

Proof state:
R : Type u_1
e : R
inst✝ : Semigroup R
idem : IsIdempotentElem e
hc : IsMulCentral e
r : R
⊢ e * r = r → r * e = r

Tactic:
intro

Result:
R : Type u_1
e : R
inst✝ : Semigroup R
idem : IsIdempotentElem e
hc : IsMulCentral e
r : R
a✝ : e * r = r
⊢ r * e = r

Proof state:
R : Type u_1
e : R
inst✝ : Semigroup R
idem : IsIdempotentElem e
hc : IsMulCentral e
r : R
⊢ r ∈ corner e ↔ e * r = r

Tactic:
rw [mem_corner_iff idem, and_iff_left_of_imp]

Result:
R : Type u_1
e : R
inst✝ : Semigroup R
idem : IsIdempotentElem e
hc : IsMulCentral e
r : R
⊢ e * r = r → r * e = r
-- Mathlib/Analysis/BoxIntegral/Partition/Basic.lean
theorem biUnionIndex_le (πi : ∀ J, Prepartition J) (J : Box ι) : π.biUnionIndex πi J ≤ I

Proof state:
case pos
ι : Type u_1
I : Box ι
π : Prepartition I
πi : (J : Box ι) → Prepartition J
J : Box ι
hJ : J ∈ π.biUnion πi
⊢ π.biUnionIndex πi J ≤ I

Tactic:
exact π.le_of_mem (π.biUnionIndex_mem hJ)

Result:
no goals

Proof state:
case neg
ι : Type u_1
I : Box ι
π : Prepartition I
πi : (J : Box ι) → Prepartition J
J : Box ι
hJ : J ∉ π.biUnion πi
⊢ π.biUnionIndex πi J ≤ I

Tactic:
rw [biUnionIndex, dif_neg hJ]

Result:
no goals

Proof state:
ι : Type u_1
I : Box ι
π : Prepartition I
πi : (J : Box ι) → Prepartition J
J : Box ι
⊢ π.biUnionIndex πi J ≤ I

Tactic:
by_cases hJ : J ∈ π.biUnion πi

Result:
case pos
ι : Type u_1
I : Box ι
π : Prepartition I
πi : (J : Box ι) → Prepartition J
J : Box ι
hJ : J ∈ π.biUnion πi
⊢ π.biUnionIndex πi J ≤ I

case neg
ι : Type u_1
I : Box ι
π : Prepartition I
πi : (J : Box ι) → Prepartition J
J : Box ι
hJ : J ∉ π.biUnion πi
⊢ π.biUnionIndex πi J ≤ I
-- Mathlib/Algebra/GroupWithZero/NonZeroDivisors.lean
lemma mul_left_mem_nonZeroDivisors_eq_zero_iff (hr : r ∈ M₀⁰) : r * x = 0 ↔ x = 0

Proof state:
M₀ : Type u_1
inst✝ : CommMonoidWithZero M₀
r x : M₀
hr : r ∈ M₀⁰
⊢ r * x = 0 ↔ x = 0

Tactic:
rw [mul_comm, mul_right_mem_nonZeroDivisors_eq_zero_iff hr]

Result:
no goals
-- Mathlib/FieldTheory/Normal/Closure.lean
@[simp]
lemma normalClosure_map_eq (K : IntermediateField F L) (σ : L →ₐ[F] L) :
    normalClosure F (K.map σ) L = normalClosure F K L

Proof state:
F : Type u_1
L : Type u_3
inst✝³ : Field F
inst✝² : Field L
inst✝¹ : Algebra F L
inst✝ : Normal F L
K : IntermediateField F L
σ : L →ₐ[F] L
⊢ normalClosure F (↥(map σ K)) L = normalClosure F (↥K) L

Tactic:
have (σ : L ≃ₐ[F] L) : normalClosure F (K.map (σ : L →ₐ[F] L)) L = normalClosure F K L := by
  simp_rw [normalClosure_def'', map_map]
  exact (Equiv.mulRight σ).iSup_congr fun _ ↦ rfl

Result:
F : Type u_1
L : Type u_3
inst✝³ : Field F
inst✝² : Field L
inst✝¹ : Algebra F L
inst✝ : Normal F L
K : IntermediateField F L
σ : L →ₐ[F] L
this : ∀ (σ : L ≃ₐ[F] L), normalClosure F (↥(map (↑σ) K)) L = normalClosure F (↥K) L
⊢ normalClosure F (↥(map σ K)) L = normalClosure F (↥K) L

Proof state:
F : Type u_1
L : Type u_3
inst✝³ : Field F
inst✝² : Field L
inst✝¹ : Algebra F L
inst✝ : Normal F L
K : IntermediateField F L
σ✝ : L →ₐ[F] L
σ : L ≃ₐ[F] L
⊢ normalClosure F (↥(map (↑σ) K)) L = normalClosure F (↥K) L

Tactic:
simp_rw [normalClosure_def'', map_map]

Result:
F : Type u_1
L : Type u_3
inst✝³ : Field F
inst✝² : Field L
inst✝¹ : Algebra F L
inst✝ : Normal F L
K : IntermediateField F L
σ✝ : L →ₐ[F] L
σ : L ≃ₐ[F] L
⊢ ⨆ f, map ((↑f).comp ↑σ) K = ⨆ f, map (↑f) K

Proof state:
F : Type u_1
L : Type u_3
inst✝³ : Field F
inst✝² : Field L
inst✝¹ : Algebra F L
inst✝ : Normal F L
K : IntermediateField F L
σ : L →ₐ[F] L
this : ∀ (σ : L ≃ₐ[F] L), normalClosure F (↥(map (↑σ) K)) L = normalClosure F (↥K) L
⊢ normalClosure F (↥(map σ K)) L = normalClosure F (↥K) L

Tactic:
exact this ((Algebra.IsAlgebraic.algEquivEquivAlgHom _ _).symm σ)

Result:
no goals

Proof state:
F : Type u_1
L : Type u_3
inst✝³ : Field F
inst✝² : Field L
inst✝¹ : Algebra F L
inst✝ : Normal F L
K : IntermediateField F L
σ✝ : L →ₐ[F] L
σ : L ≃ₐ[F] L
⊢ ⨆ f, map ((↑f).comp ↑σ) K = ⨆ f, map (↑f) K

Tactic:
exact (Equiv.mulRight σ).iSup_congr fun _ ↦ rfl

Result:
no goals
-- Mathlib/RingTheory/Multiplicity.lean
theorem emultiplicity_eq_of_dvd_of_not_dvd {k : ℕ} (hk : a ^ k ∣ b) (hsucc : ¬a ^ (k + 1) ∣ b) :
    emultiplicity a b = k

Proof state:
α : Type u_1
inst✝ : Monoid α
a b : α
k : ℕ
hk : a ^ k ∣ b
hsucc : ¬a ^ (k + 1) ∣ b
this : FiniteMultiplicity a b
⊢ ∀ n < k, a ^ (n + 1) ∣ b

Tactic:
exact fun n hn ↦ (pow_dvd_pow _ hn).trans hk

Result:
no goals

Proof state:
α : Type u_1
inst✝ : Monoid α
a b : α
k : ℕ
hk : a ^ k ∣ b
hsucc : ¬a ^ (k + 1) ∣ b
this : FiniteMultiplicity a b
⊢ emultiplicity a b = ↑k

Tactic:
simp only [emultiplicity, this, ↓reduceDIte, Nat.cast_inj, find_eq_iff, hsucc, not_false_eq_true,
  Decidable.not_not, true_and]

Result:
α : Type u_1
inst✝ : Monoid α
a b : α
k : ℕ
hk : a ^ k ∣ b
hsucc : ¬a ^ (k + 1) ∣ b
this : FiniteMultiplicity a b
⊢ ∀ n < k, a ^ (n + 1) ∣ b

Proof state:
α : Type u_1
inst✝ : Monoid α
a b : α
k : ℕ
hk : a ^ k ∣ b
hsucc : ¬a ^ (k + 1) ∣ b
⊢ emultiplicity a b = ↑k

Tactic:
classical
have : FiniteMultiplicity a b := ⟨k, hsucc⟩
simp only [emultiplicity, this, ↓reduceDIte, Nat.cast_inj, find_eq_iff, hsucc, not_false_eq_true,
Decidable.not_not, true_and]
exact fun n hn ↦ (pow_dvd_pow _ hn).trans hk

Result:
no goals

Proof state:
α : Type u_1
inst✝ : Monoid α
a b : α
k : ℕ
hk : a ^ k ∣ b
hsucc : ¬a ^ (k + 1) ∣ b
⊢ emultiplicity a b = ↑k

Tactic:
have : FiniteMultiplicity a b := ⟨k, hsucc⟩

Result:
α : Type u_1
inst✝ : Monoid α
a b : α
k : ℕ
hk : a ^ k ∣ b
hsucc : ¬a ^ (k + 1) ∣ b
this : FiniteMultiplicity a b
⊢ emultiplicity a b = ↑k
-- Mathlib/RingTheory/Finiteness/Basic.lean
theorem comp {g : B →+* C} {f : A →+* B} (hg : g.Finite) (hf : f.Finite) : (g.comp f).Finite

Proof state:
A : Type u_1
B : Type u_2
C : Type u_3
inst✝² : CommRing A
inst✝¹ : CommRing B
inst✝ : CommRing C
g : B →+* C
f : A →+* B
hg : g.Finite
hf : f.Finite
⊢ (g.comp f).Finite

Tactic:
algebraize [f, g, g.comp f]

Result:
A : Type u_1
B : Type u_2
C : Type u_3
inst✝² : CommRing A
inst✝¹ : CommRing B
inst✝ : CommRing C
g : B →+* C
f : A →+* B
hg : g.Finite
hf : f.Finite
algInst✝² : Algebra A B := f.toAlgebra
algInst✝¹ : Algebra B C := g.toAlgebra
algInst✝ : Algebra A C := (g.comp f).toAlgebra
scalarTowerInst✝ : IsScalarTower A B C := IsScalarTower.of_algebraMap_eq' (Eq.refl (algebraMap A C))
algebraizeInst✝¹ : Module.Finite B C
algebraizeInst✝ : Module.Finite A B
⊢ (g.comp f).Finite

Proof state:
A : Type u_1
B : Type u_2
C : Type u_3
inst✝² : CommRing A
inst✝¹ : CommRing B
inst✝ : CommRing C
g : B →+* C
f : A →+* B
hg : g.Finite
hf : f.Finite
algInst✝² : Algebra A B := f.toAlgebra
algInst✝¹ : Algebra B C := g.toAlgebra
algInst✝ : Algebra A C := (g.comp f).toAlgebra
scalarTowerInst✝ : IsScalarTower A B C := IsScalarTower.of_algebraMap_eq' (Eq.refl (algebraMap A C))
algebraizeInst✝¹ : Module.Finite B C
algebraizeInst✝ : Module.Finite A B
⊢ (g.comp f).Finite

Tactic:
exact Module.Finite.trans B C

Result:
no goals