harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/Order/WithBot.lean
@[simp] lemma map₂_top_right (f : α → β → γ) (a) : map₂ f a ⊤ = ⊤

Proof state:
α : Type u_1
β : Type u_2
γ : Type u_3
f : α → β → γ
a : WithTop α
⊢ map₂ f a ⊤ = ⊤

Tactic:
cases a <;> rfl

Result:
no goals
-- Mathlib/RingTheory/IntegralClosure/IsIntegralClosure/Basic.lean
theorem noZeroSMulDivisors [Algebra R A] [IsScalarTower R A B] [NoZeroSMulDivisors R B] :
    NoZeroSMulDivisors R A

Proof state:
R : Type u_1
A : Type u_2
B : Type u_3
inst✝⁸ : CommRing R
inst✝⁷ : CommRing A
inst✝⁶ : CommRing B
inst✝⁵ : Algebra R B
inst✝⁴ : Algebra A B
inst✝³ : IsIntegralClosure A R B
inst✝² : Algebra R A
inst✝¹ : IsScalarTower R A B
inst✝ : NoZeroSMulDivisors R B
⊢ NoZeroSMulDivisors R A

Tactic:
refine
  Function.Injective.noZeroSMulDivisors _ (IsIntegralClosure.algebraMap_injective A R B)
    (map_zero _) fun _ _ => ?_

Result:
R : Type u_1
A : Type u_2
B : Type u_3
inst✝⁸ : CommRing R
inst✝⁷ : CommRing A
inst✝⁶ : CommRing B
inst✝⁵ : Algebra R B
inst✝⁴ : Algebra A B
inst✝³ : IsIntegralClosure A R B
inst✝² : Algebra R A
inst✝¹ : IsScalarTower R A B
inst✝ : NoZeroSMulDivisors R B
x✝¹ : R
x✝ : A
⊢ (algebraMap A B) (x✝¹ • x✝) = x✝¹ • (algebraMap A B) x✝

Proof state:
R : Type u_1
A : Type u_2
B : Type u_3
inst✝⁸ : CommRing R
inst✝⁷ : CommRing A
inst✝⁶ : CommRing B
inst✝⁵ : Algebra R B
inst✝⁴ : Algebra A B
inst✝³ : IsIntegralClosure A R B
inst✝² : Algebra R A
inst✝¹ : IsScalarTower R A B
inst✝ : NoZeroSMulDivisors R B
x✝¹ : R
x✝ : A
⊢ (algebraMap A B) (x✝¹ • x✝) = x✝¹ • (algebraMap A B) x✝

Tactic:
simp only [Algebra.algebraMap_eq_smul_one, IsScalarTower.smul_assoc]

Result:
no goals
-- Mathlib/LinearAlgebra/CliffordAlgebra/Contraction.lean
theorem changeForm.associated_neg_proof [Invertible (2 : R)] :
    (QuadraticMap.associated (R := R) (M := M) (-Q)).toQuadraticMap = 0 - Q

Proof state:
R : Type u1
inst✝³ : CommRing R
M : Type u2
inst✝² : AddCommGroup M
inst✝¹ : Module R M
Q : QuadraticForm R M
inst✝ : Invertible 2
⊢ (QuadraticMap.associated (-Q)).toQuadraticMap = 0 - Q

Tactic:
simp [QuadraticMap.toQuadraticMap_associated]

Result:
no goals
-- Mathlib/Analysis/Calculus/FDeriv/Symmetric.lean
@[simp] lemma minSmoothness_eq_infty {n : WithTop ℕ∞} :
    minSmoothness 𝕜 n = ∞ ↔ (n = ∞ ∧ IsRCLikeNormedField 𝕜)

Proof state:
𝕜 : Type u_1
inst✝ : NontriviallyNormedField 𝕜
n : WithTop ℕ∞
⊢ minSmoothness 𝕜 n = ∞ ↔ n = ∞ ∧ IsRCLikeNormedField 𝕜

Tactic:
simp only [minSmoothness]

Result:
𝕜 : Type u_1
inst✝ : NontriviallyNormedField 𝕜
n : WithTop ℕ∞
⊢ (if IsRCLikeNormedField 𝕜 then n else ω) = ∞ ↔ n = ∞ ∧ IsRCLikeNormedField 𝕜

Proof state:
𝕜 : Type u_1
inst✝ : NontriviallyNormedField 𝕜
n : WithTop ℕ∞
⊢ (if IsRCLikeNormedField 𝕜 then n else ω) = ∞ ↔ n = ∞ ∧ IsRCLikeNormedField 𝕜

Tactic:
split_ifs with h <;> simp [h]

Result:
no goals
-- Mathlib/Data/TypeVec.lean
theorem nilFun_comp {α₀ : TypeVec 0} (f₀ : α₀ ⟹ Fin2.elim0) : nilFun ⊚ f₀ = f₀ :=
  funext fun x => by apply Fin2.elim0 x

Proof state:
α₀ : TypeVec.{u_1} 0
f₀ : α₀ ⟹ Fin2.elim0
x : Fin2 0
⊢ (nilFun ⊚ f₀) x = f₀ x

