harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/Geometry/Euclidean/Angle/Oriented/Affine.lean
theorem _root_.AffineSubspace.SOppSide.oangle_sign_eq_neg {s : AffineSubspace ℝ P} {p₁ p₂ p₃ p₄ : P}
    (hp₁ : p₁ ∈ s) (hp₂ : p₂ ∈ s) (hp₃p₄ : s.SOppSide p₃ p₄) :
    (∡ p₁ p₄ p₂).sign = -(∡ p₁ p₃ p₂).sign

Proof state:
V : Type u_1
P : Type u_2
inst✝⁴ : NormedAddCommGroup V
inst✝³ : InnerProductSpace ℝ V
inst✝² : MetricSpace P
inst✝¹ : NormedAddTorsor V P
hd2 : Fact (finrank ℝ V = 2)
inst✝ : Oriented ℝ V (Fin 2)
s : AffineSubspace ℝ P
p₁ p₂ p₃ p₄ : P
hp₁ : p₁ ∈ s
hp₂ : p₂ ∈ s
hp₃p₄ : s.SOppSide p₃ p₄
⊢ p₁ ≠ p₃

Tactic:
rintro rfl

Result:
V : Type u_1
P : Type u_2
inst✝⁴ : NormedAddCommGroup V
inst✝³ : InnerProductSpace ℝ V
inst✝² : MetricSpace P
inst✝¹ : NormedAddTorsor V P
hd2 : Fact (finrank ℝ V = 2)
inst✝ : Oriented ℝ V (Fin 2)
s : AffineSubspace ℝ P
p₁ p₂ p₄ : P
hp₁ : p₁ ∈ s
hp₂ : p₂ ∈ s
hp₃p₄ : s.SOppSide p₁ p₄
⊢ False

Proof state:
V : Type u_1
P : Type u_2
inst✝⁴ : NormedAddCommGroup V
inst✝³ : InnerProductSpace ℝ V
inst✝² : MetricSpace P
inst✝¹ : NormedAddTorsor V P
hd2 : Fact (finrank ℝ V = 2)
inst✝ : Oriented ℝ V (Fin 2)
s : AffineSubspace ℝ P
p₁ p₂ p₃ p₄ : P
hp₁ : p₁ ∈ s
hp₂ : p₂ ∈ s
hp₃p₄ : s.SOppSide p₃ p₄
hp₁p₃ : p₁ ≠ p₃
⊢ (∡ p₁ p₄ p₂).sign = -(∡ p₁ p₃ p₂).sign

Tactic:
rw [← (hp₃p₄.symm.trans (sOppSide_pointReflection hp₁ hp₃p₄.left_not_mem)).oangle_sign_eq hp₁ hp₂,
  ← oangle_rotate_sign p₁, ← oangle_rotate_sign p₁, oangle_swap₁₃_sign,
  (sbtw_pointReflection_of_ne ℝ hp₁p₃).symm.oangle_sign_eq _]

Result:
no goals

Proof state:
V : Type u_1
P : Type u_2
inst✝⁴ : NormedAddCommGroup V
inst✝³ : InnerProductSpace ℝ V
inst✝² : MetricSpace P
inst✝¹ : NormedAddTorsor V P
hd2 : Fact (finrank ℝ V = 2)
inst✝ : Oriented ℝ V (Fin 2)
s : AffineSubspace ℝ P
p₁ p₂ p₄ : P
hp₁ : p₁ ∈ s
hp₂ : p₂ ∈ s
hp₃p₄ : s.SOppSide p₁ p₄
⊢ False

Tactic:
exact hp₃p₄.left_not_mem hp₁

Result:
no goals

Proof state:
V : Type u_1
P : Type u_2
inst✝⁴ : NormedAddCommGroup V
inst✝³ : InnerProductSpace ℝ V
inst✝² : MetricSpace P
inst✝¹ : NormedAddTorsor V P
hd2 : Fact (finrank ℝ V = 2)
inst✝ : Oriented ℝ V (Fin 2)
s : AffineSubspace ℝ P
p₁ p₂ p₃ p₄ : P
hp₁ : p₁ ∈ s
hp₂ : p₂ ∈ s
hp₃p₄ : s.SOppSide p₃ p₄
⊢ (∡ p₁ p₄ p₂).sign = -(∡ p₁ p₃ p₂).sign

Tactic:
have hp₁p₃ : p₁ ≠ p₃ := by rintro rfl; exact hp₃p₄.left_not_mem hp₁

Result:
V : Type u_1
P : Type u_2
inst✝⁴ : NormedAddCommGroup V
inst✝³ : InnerProductSpace ℝ V
inst✝² : MetricSpace P
inst✝¹ : NormedAddTorsor V P
hd2 : Fact (finrank ℝ V = 2)
inst✝ : Oriented ℝ V (Fin 2)
s : AffineSubspace ℝ P
p₁ p₂ p₃ p₄ : P
hp₁ : p₁ ∈ s
hp₂ : p₂ ∈ s
hp₃p₄ : s.SOppSide p₃ p₄
hp₁p₃ : p₁ ≠ p₃
⊢ (∡ p₁ p₄ p₂).sign = -(∡ p₁ p₃ p₂).sign
-- Mathlib/Probability/Kernel/Composition/MapComap.lean
lemma comap_map_comm (κ : Kernel β γ) {f : α → β} {g : γ → δ}
    (hf : Measurable f) (hg : Measurable g) :
    comap (map κ g) f hf = map (comap κ f hf) g

Proof state:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
γ : Type u_4
δ : Type u_5
mγ : MeasurableSpace γ
mδ : MeasurableSpace δ
κ : Kernel β γ
f : α → β
g : γ → δ
hf : Measurable f
hg : Measurable g
⊢ (κ.map g).comap f hf = (κ.comap f hf).map g

Tactic:
ext x s _

Result:
case h.h
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
γ : Type u_4
δ : Type u_5
mγ : MeasurableSpace γ
mδ : MeasurableSpace δ
κ : Kernel β γ
f : α → β
g : γ → δ
hf : Measurable f
hg : Measurable g
x : α
s : Set δ
a✝ : MeasurableSet s
⊢ (((κ.map g).comap f hf) x) s = (((κ.comap f hf).map g) x) s

Proof state:
case h.h
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
γ : Type u_4
δ : Type u_5
mγ : MeasurableSpace γ
mδ : MeasurableSpace δ
κ : Kernel β γ
f : α → β
g : γ → δ
hf : Measurable f
hg : Measurable g
x : α
s : Set δ
a✝ : MeasurableSet s
⊢ (((κ.map g).comap f hf) x) s = (((κ.comap f hf).map g) x) s

Tactic:
rw [comap_apply, map_apply _ hg, map_apply _ hg, comap_apply]

Result:
no goals
-- Mathlib/LinearAlgebra/BilinearForm/Hom.lean
theorem compLeft_id (B : BilinForm R M) : B.compLeft LinearMap.id = B

Proof state:
case H
R : Type u_1
M : Type u_2
inst✝² : CommSemiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
B : BilinForm R M
x✝ y✝ : M
⊢ ((B.compLeft id) x✝) y✝ = (B x✝) y✝

Tactic:
rfl

Result:
no goals

Proof state:
R : Type u_1
M : Type u_2
inst✝² : CommSemiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
B : BilinForm R M
⊢ B.compLeft id = B

Tactic:
ext

Result:
case H
R : Type u_1
M : Type u_2
inst✝² : CommSemiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
B : BilinForm R M
x✝ y✝ : M
⊢ ((B.compLeft id) x✝) y✝ = (B x✝) y✝
-- Mathlib/Data/ENNReal/Inv.lean
theorem mul_inv_le_iff {x y z : ℝ≥0∞} (h1 : y ≠ 0) (h2 : y ≠ ∞) :
    x * y⁻¹ ≤ z ↔ x ≤ z * y

Proof state:
x y z : ℝ≥0∞
h1 : y ≠ 0
h2 : y ≠ ⊤
⊢ x * y⁻¹ ≤ z ↔ x ≤ z * y

Tactic:
rw [mul_comm, ENNReal.inv_mul_le_iff h1 h2, mul_comm]

Result:
no goals
-- Mathlib/Algebra/GroupWithZero/Pointwise/Finset.lean
lemma inv_op_smul_finset_distrib₀ (a : α) (s : Finset α) : (s <• a)⁻¹ = a⁻¹ • s⁻¹

Proof state:
case inl
α : Type u_1
inst✝¹ : GroupWithZero α
inst✝ : DecidableEq α
s : Finset α
⊢ (s <• 0)⁻¹ = 0⁻¹ •> s⁻¹

Tactic:
obtain rfl | hs := s.eq_empty_or_nonempty <;> simp [*]

Result:
no goals

Proof state:
case inr.h
α : Type u_1
inst✝¹ : GroupWithZero α
inst✝ : DecidableEq α
a : α
s : Finset α
ha : a ≠ 0
a✝ : α
⊢ a✝ ∈ (s <• a)⁻¹ ↔ a✝ ∈ a⁻¹ •> s⁻¹

Tactic:
simp only [mem_inv', ne_eq, MulOpposite.op_eq_zero_iff, not_false_eq_true, ←
inv_smul_mem_iff₀, MulOpposite.smul_eq_mul_unop, MulOpposite.unop_inv, MulOpposite.unop_op,
inv_eq_zero, inv_inv, smul_eq_mul, mul_inv_rev, ha]

Result:
no goals

Proof state:
case inr
α : Type u_1
inst✝¹ : GroupWithZero α
inst✝ : DecidableEq α
a : α
s : Finset α
ha : a ≠ 0
⊢ (s <• a)⁻¹ = a⁻¹ •> s⁻¹

Tactic:
ext