Tactic:
apply Fin2.elim0 x

Result:
no goals
-- Mathlib/Analysis/SpecialFunctions/Pow/Real.lean
lemma zpow_le_iff_le_log {n : ℤ} (hx : 0 < x) (hy : 0 < y) : x ^ n ≤ y ↔ n * log x ≤ log y

Proof state:
x y : ℝ
n : ℤ
hx : 0 < x
hy : 0 < y
⊢ x ^ n ≤ y ↔ ↑n * log x ≤ log y

Tactic:
rw [← rpow_le_iff_le_log hx hy, rpow_intCast]

Result:
no goals
-- Mathlib/Algebra/Group/Invertible/Defs.lean
theorem mul_left_eq_iff_eq_invOf_mul : c * a = b ↔ a = ⅟c * b

Proof state:
α : Type u
inst✝¹ : Monoid α
a b c : α
inst✝ : Invertible c
⊢ c * a = b ↔ a = ⅟c * b

Tactic:
rw [← mul_right_inj_of_invertible (c := ⅟c), invOf_mul_cancel_left]

Result:
no goals
-- Mathlib/Order/Minimal.lean
theorem maximal_mem_image_iff (ha : a ∈ s) : Maximal (· ∈ f '' s) (f a) ↔ Maximal (· ∈ s) a :=
  _root_.maximal_mem_image_monotone_iff ha (by simp [f.le_iff_le])

Proof state:
α : Type u_1
a : α
inst✝¹ : Preorder α
β : Type u_2
inst✝ : Preorder β
s : Set α
f : α ↪o β
ha : a ∈ s
⊢ ∀ ⦃x y : α⦄, x ∈ s → y ∈ s → (f x ≤ f y ↔ x ≤ y)

Tactic:
simp [f.le_iff_le]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Array/Erase.lean
theorem size_erase_le (a : α) (l : Array α) : (l.erase a).size ≤ l.size

Proof state:
case mk
α : Type u_1
inst✝ : BEq α
a : α
l : List α
⊢ ({ toList := l }.erase a).size ≤ { toList := l }.size

Tactic:
simpa using List.length_erase_le a l

Result:
no goals

Proof state:
α : Type u_1
inst✝ : BEq α
a : α
l : Array α
⊢ (l.erase a).size ≤ l.size

Tactic:
rcases l with ⟨l⟩

Result:
case mk
α : Type u_1
inst✝ : BEq α
a : α
l : List α
⊢ ({ toList := l }.erase a).size ≤ { toList := l }.size
-- Mathlib/Analysis/Convex/Join.lean
theorem convexJoin_singleton_right (s : Set E) (y : E) :
    convexJoin 𝕜 s {y} = ⋃ x ∈ s, segment 𝕜 x y

Proof state:
𝕜 : Type u_2
E : Type u_3
inst✝² : OrderedSemiring 𝕜
inst✝¹ : AddCommMonoid E
inst✝ : Module 𝕜 E
s : Set E
y : E
⊢ convexJoin 𝕜 s {y} = ⋃ x ∈ s, segment 𝕜 x y

Tactic:
simp [convexJoin]

Result:
no goals
-- Mathlib/CategoryTheory/CofilteredSystem.lean
theorem isMittagLeffler_iff_subset_range_comp : F.IsMittagLeffler ↔ ∀ j : J, ∃ (i : _) (f : i ⟶ j),
    ∀ ⦃k⦄ (g : k ⟶ i), range (F.map f) ⊆ range (F.map <| g ≫ f)

Proof state:
J : Type u
inst✝¹ : Category.{u_1, u} J
F : J ⥤ Type v
inst✝ : IsCofilteredOrEmpty J
⊢ F.IsMittagLeffler ↔ ∀ (j : J), ∃ i f, ∀ ⦃k : J⦄ (g : k ⟶ i), range (F.map f) ⊆ range (F.map (g ≫ f))

Tactic:
simp_rw [isMittagLeffler_iff_eventualRange, eventualRange_eq_iff]

Result:
no goals
-- Mathlib/CategoryTheory/Limits/Shapes/Terminal.lean
theorem hasTerminalChangeDiagram (h : HasLimit F₁) : HasLimit F₂ :=
  ⟨⟨⟨⟨limit F₁, by aesop_cat, by simp⟩,
    isLimitChangeEmptyCone C (limit.isLimit F₁) _ (eqToIso rfl)⟩⟩⟩