Result:
case inr.h
α : Type u_1
inst✝¹ : GroupWithZero α
inst✝ : DecidableEq α
a : α
s : Finset α
ha : a ≠ 0
a✝ : α
⊢ a✝ ∈ (s <• a)⁻¹ ↔ a✝ ∈ a⁻¹ •> s⁻¹

Proof state:
α : Type u_1
inst✝¹ : GroupWithZero α
inst✝ : DecidableEq α
a : α
s : Finset α
⊢ (s <• a)⁻¹ = a⁻¹ •> s⁻¹

Tactic:
obtain rfl | ha := eq_or_ne a 0

Result:
case inl
α : Type u_1
inst✝¹ : GroupWithZero α
inst✝ : DecidableEq α
s : Finset α
⊢ (s <• 0)⁻¹ = 0⁻¹ •> s⁻¹

case inr
α : Type u_1
inst✝¹ : GroupWithZero α
inst✝ : DecidableEq α
a : α
s : Finset α
ha : a ≠ 0
⊢ (s <• a)⁻¹ = a⁻¹ •> s⁻¹
-- Mathlib/Topology/MetricSpace/Thickening.lean
theorem thickening_subset_cthickening (δ : ℝ) (E : Set α) : thickening δ E ⊆ cthickening δ E

Proof state:
α : Type u
inst✝ : PseudoEMetricSpace α
δ : ℝ
E : Set α
x : α
hx : x ∈ thickening δ E
⊢ x ∈ cthickening δ E

Tactic:
rw [thickening, mem_setOf_eq] at hx

Result:
α : Type u
inst✝ : PseudoEMetricSpace α
δ : ℝ
E : Set α
x : α
hx : infEdist x E < ENNReal.ofReal δ
⊢ x ∈ cthickening δ E

Proof state:
α : Type u
inst✝ : PseudoEMetricSpace α
δ : ℝ
E : Set α
⊢ thickening δ E ⊆ cthickening δ E

Tactic:
intro x hx

Result:
α : Type u
inst✝ : PseudoEMetricSpace α
δ : ℝ
E : Set α
x : α
hx : x ∈ thickening δ E
⊢ x ∈ cthickening δ E

Proof state:
α : Type u
inst✝ : PseudoEMetricSpace α
δ : ℝ
E : Set α
x : α
hx : infEdist x E < ENNReal.ofReal δ
⊢ x ∈ cthickening δ E

Tactic:
exact hx.le

Result:
no goals
-- Mathlib/RingTheory/TensorProduct/Basic.lean
theorem lift_comp_includeLeft (f : A →ₐ[S] C) (g : B →ₐ[R] C) (hfg : ∀ x y, Commute (f x) (g y)) :
    (lift f g hfg).comp includeLeft = f :=
  AlgHom.ext <| by simp

Proof state:
R : Type uR
S : Type uS
A : Type uA
B : Type uB
C : Type uC
inst✝¹² : CommSemiring R
inst✝¹¹ : CommSemiring S
inst✝¹⁰ : Algebra R S
inst✝⁹ : Semiring A
inst✝⁸ : Algebra R A
inst✝⁷ : Algebra S A
inst✝⁶ : IsScalarTower R S A
inst✝⁵ : Semiring B
inst✝⁴ : Algebra R B
inst✝³ : Semiring C
inst✝² : Algebra S C
inst✝¹ : Algebra R C
inst✝ : IsScalarTower R S C
f : A →ₐ[S] C
g : B →ₐ[R] C
hfg : ∀ (x : A) (y : B), Commute (f x) (g y)
⊢ ∀ (x : A), ((lift f g hfg).comp includeLeft) x = f x

Tactic:
simp

Result:
no goals
-- Mathlib/RingTheory/LocalProperties/Submodule.lean
theorem Module.eq_zero_of_isLocalized_span (x : M) (h : ∀ r : s, f r x = 0) : x = 0 :=
  eq_of_isLocalized_span s span_eq _ f x 0 <| by simpa only [map_zero] using h

Proof state:
R : Type u_1
M : Type u_2
inst✝⁵ : CommSemiring R
inst✝⁴ : AddCommMonoid M
inst✝³ : Module R M
s : Set R
span_eq : span s = ⊤
Mₚ : ↑s → Type u_5
inst✝² : (r : ↑s) → AddCommMonoid (Mₚ r)
inst✝¹ : (r : ↑s) → Module R (Mₚ r)
f : (r : ↑s) → M →ₗ[R] Mₚ r
inst✝ : ∀ (r : ↑s), IsLocalizedModule (Submonoid.powers ↑r) (f r)
x : M
h : ∀ (r : ↑s), (f r) x = 0
⊢ ∀ (r : ↑s), (f r) x = (f r) 0

Tactic:
simpa only [map_zero] using h

Result:
no goals
-- Mathlib/Algebra/Order/GroupWithZero/Unbundled.lean
theorem le_mul_of_one_le_right [PosMulMono α] (ha : 0 ≤ a) (h : 1 ≤ b) : a ≤ a * b

Proof state:
α : Type u_3
a b : α
inst✝³ : MulOneClass α
inst✝² : Zero α
inst✝¹ : Preorder α
inst✝ : PosMulMono α
ha : 0 ≤ a
h : 1 ≤ b
⊢ a ≤ a * b

Tactic:
simpa only [mul_one] using mul_le_mul_of_nonneg_left h ha

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/List/Control.lean
theorem foldlM_cons [Monad m] (f : β → α → m β) (b) (a) (l : List α) :
    (a :: l).foldlM f b = f b a >>= l.foldlM f

Proof state:
m : Type u_1 → Type u_2
β : Type u_1
α : Type u_3
inst✝ : Monad m
f : β → α → m β
b : β
a : α
l : List α
⊢ List.foldlM f b (a :: l) = do
    let init ← f b a
    List.foldlM f init l

Tactic:
simp [List.foldlM]

Result:
no goals
-- Mathlib/CategoryTheory/SmallObject/Iteration/Basic.lean
lemma w :
    F.map (homOfLE h₁₂ : ⟨k₁, h₁₂.trans h₂⟩ ⟶ ⟨k₂, h₂⟩) =
      eqToHom (by rw [h.src]) ≫ G.map (homOfLE h₁₂ : ⟨k₁, h₁₂.trans h₂⟩ ⟶ ⟨k₂, h₂⟩) ≫
        eqToHom (by rw [h.tgt])

Proof state:
C : Type u
inst✝¹ : Category.{v, u} C
K : Type w
inst✝ : LinearOrder K
x : K
F G : ↑(Set.Iic x) ⥤ C
k₁ k₂ : K
h₁₂ : k₁ ≤ k₂
h₂ : k₂ ≤ x
h : MapEq F G k₁ k₂ h₁₂ h₂
this :
  ∃ (hX : F.obj ⟨k₁, ⋯⟩ = G.obj ⟨k₁, ⋯⟩) (hY : F.obj ⟨k₂, h₂⟩ = G.obj ⟨k₂, h₂⟩),
    F.map (homOfLE h₁₂) = eqToHom hX ≫ G.map (homOfLE h₁₂) ≫ eqToHom ⋯
⊢ F.map (homOfLE h₁₂) = eqToHom ⋯ ≫ G.map (homOfLE h₁₂) ≫ eqToHom ⋯

Tactic:
tauto

Result:
no goals

Proof state:
C : Type u
inst✝¹ : Category.{v, u} C
K : Type w
inst✝ : LinearOrder K
x : K
F G : ↑(Set.Iic x) ⥤ C
k₁ k₂ : K
h₁₂ : k₁ ≤ k₂
h₂ : k₂ ≤ x
h : MapEq F G k₁ k₂ h₁₂ h₂
⊢ F.map (homOfLE h₁₂) = eqToHom ⋯ ≫ G.map (homOfLE h₁₂) ≫ eqToHom ⋯

Tactic:
have := (Arrow.mk_eq_mk_iff _ _).1 h

Result:
C : Type u
inst✝¹ : Category.{v, u} C
K : Type w
inst✝ : LinearOrder K
x : K
F G : ↑(Set.Iic x) ⥤ C
k₁ k₂ : K
h₁₂ : k₁ ≤ k₂
h₂ : k₂ ≤ x
h : MapEq F G k₁ k₂ h₁₂ h₂
this :
  ∃ (hX : F.obj ⟨k₁, ⋯⟩ = G.obj ⟨k₁, ⋯⟩) (hY : F.obj ⟨k₂, h₂⟩ = G.obj ⟨k₂, h₂⟩),
    F.map (homOfLE h₁₂) = eqToHom hX ≫ G.map (homOfLE h₁₂) ≫ eqToHom ⋯
⊢ F.map (homOfLE h₁₂) = eqToHom ⋯ ≫ G.map (homOfLE h₁₂) ≫ eqToHom ⋯

Proof state:
C : Type u
inst✝⁶ : Category.{v, u} C
J : Type w
Φ : SuccStruct C
inst✝⁵ : LinearOrder J
inst✝⁴ : SuccOrder J
inst✝³ : OrderBot J
inst✝² : HasIterationOfShape J C
inst✝¹ : WellFoundedLT J
j : J
K : Type w
inst✝ : LinearOrder K
x : K
F G : ↑(Set.Iic x) ⥤ C
k₁ k₂ : K
h₁₂ : k₁ ≤ k₂
h₂ : k₂ ≤ x
h : MapEq F G k₁ k₂ h₁₂ h₂
⊢ G.obj ⟨k₂, h₂⟩ = F.obj ⟨k₂, h₂⟩

Tactic:
rw [h.tgt]

Result:
no goals