Proof state:
C : Type u₁
inst✝ : Category.{v₁, u₁} C
F₁ : Discrete PEmpty.{w + 1} ⥤ C
F₂ : Discrete PEmpty.{w' + 1} ⥤ C
h : HasLimit F₁
⊢ ∀ ⦃X Y : Discrete PEmpty.{w' + 1}⦄ (f : X ⟶ Y),
    ((Functor.const (Discrete PEmpty.{w' + 1})).obj (limit F₁)).map f ≫ id (Discrete.casesOn Y fun as => ⋯.elim) =
      id (Discrete.casesOn X fun as => ⋯.elim) ≫ F₂.map f

Tactic:
simp

Result:
no goals

Proof state:
C : Type u₁
inst✝ : Category.{v₁, u₁} C
F₁ : Discrete PEmpty.{w + 1} ⥤ C
F₂ : Discrete PEmpty.{w' + 1} ⥤ C
h : HasLimit F₁
⊢ (X : Discrete PEmpty.{w' + 1}) → ((Functor.const (Discrete PEmpty.{w' + 1})).obj (limit F₁)).obj X ⟶ F₂.obj X

Tactic:
aesop_cat

Result:
no goals
-- Mathlib/Topology/Bornology/Absorbs.lean
protected lemma add [AddZeroClass E] [DistribSMul M E]
    (h₁ : Absorbs M s₁ t₁) (h₂ : Absorbs M s₂ t₂) : Absorbs M (s₁ + s₂) (t₁ + t₂) :=
  h₂.mp <| h₁.eventually.mono fun x hx₁ hx₂ ↦ by rw [smul_add]; exact add_subset_add hx₁ hx₂

Proof state:
M : Type u_1
E : Type u_2
inst✝² : Bornology M
s₁ s₂ t₁ t₂ : Set E
inst✝¹ : AddZeroClass E
inst✝ : DistribSMul M E
h₁ : Absorbs M s₁ t₁
h₂ : Absorbs M s₂ t₂
x : M
hx₁ : t₁ ⊆ x • s₁
hx₂ : t₂ ⊆ x • s₂
⊢ t₁ + t₂ ⊆ x • (s₁ + s₂)

Tactic:
rw [smul_add]

Result:
M : Type u_1
E : Type u_2
inst✝² : Bornology M
s₁ s₂ t₁ t₂ : Set E
inst✝¹ : AddZeroClass E
inst✝ : DistribSMul M E
h₁ : Absorbs M s₁ t₁
h₂ : Absorbs M s₂ t₂
x : M
hx₁ : t₁ ⊆ x • s₁
hx₂ : t₂ ⊆ x • s₂
⊢ t₁ + t₂ ⊆ x • s₁ + x • s₂

Proof state:
M : Type u_1
E : Type u_2
inst✝² : Bornology M
s₁ s₂ t₁ t₂ : Set E
inst✝¹ : AddZeroClass E
inst✝ : DistribSMul M E
h₁ : Absorbs M s₁ t₁
h₂ : Absorbs M s₂ t₂
x : M
hx₁ : t₁ ⊆ x • s₁
hx₂ : t₂ ⊆ x • s₂
⊢ t₁ + t₂ ⊆ x • s₁ + x • s₂

Tactic:
exact add_subset_add hx₁ hx₂

Result:
no goals
-- Mathlib/CategoryTheory/Monoidal/Functor.lean
theorem left_unitality_inv (X : C) :
    (λ_ (F.obj X)).inv ≫ ε F ▷ F.obj X ≫ μ F (𝟙_ C) X = F.map (λ_ X).inv

Proof state:
C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
inst✝³ : MonoidalCategory C
D : Type u₂
inst✝² : Category.{v₂, u₂} D
inst✝¹ : MonoidalCategory D
F : C ⥤ D
inst✝ : F.LaxMonoidal
X : C
⊢ (λ_ (F.obj X)).inv ≫ ε F ▷ F.obj X ≫ μ F (𝟙_ C) X = F.map (λ_ X).inv

Tactic:
rw [Iso.inv_comp_eq, left_unitality, Category.assoc, Category.assoc, ← F.map_comp,
  Iso.hom_inv_id, F.map_id, comp_id]

Result:
no goals
-- Mathlib/LinearAlgebra/TensorProduct/Basis.lean
theorem Basis.tensorProduct_apply' (b : Basis ι S M) (c : Basis κ R N) (i : ι × κ) :
    Basis.tensorProduct b c i = b i.1 ⊗ₜ c i.2

Proof state:
R : Type u_1
S : Type u_2
M : Type u_3
N : Type u_4
ι : Type u_5
κ : Type u_6
inst✝⁸ : CommSemiring R
inst✝⁷ : Semiring S
inst✝⁶ : Algebra R S
inst✝⁵ : AddCommMonoid M
inst✝⁴ : Module R M
inst✝³ : Module S M
inst✝² : IsScalarTower R S M
inst✝¹ : AddCommMonoid N
inst✝ : Module R N
b : Basis ι S M
c : Basis κ R N
i : ι × κ
⊢ (b.tensorProduct c) i = b i.1 ⊗ₜ[R] c i.2

Tactic:
simp [Basis.tensorProduct]

Result:
no goals
-- Mathlib/.lake/packages/batteries/Batteries/Classes/Order.lean
theorem LTCmp.cmp_iff_gt [LT α] [LTCmp (α := α) cmp] : cmp x y = .gt ↔ y < x

Proof state:
α : Type u_1
cmp : α → α → Ordering
x y : α
inst✝¹ : LT α
inst✝ : LTCmp cmp
⊢ cmp x y = Ordering.gt ↔ y < x

Tactic:
rw [OrientedCmp.cmp_eq_gt, LTCmp.cmp_iff_lt]

Result:
no goals
-- Mathlib/CategoryTheory/Generator/Basic.lean
theorem isSeparating_unop_iff (𝒢 : Set Cᵒᵖ) : IsSeparating 𝒢.unop ↔ IsCoseparating 𝒢

Proof state:
C : Type u₁
inst✝ : Category.{v₁, u₁} C
𝒢 : Set Cᵒᵖ
⊢ IsSeparating 𝒢.unop ↔ IsCoseparating 𝒢

Tactic:
rw [← isCoseparating_op_iff, Set.unop_op]

Result:
no goals
-- Mathlib/Topology/Separation/GDelta.lean
theorem Set.Countable.isGδ_compl {s : Set X} [T1Space X] (hs : s.Countable) : IsGδ sᶜ

Proof state:
X : Type u_1
inst✝¹ : TopologicalSpace X
s : Set X
inst✝ : T1Space X
hs : s.Countable
⊢ IsGδ (⋂ i ∈ s, {i}ᶜ)

Tactic:
exact .biInter hs fun x _ => .compl_singleton x

Result:
no goals

Proof state:
X : Type u_1
inst✝¹ : TopologicalSpace X
s : Set X
inst✝ : T1Space X
hs : s.Countable
⊢ IsGδ sᶜ

Tactic:
rw [← biUnion_of_singleton s, compl_iUnion₂]

Result:
X : Type u_1
inst✝¹ : TopologicalSpace X
s : Set X
inst✝ : T1Space X
hs : s.Countable
⊢ IsGδ (⋂ i ∈ s, {i}ᶜ)
-- Mathlib/NumberTheory/ModularForms/SlashActions.lean
theorem zero_slash (k : ℤ) (A : GL(2, ℝ)⁺) : (0 : ℍ → ℂ) ∣[k]A = 0 :=
  funext fun _ => by simp only [slash, Pi.zero_apply, zero_mul]

Proof state:
k : ℤ
A : ↥GL(2, ℝ)⁺
x✝ : ℍ
⊢ (0 ∣[k]A) x✝ = 0 x✝

Tactic:
simp only [slash, Pi.zero_apply, zero_mul]

Result:
no goals
-- Mathlib/Algebra/BigOperators/Finsupp.lean
theorem if_mem_support [DecidableEq α] {N : Type*} [AddCommMonoid N] (f : α →₀ N) (a : α) :
    (if a ∈ f.support then f a else 0) = f a

Proof state:
α : Type u_1
inst✝¹ : DecidableEq α
N : Type u_16
inst✝ : AddCommMonoid N
f : α →₀ N
a : α
⊢ f a = 0 → 0 = f a

Tactic:
exact fun h ↦ h.symm

Result:
no goals

Proof state:
α : Type u_1
inst✝¹ : DecidableEq α
N : Type u_16
inst✝ : AddCommMonoid N
f : α →₀ N
a : α
⊢ (if a ∈ f.support then f a else 0) = f a

Tactic:
simp only [mem_support_iff, ne_eq, ite_eq_left_iff, not_not]

Result:
α : Type u_1
inst✝¹ : DecidableEq α
N : Type u_16
inst✝ : AddCommMonoid N
f : α →₀ N
a : α
⊢ f a = 0 → 0 = f a
-- Mathlib/Algebra/Order/Ring/Abs.lean
lemma abs_neg_one_pow (n : ℕ) : |(-1 : α) ^ n| = 1

Proof state:
α : Type u_1
inst✝ : LinearOrderedRing α
n : ℕ
⊢ |(-1) ^ n| = 1

Tactic:
rw [← pow_abs, abs_neg, abs_one, one_pow]

Result:
no goals
-- Mathlib/Data/Int/Init.lean
lemma le_add_iff_lt_of_dvd_sub (ha : 0 < a) (hab : a ∣ c - b) : a + b ≤ c ↔ b < c

Proof state:
a b c : ℤ
ha : 0 < a
hab : a ∣ c - b
⊢ a + b ≤ c ↔ b < c

Tactic:
rw [Int.add_le_iff_le_sub, ← Int.sub_pos, le_iff_pos_of_dvd ha hab]

Result:
no goals
-- Mathlib/Analysis/Seminorm.lean
theorem ball_zero_eq_preimage_ball {r : ℝ} : p.ball 0 r = p ⁻¹' Metric.ball 0 r

Proof state:
𝕜 : Type u_3
E : Type u_7
inst✝² : SeminormedRing 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
p : Seminorm 𝕜 E
r : ℝ
⊢ p.ball 0 r = ⇑p ⁻¹' Metric.ball 0 r

Tactic:
rw [ball_zero_eq, preimage_metric_ball]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Array/Erase.lean
theorem eraseP_ne_empty_iff {xs : Array α} {p : α → Bool} : xs.eraseP p ≠ #[] ↔ xs ≠ #[] ∧ ∀ x, p x → xs ≠ #[x]

Proof state:
α : Type u_1
xs : Array α
p : α → Bool
⊢ xs.eraseP p ≠ #[] ↔ xs ≠ #[] ∧ ∀ (x : α), p x = true → xs ≠ #[x]

Tactic:
simp

Result:
no goals
-- Mathlib/Data/Sum/Interval.lean
lemma sumLexLift_nonempty :
    (sumLexLift f₁ f₂ g₁ g₂ a b).Nonempty ↔
      (∃ a₁ b₁, a = inl a₁ ∧ b = inl b₁ ∧ (f₁ a₁ b₁).Nonempty) ∨
        (∃ a₁ b₂, a = inl a₁ ∧ b = inr b₂ ∧ ((g₁ a₁ b₂).Nonempty ∨ (g₂ a₁ b₂).Nonempty)) ∨
          ∃ a₂ b₂, a = inr a₂ ∧ b = inr b₂ ∧ (f₂ a₂ b₂).Nonempty

Proof state:
α₁ : Type u_1
α₂ : Type u_2
β₁ : Type u_3
β₂ : Type u_4
γ₁ : Type u_5
γ₂ : Type u_6
f₁ : α₁ → β₁ → Finset γ₁
f₂ : α₂ → β₂ → Finset γ₂
g₁ : α₁ → β₂ → Finset γ₁
g₂ : α₁ → β₂ → Finset γ₂
a : α₁ ⊕ α₂
b : β₁ ⊕ β₂
⊢ (sumLexLift f₁ f₂ g₁ g₂ a b).Nonempty ↔
    (∃ a₁ b₁, a = inl a₁ ∧ b = inl b₁ ∧ (f₁ a₁ b₁).Nonempty) ∨
      (∃ a₁ b₂, a = inl a₁ ∧ b = inr b₂ ∧ ((g₁ a₁ b₂).Nonempty ∨ (g₂ a₁ b₂).Nonempty)) ∨
        ∃ a₂ b₂, a = inr a₂ ∧ b = inr b₂ ∧ (f₂ a₂ b₂).Nonempty

Tactic:
simp only [nonempty_iff_ne_empty, Ne, sumLexLift_eq_empty, not_and_or, exists_prop,
  not_forall]

Result:
no goals
-- Mathlib/MeasureTheory/Function/ConditionalExpectation/CondexpL1.lean
theorem condExpL1CLM_indicatorConst (hs : MeasurableSet s) (hμs : μ s ≠ ∞) (x : F') :
    (condExpL1CLM F' hm μ) ↑(simpleFunc.indicatorConst 1 hs hμs x) = condExpInd F' hm μ s x

Proof state:
α : Type u_1
F' : Type u_3
inst✝³ : NormedAddCommGroup F'
inst✝² : NormedSpace ℝ F'
inst✝¹ : CompleteSpace F'
m m0 : MeasurableSpace α
μ : Measure α
hm : m ≤ m0
inst✝ : SigmaFinite (μ.trim hm)
s : Set α
hs : MeasurableSet s
hμs : μ s ≠ ⊤
x : F'
⊢ (condExpL1CLM F' hm μ) (indicatorConstLp 1 hs hμs x) = (condExpInd F' hm μ s) x

Tactic:
exact condExpL1CLM_indicatorConstLp hs hμs x

Result:
no goals

Proof state:
α : Type u_1
F' : Type u_3
inst✝³ : NormedAddCommGroup F'
inst✝² : NormedSpace ℝ F'
inst✝¹ : CompleteSpace F'
m m0 : MeasurableSpace α
μ : Measure α
hm : m ≤ m0
inst✝ : SigmaFinite (μ.trim hm)
s : Set α
hs : MeasurableSet s
hμs : μ s ≠ ⊤
x : F'
⊢ (condExpL1CLM F' hm μ) ↑(simpleFunc.indicatorConst 1 hs hμs x) = (condExpInd F' hm μ s) x

Tactic:
rw [Lp.simpleFunc.coe_indicatorConst]

Result:
α : Type u_1
F' : Type u_3
inst✝³ : NormedAddCommGroup F'
inst✝² : NormedSpace ℝ F'
inst✝¹ : CompleteSpace F'
m m0 : MeasurableSpace α
μ : Measure α
hm : m ≤ m0
inst✝ : SigmaFinite (μ.trim hm)
s : Set α
hs : MeasurableSet s
hμs : μ s ≠ ⊤
x : F'
⊢ (condExpL1CLM F' hm μ) (indicatorConstLp 1 hs hμs x) = (condExpInd F' hm μ s) x
-- Mathlib/Probability/Kernel/Composition/MapComap.lean
lemma map_apply_eq_iff_map_symm_apply_eq (κ : Kernel α β) {f : β ≃ᵐ γ} (η : Kernel α γ) :
    κ.map f = η ↔ κ = η.map f.symm

Proof state:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
γ : Type u_4
mγ : MeasurableSpace γ
κ : Kernel α β
f : β ≃ᵐ γ
η : Kernel α γ
⊢ κ.map ⇑f = η ↔ κ = η.map ⇑f.symm

Tactic:
simp_rw [Kernel.ext_iff, map_apply _ f.measurable, map_apply _ f.symm.measurable,
  f.map_apply_eq_iff_map_symm_apply_eq]

Result:
no goals
-- Mathlib/Analysis/Complex/Angle.lean
lemma angle_exp_exp (x y : ℝ) :
    angle (exp (x * I)) (exp (y * I)) = |toIocMod Real.two_pi_pos (-π) (x - y)|

Proof state:
x y : ℝ
⊢ angle (cexp (↑x * I)) (cexp (↑y * I)) = |toIocMod Real.two_pi_pos (-π) (x - y)|

Tactic:
simp_rw [angle_eq_abs_arg (exp_ne_zero _) (exp_ne_zero _), ← exp_sub, ← sub_mul, ← ofReal_sub,
  arg_exp_mul_I]

Result:
no goals
-- Mathlib/Algebra/Order/Monovary.lean
@[to_additive (attr := simp)]
lemma monovaryOn_inv_right : MonovaryOn f g⁻¹ s ↔ AntivaryOn f g s

Proof state:
ι : Type u_1
α : Type u_2
β : Type u_3
inst✝¹ : OrderedCommGroup α
inst✝ : OrderedCommGroup β
s : Set ι
f : ι → α
g : ι → β
⊢ MonovaryOn f g⁻¹ s ↔ AntivaryOn f g s

Tactic:
simpa [MonovaryOn, AntivaryOn] using forall₂_swap

Result:
no goals
-- Mathlib/Combinatorics/SimpleGraph/Clique.lean
theorem IsClique.map (h : G.IsClique s) {f : α ↪ β} : (G.map f).IsClique (f '' s)

Proof state:
α : Type u_1
β : Type u_2
G : SimpleGraph α
s : Set α
h : G.IsClique s
f : α ↪ β
⊢ (SimpleGraph.map f G).IsClique (⇑f '' s)

Tactic:
rintro _ ⟨a, ha, rfl⟩ _ ⟨b, hb, rfl⟩ hab

Result:
case intro.intro.intro.intro
α : Type u_1
β : Type u_2
G : SimpleGraph α
s : Set α
h : G.IsClique s
f : α ↪ β
a : α
ha : a ∈ s
b : α
hb : b ∈ s
hab : f a ≠ f b
⊢ (SimpleGraph.map f G).Adj (f a) (f b)

Proof state:
case intro.intro.intro.intro
α : Type u_1
β : Type u_2
G : SimpleGraph α
s : Set α
h : G.IsClique s
f : α ↪ β
a : α
ha : a ∈ s
b : α
hb : b ∈ s
hab : f a ≠ f b
⊢ (SimpleGraph.map f G).Adj (f a) (f b)

Tactic:
exact ⟨a, b, h ha hb <| ne_of_apply_ne _ hab, rfl, rfl⟩

Result:
no goals
-- Mathlib/RingTheory/Algebraic/MvPolynomial.lean
theorem transcendental_polynomial_aeval_X_iff (i : σ) {f : R[X]} :
    Transcendental R (Polynomial.aeval (X i : MvPolynomial σ R) f) ↔ Transcendental R f

Proof state:
σ : Type u_1
R : Type u_2
inst✝ : CommRing R
i : σ
f : R[X]
⊢ Transcendental R ((Polynomial.aeval (X i)) f) → Transcendental R f

Tactic:
simp_rw [Transcendental, not_imp_not]

Result:
σ : Type u_1
R : Type u_2
inst✝ : CommRing R
i : σ
f : R[X]
⊢ IsAlgebraic R f → IsAlgebraic R ((Polynomial.aeval (X i)) f)

Proof state:
σ : Type u_1
R : Type u_2
inst✝ : CommRing R
i : σ
f : R[X]
⊢ Transcendental R ((Polynomial.aeval (X i)) f) ↔ Transcendental R f

Tactic:
refine ⟨?_, transcendental_polynomial_aeval_X R i⟩

Result:
σ : Type u_1
R : Type u_2
inst✝ : CommRing R
i : σ
f : R[X]
⊢ Transcendental R ((Polynomial.aeval (X i)) f) → Transcendental R f

Proof state:
σ : Type u_1
R : Type u_2
inst✝ : CommRing R
i : σ
f : R[X]
⊢ IsAlgebraic R f → IsAlgebraic R ((Polynomial.aeval (X i)) f)

Tactic:
exact fun h ↦ h.algHom _

Result:
no goals
-- Mathlib/MeasureTheory/Measure/NullMeasurable.lean
theorem measure_iUnion₀ [Countable ι] {f : ι → Set α} (hd : Pairwise (AEDisjoint μ on f))
    (h : ∀ i, NullMeasurableSet (f i) μ) : μ (⋃ i, f i) = ∑' i, μ (f i)

Proof state:
ι : Type u_1
α : Type u_2
m0 : MeasurableSpace α
μ : Measure α
inst✝ : Countable ι
f : ι → Set α
hd : Pairwise (AEDisjoint μ on f)
h : ∀ (i : ι), NullMeasurableSet (f i) μ
⊢ μ (⋃ i, f i) = ∑' (i : ι), μ (f i)

Tactic:
rcases exists_subordinate_pairwise_disjoint h hd with ⟨t, _ht_sub, ht_eq, htm, htd⟩

Result:
case intro.intro.intro.intro
ι : Type u_1
α : Type u_2
m0 : MeasurableSpace α
μ : Measure α
inst✝ : Countable ι
f : ι → Set α
hd : Pairwise (AEDisjoint μ on f)
h : ∀ (i : ι), NullMeasurableSet (f i) μ
t : ι → Set α
_ht_sub : ∀ (i : ι), t i ⊆ f i
ht_eq : ∀ (i : ι), f i =ᶠ[ae μ] t i
htm : ∀ (i : ι), MeasurableSet (t i)
htd : Pairwise (Disjoint on t)
⊢ μ (⋃ i, f i) = ∑' (i : ι), μ (f i)

Proof state:
case intro.intro.intro.intro
ι : Type u_1
α : Type u_2
m0 : MeasurableSpace α
μ : Measure α
inst✝ : Countable ι
f : ι → Set α
hd : Pairwise (AEDisjoint μ on f)
h : ∀ (i : ι), NullMeasurableSet (f i) μ
t : ι → Set α
_ht_sub : ∀ (i : ι), t i ⊆ f i
ht_eq : ∀ (i : ι), f i =ᶠ[ae μ] t i
htm : ∀ (i : ι), MeasurableSet (t i)
htd : Pairwise (Disjoint on t)
⊢ μ (⋃ i, f i) = ∑' (i : ι), μ (f i)

Tactic:
calc
  μ (⋃ i, f i) = μ (⋃ i, t i) := measure_congr (EventuallyEq.countable_iUnion ht_eq)
  _ = ∑' i, μ (t i) := measure_iUnion htd htm
  _ = ∑' i, μ (f i) := tsum_congr fun i => measure_congr (ht_eq _).symm

Result:
no goals
-- Mathlib/Algebra/Homology/Bifunctor.lean
@[reassoc (attr := simp)]
lemma ι_mapBifunctorMap (i₁ : I₁) (i₂ : I₂) (j : J)
    (h : ComplexShape.π c₁ c₂ c (i₁, i₂) = j) :
    ιMapBifunctor K₁ K₂ F c i₁ i₂ j h ≫ (mapBifunctorMap f₁ f₂ F c).f j =
      (F.map (f₁.f i₁)).app (K₂.X i₂) ≫ (F.obj (L₁.X i₁)).map (f₂.f i₂) ≫
        ιMapBifunctor L₁ L₂ F c i₁ i₂ j h

Proof state:
C₁ : Type u_1
C₂ : Type u_2
D : Type u_3
inst✝¹¹ : Category.{u_9, u_1} C₁
inst✝¹⁰ : Category.{u_8, u_2} C₂
inst✝⁹ : Category.{u_7, u_3} D
I₁ : Type u_4
I₂ : Type u_5
J : Type u_6
c₁ : ComplexShape I₁
c₂ : ComplexShape I₂
inst✝⁸ : HasZeroMorphisms C₁
inst✝⁷ : HasZeroMorphisms C₂
inst✝⁶ : Preadditive D
K₁ L₁ : HomologicalComplex C₁ c₁
K₂ L₂ : HomologicalComplex C₂ c₂
f₁ : K₁ ⟶ L₁
f₂ : K₂ ⟶ L₂
F : C₁ ⥤ C₂ ⥤ D
inst✝⁵ : F.PreservesZeroMorphisms
inst✝⁴ : ∀ (X₁ : C₁), (F.obj X₁).PreservesZeroMorphisms
c : ComplexShape J
inst✝³ : TotalComplexShape c₁ c₂ c
inst✝² : K₁.HasMapBifunctor K₂ F c
inst✝¹ : L₁.HasMapBifunctor L₂ F c
inst✝ : DecidableEq J
i₁ : I₁
i₂ : I₂
j : J
h : c₁.π c₂ c (i₁, i₂) = j
⊢ K₁.ιMapBifunctor K₂ F c i₁ i₂ j h ≫ (mapBifunctorMap f₁ f₂ F c).f j =
    (F.map (f₁.f i₁)).app (K₂.X i₂) ≫ (F.obj (L₁.X i₁)).map (f₂.f i₂) ≫ L₁.ιMapBifunctor L₂ F c i₁ i₂ j h

Tactic:
simp [mapBifunctorMap]

Result:
no goals
-- Mathlib/Analysis/Calculus/SmoothSeries.lean
theorem summable_of_summable_hasDerivAt (hu : Summable u)
    (hg : ∀ n y, HasDerivAt (g n) (g' n y) y) (hg' : ∀ n y, ‖g' n y‖ ≤ u n)
    (hg0 : Summable fun n => g n y₀) (y : 𝕜) : Summable fun n => g n y

Proof state:
α : Type u_1
𝕜 : Type u_3
F : Type u_5
inst✝⁴ : NontriviallyNormedField 𝕜
inst✝³ : IsRCLikeNormedField 𝕜
inst✝² : NormedAddCommGroup F
inst✝¹ : CompleteSpace F
u : α → ℝ
inst✝ : NormedSpace 𝕜 F
g g' : α → 𝕜 → F
y₀ : 𝕜
hu : Summable u
hg : ∀ (n : α) (y : 𝕜), HasDerivAt (g n) (g' n y) y
hg' : ∀ (n : α) (y : 𝕜), ‖g' n y‖ ≤ u n
hg0 : Summable fun n => g n y₀
y : 𝕜
⊢ Summable fun n => g n y

Tactic:
exact summable_of_summable_hasDerivAt_of_isPreconnected hu isOpen_univ isPreconnected_univ
  (fun n x _ => hg n x) (fun n x _ => hg' n x) (mem_univ _) hg0 (mem_univ _)

Result:
no goals
-- Mathlib/Data/ENNReal/Holder.lean
lemma le : r ≤ p

Proof state:
p q r : ℝ≥0∞
inst✝ : p.HolderTriple q r
⊢ r ≤ p

Tactic:
simp [← ENNReal.inv_le_inv, ← @inv_inv_add_inv p q r, inv_inv]

Result:
no goals
-- Mathlib/Algebra/Order/GroupWithZero/Unbundled.lean
/-- See `le_inv_mul_iff₀` for a version with multiplication on the other side. -/
lemma le_inv_mul_iff₀' (hc : 0 < c) : a ≤ c⁻¹ * b ↔ c * a ≤ b

Proof state:
G₀ : Type u_2
inst✝⁴ : CommGroupWithZero G₀
inst✝³ : PartialOrder G₀
inst✝² : ZeroLEOneClass G₀
inst✝¹ : PosMulReflectLT G₀
inst✝ : PosMulMono G₀
a b c : G₀
hc : 0 < c
⊢ a ≤ c⁻¹ * b ↔ c * a ≤ b

Tactic:
rw [le_inv_mul_iff₀ hc, mul_comm]

Result:
no goals
-- Mathlib/Probability/ProbabilityMassFunction/Constructions.lean
theorem support_map : (map f p).support = f '' p.support :=
  Set.ext fun b => by simp [map, @eq_comm β b]

Proof state:
α : Type u_1
β : Type u_2
f : α → β
p : PMF α
b : β
⊢ b ∈ (map f p).support ↔ b ∈ f '' p.support

Tactic:
simp [map, @eq_comm β b]

Result:
no goals
-- Mathlib/LinearAlgebra/Matrix/Determinant/Basic.lean
theorem det_mul_left_comm (M N P : Matrix m m R) : det (M * (N * P)) = det (N * (M * P))

Proof state:
m : Type u_1
inst✝² : DecidableEq m
inst✝¹ : Fintype m
R : Type v
inst✝ : CommRing R
M N P : Matrix m m R
⊢ (M * (N * P)).det = (N * (M * P)).det

Tactic:
rw [← Matrix.mul_assoc, ← Matrix.mul_assoc, det_mul, det_mul_comm M N, ← det_mul]

Result:
no goals
-- Mathlib/SetTheory/Ordinal/Arithmetic.lean
theorem exists_of_lt_bmex {o : Ordinal} {f : ∀ a < o, Ordinal} {a} (ha : a < bmex o f) :
    ∃ i hi, f i hi = a

Proof state:
o : Ordinal.{u_4}
f : (a : Ordinal.{u_4}) → a < o → Ordinal.{max u_4 u_5}
a : Ordinal.{max u_5 u_4}
ha : a < o.bmex f
⊢ ∃ i, ∃ (hi : i < o), f i hi = a

Tactic:
obtain ⟨i, hi⟩ := exists_of_lt_mex ha

Result:
case intro
o : Ordinal.{u_4}
f : (a : Ordinal.{u_4}) → a < o → Ordinal.{max u_4 u_5}
a : Ordinal.{max u_5 u_4}
ha : a < o.bmex f
i : o.toType
hi : o.familyOfBFamily f i = a
⊢ ∃ i, ∃ (hi : i < o), f i hi = a

Proof state:
case intro
o : Ordinal.{u_4}
f : (a : Ordinal.{u_4}) → a < o → Ordinal.{max u_4 u_5}
a : Ordinal.{max u_5 u_4}
ha : a < o.bmex f
i : o.toType
hi : o.familyOfBFamily f i = a
⊢ ∃ i, ∃ (hi : i < o), f i hi = a

Tactic:
exact ⟨_, typein_lt_self i, hi⟩

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Std/Data/DHashMap/Internal/List/Associative.lean
theorem getKey?_eq_some_getKey! [BEq α] [Inhabited α] {l : List ((a : α) × β a)} {a : α}
    (h : containsKey a l = true) :
    getKey? a l = some (getKey! a l)

Proof state:
α : Type u
β : α → Type v
inst✝¹ : BEq α
inst✝ : Inhabited α
l : List ((a : α) × β a)
a : α
h : containsKey a l = true
⊢ getKey? a l = some (getKey! a l)

Tactic:
rw [getKey?_eq_some_getKey h, getKey_eq_getKey!]

Result:
no goals