Proof state:
C : Type u
inst✝⁶ : Category.{v, u} C
J : Type w
Φ : SuccStruct C
inst✝⁵ : LinearOrder J
inst✝⁴ : SuccOrder J
inst✝³ : OrderBot J
inst✝² : HasIterationOfShape J C
inst✝¹ : WellFoundedLT J
j : J
K : Type w
inst✝ : LinearOrder K
x : K
F G : ↑(Set.Iic x) ⥤ C
k₁ k₂ : K
h₁₂ : k₁ ≤ k₂
h₂ : k₂ ≤ x
h : MapEq F G k₁ k₂ h₁₂ h₂
⊢ F.obj ⟨k₁, ⋯⟩ = G.obj ⟨k₁, ⋯⟩

Tactic:
rw [h.src]

Result:
no goals
-- Mathlib/Algebra/Polynomial/Derivation.lean
theorem comp_aeval_eq (d : Derivation R A M) (f : R[X]) :
    d (aeval a f) = aeval a (derivative f) • d a :=
  calc
    _ = (AEval.of R M a).symm (d.compAEval a f) := rfl
    _ = _

Proof state:
R : Type u_1
A : Type u_2
M : Type u_3
inst✝⁶ : CommSemiring R
inst✝⁵ : CommSemiring A
inst✝⁴ : Algebra R A
inst✝³ : AddCommMonoid M
inst✝² : Module A M
inst✝¹ : Module R M
inst✝ : IsScalarTower R A M
a : A
d : Derivation R A M
f : R[X]
⊢ (AEval.of R M a).symm ((d.compAEval a) f) = (aeval a) (derivative f) • d a

Tactic:
simp [-compAEval_apply, compAEval_eq]

Result:
no goals
-- Mathlib/MeasureTheory/OuterMeasure/BorelCantelli.lean
theorem measure_limsup_atTop_eq_zero {s : ℕ → Set α} (hs : ∑' i, μ (s i) ≠ ∞) :
    μ (limsup s atTop) = 0

Proof state:
α : Type u_1
F : Type u_3
inst✝¹ : FunLike F (Set α) ℝ≥0∞
inst✝ : OuterMeasureClass F α
μ : F
s : ℕ → Set α
hs : ∑' (i : ℕ), μ (s i) ≠ ⊤
⊢ μ (limsup s atTop) = 0

Tactic:
rw [← Nat.cofinite_eq_atTop, measure_limsup_cofinite_eq_zero hs]

Result:
no goals
-- Mathlib/Algebra/Azumaya/Basic.lean
theorem of_AlgEquiv (e : A ≃ₐ[R] B) [IsAzumaya R A] : IsAzumaya R B :=
  let _ : Module.Projective R B := .of_equiv e.toLinearEquiv
  let _ : FaithfulSMul R B := .of_injective e e.injective
  let _ : Module.Finite R B := .equiv e.toLinearEquiv
  ⟨Function.Bijective.of_comp_iff (AlgHom.mulLeftRight R B)
    (Algebra.TensorProduct.congr e e.op).bijective |>.1 <| by
    rw [← AlgEquiv.coe_algHom, ← AlgHom.coe_comp, mulLeftRight_comp_congr]
    simp [AlgHom.mulLeftRight_bij]⟩

Proof state:
R : Type u_1
A : Type u_2
B : Type u_3
inst✝⁵ : CommSemiring R
inst✝⁴ : Ring A
inst✝³ : Ring B
inst✝² : Algebra R A
inst✝¹ : Algebra R B
e : A ≃ₐ[R] B
inst✝ : IsAzumaya R A
x✝² : Module.Projective R B := Module.Projective.of_equiv e.toLinearEquiv
x✝¹ : FaithfulSMul R B := FaithfulSMul.of_injective e (AlgEquiv.injective e)
x✝ : Module.Finite R B := Module.Finite.equiv e.toLinearEquiv
⊢ Function.Bijective (⇑(AlgHom.mulLeftRight R B) ∘ ⇑(Algebra.TensorProduct.congr e (AlgEquiv.op e)))

Tactic:
rw [← AlgEquiv.coe_algHom, ← AlgHom.coe_comp, mulLeftRight_comp_congr]

Result:
R : Type u_1
A : Type u_2
B : Type u_3
inst✝⁵ : CommSemiring R
inst✝⁴ : Ring A
inst✝³ : Ring B
inst✝² : Algebra R A
inst✝¹ : Algebra R B
e : A ≃ₐ[R] B
inst✝ : IsAzumaya R A
x✝² : Module.Projective R B := Module.Projective.of_equiv e.toLinearEquiv
x✝¹ : FaithfulSMul R B := FaithfulSMul.of_injective e (AlgEquiv.injective e)
x✝ : Module.Finite R B := Module.Finite.equiv e.toLinearEquiv
⊢ Function.Bijective ⇑((↑e.toLinearEquiv.algConj).comp (AlgHom.mulLeftRight R A))

Proof state:
R : Type u_1
A : Type u_2
B : Type u_3
inst✝⁵ : CommSemiring R
inst✝⁴ : Ring A
inst✝³ : Ring B
inst✝² : Algebra R A
inst✝¹ : Algebra R B
e : A ≃ₐ[R] B
inst✝ : IsAzumaya R A
x✝² : Module.Projective R B := Module.Projective.of_equiv e.toLinearEquiv
x✝¹ : FaithfulSMul R B := FaithfulSMul.of_injective e (AlgEquiv.injective e)
x✝ : Module.Finite R B := Module.Finite.equiv e.toLinearEquiv
⊢ Function.Bijective ⇑((↑e.toLinearEquiv.algConj).comp (AlgHom.mulLeftRight R A))

Tactic:
simp [AlgHom.mulLeftRight_bij]

Result:
no goals
-- Mathlib/Data/Set/Subsingleton.lean
theorem Subsingleton.induction_on {p : Set α → Prop} (hs : s.Subsingleton) (he : p ∅)
    (h₁ : ∀ x, p {x}) : p s

Proof state:
case inl
α : Type u
p : Set α → Prop
he : p ∅
h₁ : ∀ (x : α), p {x}
hs : ∅.Subsingleton
⊢ p ∅

case inr.intro
α : Type u
p : Set α → Prop
he : p ∅
h₁ : ∀ (x : α), p {x}
x : α
hs : {x}.Subsingleton
⊢ p {x}

Tactic:
exacts [he, h₁ _]

Result:
no goals

Proof state:
α : Type u
s : Set α
p : Set α → Prop
hs : s.Subsingleton
he : p ∅
h₁ : ∀ (x : α), p {x}
⊢ p s

Tactic:
rcases hs.eq_empty_or_singleton with (rfl | ⟨x, rfl⟩)

Result:
case inl
α : Type u
p : Set α → Prop
he : p ∅
h₁ : ∀ (x : α), p {x}
hs : ∅.Subsingleton
⊢ p ∅

case inr.intro
α : Type u
p : Set α → Prop
he : p ∅
h₁ : ∀ (x : α), p {x}
x : α
hs : {x}.Subsingleton
⊢ p {x}
-- Mathlib/GroupTheory/CommutingProbability.lean
theorem commProb_pi {α : Type*} (i : α → Type*) [Fintype α] [∀ a, Mul (i a)] :
    commProb (∀ a, i a) = ∏ a, commProb (i a)

Proof state:
α : Type u_2
i : α → Type u_3
inst✝¹ : Fintype α
inst✝ : (a : α) → Mul (i a)
⊢ commProb ((a : α) → i a) = ∏ a : α, commProb (i a)

Tactic:
simp_rw [commProb_def, Finset.prod_div_distrib, Finset.prod_pow, ← Nat.cast_prod,
  ← Nat.card_pi, Commute, SemiconjBy, funext_iff]

Result:
α : Type u_2
i : α → Type u_3
inst✝¹ : Fintype α
inst✝ : (a : α) → Mul (i a)
⊢ ↑(Nat.card { p // ∀ (x : α), (p.1 * p.2) x = (p.2 * p.1) x }) / ↑(Nat.card ((a : α) → i a)) ^ 2 =
    ↑(Nat.card ((a : α) → { p // p.1 * p.2 = p.2 * p.1 })) / ↑(Nat.card ((a : α) → i a)) ^ 2

Proof state:
case e_a.e_a
α : Type u_2
i : α → Type u_3
inst✝¹ : Fintype α
inst✝ : (a : α) → Mul (i a)
⊢ Nat.card { p // ∀ (x : α), (p.1 * p.2) x = (p.2 * p.1) x } = Nat.card ((a : α) → { p // p.1 * p.2 = p.2 * p.1 })

Tactic:
exact Nat.card_congr ⟨fun x a => ⟨⟨x.1.1 a, x.1.2 a⟩, x.2 a⟩, fun x => ⟨⟨fun a => (x a).1.1,
  fun a => (x a).1.2⟩, fun a => (x a).2⟩, fun x => rfl, fun x => rfl⟩

Result:
no goals

Proof state:
α : Type u_2
i : α → Type u_3
inst✝¹ : Fintype α
inst✝ : (a : α) → Mul (i a)
⊢ ↑(Nat.card { p // ∀ (x : α), (p.1 * p.2) x = (p.2 * p.1) x }) / ↑(Nat.card ((a : α) → i a)) ^ 2 =
    ↑(Nat.card ((a : α) → { p // p.1 * p.2 = p.2 * p.1 })) / ↑(Nat.card ((a : α) → i a)) ^ 2

Tactic:
congr 2

Result:
case e_a.e_a
α : Type u_2
i : α → Type u_3
inst✝¹ : Fintype α
inst✝ : (a : α) → Mul (i a)
⊢ Nat.card { p // ∀ (x : α), (p.1 * p.2) x = (p.2 * p.1) x } = Nat.card ((a : α) → { p // p.1 * p.2 = p.2 * p.1 })
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/List/Lemmas.lean
theorem foldr_hom (f : β₁ → β₂) (g₁ : α → β₁ → β₁) (g₂ : α → β₂ → β₂) (l : List α) (init : β₁)
    (H : ∀ x y, g₂ x (f y) = f (g₁ x y)) : l.foldr g₂ (f init) = f (l.foldr g₁ init)

Proof state:
β₁ : Type u_1
β₂ : Type u_2
α : Type u_3
f : β₁ → β₂
g₁ : α → β₁ → β₁
g₂ : α → β₂ → β₂
l : List α
init : β₁
H : ∀ (x : α) (y : β₁), g₂ x (f y) = f (g₁ x y)
⊢ foldr g₂ (f init) l = f (foldr g₁ init l)

Tactic:
induction l <;> simp [*, H]

Result:
no goals
-- Mathlib/RingTheory/DedekindDomain/Factorization.lean
theorem count_maximal (w : HeightOneSpectrum R) [Decidable (w = v)] :
    count K v (w.asIdeal : FractionalIdeal R⁰ K) = if w = v then 1 else 0

Proof state:
case pos
R : Type u_1
inst✝⁵ : CommRing R
K : Type u_2
inst✝⁴ : Field K
inst✝³ : Algebra R K
inst✝² : IsFractionRing R K
inst✝¹ : IsDedekindDomain R
v w : HeightOneSpectrum R
inst✝ : Decidable (w = v)
h : w = v
⊢ count K v ↑w.asIdeal = 1

Tactic:
rw [h, count_self]

Result:
no goals

Proof state:
case neg
R : Type u_1
inst✝⁵ : CommRing R
K : Type u_2
inst✝⁴ : Field K
inst✝³ : Algebra R K
inst✝² : IsFractionRing R K
inst✝¹ : IsDedekindDomain R
v w : HeightOneSpectrum R
inst✝ : Decidable (w = v)
h : ¬w = v
⊢ count K v ↑w.asIdeal = 0

Tactic:
exact count_maximal_coprime K v h

Result:
no goals

Proof state:
R : Type u_1
inst✝⁵ : CommRing R
K : Type u_2
inst✝⁴ : Field K
inst✝³ : Algebra R K
inst✝² : IsFractionRing R K
inst✝¹ : IsDedekindDomain R
v w : HeightOneSpectrum R
inst✝ : Decidable (w = v)
⊢ count K v ↑w.asIdeal = if w = v then 1 else 0

Tactic:
split_ifs with h

Result:
case pos
R : Type u_1
inst✝⁵ : CommRing R
K : Type u_2
inst✝⁴ : Field K
inst✝³ : Algebra R K
inst✝² : IsFractionRing R K
inst✝¹ : IsDedekindDomain R
v w : HeightOneSpectrum R
inst✝ : Decidable (w = v)
h : w = v
⊢ count K v ↑w.asIdeal = 1

case neg
R : Type u_1
inst✝⁵ : CommRing R
K : Type u_2
inst✝⁴ : Field K
inst✝³ : Algebra R K
inst✝² : IsFractionRing R K
inst✝¹ : IsDedekindDomain R
v w : HeightOneSpectrum R
inst✝ : Decidable (w = v)
h : ¬w = v
⊢ count K v ↑w.asIdeal = 0
-- Mathlib/Algebra/GeomSum.lean
theorem RingHom.map_geom_sum [Semiring α] [Semiring β] (x : α) (n : ℕ) (f : α →+* β) :
    f (∑ i ∈ range n, x ^ i) = ∑ i ∈ range n, f x ^ i

Proof state:
α : Type u
β : Type u_1
inst✝¹ : Semiring α
inst✝ : Semiring β
x : α
n : ℕ
f : α →+* β
⊢ f (∑ i ∈ range n, x ^ i) = ∑ i ∈ range n, f x ^ i

Tactic:
simp [map_sum f]

Result:
no goals
-- Mathlib/Algebra/Polynomial/Derivative.lean
theorem iterate_derivative_map [Semiring S] (p : R[X]) (f : R →+* S) (k : ℕ) :
    Polynomial.derivative^[k] (p.map f) = (Polynomial.derivative^[k] p).map f

Proof state:
case zero
R : Type u
S : Type v
inst✝¹ : Semiring R
inst✝ : Semiring S
f : R →+* S
p : R[X]
⊢ (⇑derivative)^[0] (map f p) = map f ((⇑derivative)^[0] p)

Tactic:
simp

Result:
no goals

Proof state:
R : Type u
S : Type v
inst✝¹ : Semiring R
inst✝ : Semiring S
p : R[X]
f : R →+* S
k : ℕ
⊢ (⇑derivative)^[k] (map f p) = map f ((⇑derivative)^[k] p)

Tactic:
induction' k with k ih generalizing p

Result:
case zero
R : Type u
S : Type v
inst✝¹ : Semiring R
inst✝ : Semiring S
f : R →+* S
p : R[X]
⊢ (⇑derivative)^[0] (map f p) = map f ((⇑derivative)^[0] p)

case succ
R : Type u
S : Type v
inst✝¹ : Semiring R
inst✝ : Semiring S
f : R →+* S
k : ℕ
ih : ∀ (p : R[X]), (⇑derivative)^[k] (map f p) = map f ((⇑derivative)^[k] p)
p : R[X]
⊢ (⇑derivative)^[k + 1] (map f p) = map f ((⇑derivative)^[k + 1] p)

Proof state:
case succ
R : Type u
S : Type v
inst✝¹ : Semiring R
inst✝ : Semiring S
f : R →+* S
k : ℕ
ih : ∀ (p : R[X]), (⇑derivative)^[k] (map f p) = map f ((⇑derivative)^[k] p)
p : R[X]
⊢ (⇑derivative)^[k + 1] (map f p) = map f ((⇑derivative)^[k + 1] p)

Tactic:
simp only [ih, Function.iterate_succ, Polynomial.derivative_map, Function.comp_apply]

Result:
no goals
-- Mathlib/MeasureTheory/Function/L1Space/Integrable.lean
theorem integrable_of_norm_sub_le {f₀ f₁ : α → β} {g : α → ℝ} (hf₁_m : AEStronglyMeasurable f₁ μ)
    (hf₀_i : Integrable f₀ μ) (hg_i : Integrable g μ) (h : ∀ᵐ a ∂μ, ‖f₀ a - f₁ a‖ ≤ g a) :
    Integrable f₁ μ :=
  haveI : ∀ᵐ a ∂μ, ‖f₁ a‖ ≤ ‖f₀ a‖ + g a

Proof state:
α : Type u_1
β : Type u_2
m : MeasurableSpace α
μ : Measure α
inst✝ : NormedAddCommGroup β
f₀ f₁ : α → β
g : α → ℝ
hf₁_m : AEStronglyMeasurable f₁ μ
hf₀_i : Integrable f₀ μ
hg_i : Integrable g μ
h : ∀ᵐ (a : α) ∂μ, ‖f₀ a - f₁ a‖ ≤ g a
⊢ ∀ (x : α), ‖f₀ x - f₁ x‖ ≤ g x → ‖f₁ x‖ ≤ ‖f₀ x‖ + g x

Tactic:
intro a ha

Result:
α : Type u_1
β : Type u_2
m : MeasurableSpace α
μ : Measure α
inst✝ : NormedAddCommGroup β
f₀ f₁ : α → β
g : α → ℝ
hf₁_m : AEStronglyMeasurable f₁ μ
hf₀_i : Integrable f₀ μ
hg_i : Integrable g μ
h : ∀ᵐ (a : α) ∂μ, ‖f₀ a - f₁ a‖ ≤ g a
a : α
ha : ‖f₀ a - f₁ a‖ ≤ g a
⊢ ‖f₁ a‖ ≤ ‖f₀ a‖ + g a

Proof state:
α : Type u_1
β : Type u_2
m : MeasurableSpace α
μ : Measure α
inst✝ : NormedAddCommGroup β
f₀ f₁ : α → β
g : α → ℝ
hf₁_m : AEStronglyMeasurable f₁ μ
hf₀_i : Integrable f₀ μ
hg_i : Integrable g μ
h : ∀ᵐ (a : α) ∂μ, ‖f₀ a - f₁ a‖ ≤ g a
a : α
ha : ‖f₀ a - f₁ a‖ ≤ g a
⊢ ‖f₁ a‖ ≤ ‖f₀ a‖ + g a

Tactic:
calc
  ‖f₁ a‖ ≤ ‖f₀ a‖ + ‖f₀ a - f₁ a‖ := norm_le_insert _ _
  _ ≤ ‖f₀ a‖ + g a := add_le_add_left ha _

Result:
no goals

Proof state:
α : Type u_1
β : Type u_2
m : MeasurableSpace α
μ : Measure α
inst✝ : NormedAddCommGroup β
f₀ f₁ : α → β
g : α → ℝ
hf₁_m : AEStronglyMeasurable f₁ μ
hf₀_i : Integrable f₀ μ
hg_i : Integrable g μ
h : ∀ᵐ (a : α) ∂μ, ‖f₀ a - f₁ a‖ ≤ g a
⊢ ∀ᵐ (a : α) ∂μ, ‖f₁ a‖ ≤ ‖f₀ a‖ + g a

Tactic:
apply h.mono

Result:
α : Type u_1
β : Type u_2
m : MeasurableSpace α
μ : Measure α
inst✝ : NormedAddCommGroup β
f₀ f₁ : α → β
g : α → ℝ
hf₁_m : AEStronglyMeasurable f₁ μ
hf₀_i : Integrable f₀ μ
hg_i : Integrable g μ
h : ∀ᵐ (a : α) ∂μ, ‖f₀ a - f₁ a‖ ≤ g a
⊢ ∀ (x : α), ‖f₀ x - f₁ x‖ ≤ g x → ‖f₁ x‖ ≤ ‖f₀ x‖ + g x