harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/LinearAlgebra/PerfectPairing/Basic.lean
@[simp]
lemma map_dualAnnihilator_linearEquiv_flip_symm (p : Submodule R N) :
    p.dualAnnihilator.map e.flip.symm = (p.map e).dualCoannihilator

Proof state:
R : Type u_1
M : Type u_2
N : Type u_3
inst✝⁵ : CommRing R
inst✝⁴ : AddCommGroup M
inst✝³ : Module R M
inst✝² : AddCommGroup N
inst✝¹ : Module R N
inst✝ : IsReflexive R M
e : N ≃ₗ[R] Dual R M
p : Submodule R N
this : IsReflexive R N
⊢ map e.flip.symm p.dualAnnihilator = (map e p).dualCoannihilator

Tactic:
rw [← dualCoannihilator_map_linearEquiv_flip, flip_flip]

Result:
no goals

Proof state:
R : Type u_1
M : Type u_2
N : Type u_3
inst✝⁵ : CommRing R
inst✝⁴ : AddCommGroup M
inst✝³ : Module R M
inst✝² : AddCommGroup N
inst✝¹ : Module R N
inst✝ : IsReflexive R M
e : N ≃ₗ[R] Dual R M
p : Submodule R N
⊢ map e.flip.symm p.dualAnnihilator = (map e p).dualCoannihilator

Tactic:
have : IsReflexive R N := e.isReflexive_of_equiv_dual_of_isReflexive

Result:
R : Type u_1
M : Type u_2
N : Type u_3
inst✝⁵ : CommRing R
inst✝⁴ : AddCommGroup M
inst✝³ : Module R M
inst✝² : AddCommGroup N
inst✝¹ : Module R N
inst✝ : IsReflexive R M
e : N ≃ₗ[R] Dual R M
p : Submodule R N
this : IsReflexive R N
⊢ map e.flip.symm p.dualAnnihilator = (map e p).dualCoannihilator
-- Mathlib/FieldTheory/LinearDisjoint.lean
theorem linearIndependent_mul' (H : A.LinearDisjoint L) {κ ι : Type*} {a : κ → A} {b : ι → L}
    (ha : LinearIndependent F a) (hb : LinearIndependent F b) :
    LinearIndependent F fun (i : κ × ι) ↦ (a i.1).1 * algebraMap L E (b i.2)

Proof state:
F : Type u
E : Type v
inst✝⁶ : Field F
inst✝⁵ : Field E
inst✝⁴ : Algebra F E
A : IntermediateField F E
L : Type w
inst✝³ : Field L
inst✝² : Algebra F L
inst✝¹ : Algebra L E
inst✝ : IsScalarTower F L E
H : A.LinearDisjoint L
κ : Type u_1
ι : Type u_2
a : κ → ↥A
b : ι → L
ha : LinearIndependent F a
hb : LinearIndependent F b
⊢ LinearIndependent F fun i => ↑(a i.1) * (algebraMap L E) (b i.2)

Tactic:
apply Subalgebra.LinearDisjoint.linearIndependent_mul_of_flat_left H ha <| hb.map' _
  (AlgEquiv.ofInjectiveField (IsScalarTower.toAlgHom F L E)).toLinearEquiv.ker

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/List/Nat/Range.lean
theorem enum_map_fst (l : List α) : map Prod.fst (enum l) = range l.length

Proof state:
α : Type u_1
l : List α
⊢ map Prod.fst l.enum = range l.length

Tactic:
simp only [enum, enumFrom_map_fst, range_eq_range']

Result:
no goals
-- Mathlib/Data/Ordmap/Ordset.lean
theorem dual_balance' (l : Ordnode α) (x : α) (r : Ordnode α) :
    dual (balance' l x r) = balance' (dual r) x (dual l)

Proof state:
α : Type u_1
l : Ordnode α
x : α
r : Ordnode α
⊢ (l.balance' x r).dual = r.dual.balance' x l.dual

Tactic:
simp [balance', add_comm]

Result:
α : Type u_1
l : Ordnode α
x : α
r : Ordnode α
⊢ (if l.size + r.size ≤ 1 then l.node' x r
      else
        if delta * l.size < r.size then l.rotateL x r
        else if delta * r.size < l.size then l.rotateR x r else l.node' x r).dual =
    if l.size + r.size ≤ 1 then r.dual.node' x l.dual
    else
      if delta * r.size < l.size then r.dual.rotateL x l.dual
      else if delta * l.size < r.size then r.dual.rotateR x l.dual else r.dual.node' x l.dual

Proof state:
case pos
α : Type u_1
l : Ordnode α
x : α
r : Ordnode α
h : ¬l.size + r.size ≤ 1
h_1 : delta * l.size < r.size
h_2 : delta * r.size < l.size
⊢ r.dual.rotateR x l.dual = r.dual.rotateL x l.dual

Tactic:
cases delta_lt_false h_1 h_2

Result:
no goals

Proof state:
α : Type u_1
l : Ordnode α
x : α
r : Ordnode α
⊢ (if l.size + r.size ≤ 1 then l.node' x r
      else
        if delta * l.size < r.size then l.rotateL x r
        else if delta * r.size < l.size then l.rotateR x r else l.node' x r).dual =
    if l.size + r.size ≤ 1 then r.dual.node' x l.dual
    else
      if delta * r.size < l.size then r.dual.rotateL x l.dual
      else if delta * l.size < r.size then r.dual.rotateR x l.dual else r.dual.node' x l.dual

Tactic:
split_ifs with h h_1 h_2 <;>
simp [dual_node', dual_rotateL, dual_rotateR, add_comm]

Result:
case pos
α : Type u_1
l : Ordnode α
x : α
r : Ordnode α
h : ¬l.size + r.size ≤ 1
h_1 : delta * l.size < r.size
h_2 : delta * r.size < l.size
⊢ r.dual.rotateR x l.dual = r.dual.rotateL x l.dual
-- Mathlib/Data/Finset/Lattice/Lemmas.lean
theorem toFinset_append : toFinset (l ++ l') = l.toFinset ∪ l'.toFinset

Proof state:
case nil
α : Type u_1
inst✝ : DecidableEq α
l l' : List α
⊢ ([] ++ l').toFinset = [].toFinset ∪ l'.toFinset

Tactic:
simp

Result:
no goals

Proof state:
case cons
α : Type u_1
inst✝ : DecidableEq α
l l' : List α
hd : α
tl : List α
hl : (tl ++ l').toFinset = tl.toFinset ∪ l'.toFinset
⊢ (hd :: tl ++ l').toFinset = (hd :: tl).toFinset ∪ l'.toFinset

Tactic:
simp [hl]

Result:
no goals

Proof state:
α : Type u_1
inst✝ : DecidableEq α
l l' : List α
⊢ (l ++ l').toFinset = l.toFinset ∪ l'.toFinset

Tactic:
induction' l with hd tl hl

Result:
case nil
α : Type u_1
inst✝ : DecidableEq α
l l' : List α
⊢ ([] ++ l').toFinset = [].toFinset ∪ l'.toFinset

case cons
α : Type u_1
inst✝ : DecidableEq α
l l' : List α
hd : α
tl : List α
hl : (tl ++ l').toFinset = tl.toFinset ∪ l'.toFinset
⊢ (hd :: tl ++ l').toFinset = (hd :: tl).toFinset ∪ l'.toFinset
-- Mathlib/RingTheory/Adjoin/Basic.lean
lemma commute_of_mem_adjoin_singleton_of_commute {a b c : A}
    (hc : c ∈ adjoin R {b}) (h : Commute a b) :
    Commute a c :=
  commute_of_mem_adjoin_of_forall_mem_commute hc <| by simpa

Proof state:
R : Type uR
A : Type uA
inst✝² : CommSemiring R
inst✝¹ : Semiring A
inst✝ : Algebra R A
a b c : A
hc : c ∈ adjoin R {b}
h : Commute a b
⊢ ∀ b_1 ∈ {b}, Commute a b_1

Tactic:
simpa

Result:
no goals
-- Mathlib/Data/Set/Function.lean
theorem mapsTo_iff_exists_map_subtype : MapsTo f s t ↔ ∃ g : s → t, ∀ x : s, f x = g x :=
  ⟨fun h => ⟨h.restrict f s t, fun _ => rfl⟩, fun ⟨g, hg⟩ x hx => by
    rw [hg ⟨x, hx⟩]
    apply Subtype.coe_prop⟩

Proof state:
α : Type u_1
β : Type u_2
s : Set α
t : Set β
f : α → β
x✝ : ∃ g, ∀ (x : ↑s), f ↑x = ↑(g x)
x : α
hx : x ∈ s
g : ↑s → ↑t
hg : ∀ (x : ↑s), f ↑x = ↑(g x)
⊢ f x ∈ t

Tactic:
rw [hg ⟨x, hx⟩]

Result:
α : Type u_1
β : Type u_2
s : Set α
t : Set β
f : α → β
x✝ : ∃ g, ∀ (x : ↑s), f ↑x = ↑(g x)
x : α
hx : x ∈ s
g : ↑s → ↑t
hg : ∀ (x : ↑s), f ↑x = ↑(g x)
⊢ ↑(g ⟨x, hx⟩) ∈ t

Proof state:
α : Type u_1
β : Type u_2
s : Set α
t : Set β
f : α → β
x✝ : ∃ g, ∀ (x : ↑s), f ↑x = ↑(g x)
x : α
hx : x ∈ s
g : ↑s → ↑t
hg : ∀ (x : ↑s), f ↑x = ↑(g x)
⊢ ↑(g ⟨x, hx⟩) ∈ t

Tactic:
apply Subtype.coe_prop

Result:
no goals
-- Mathlib/Tactic/NormNum/DivMod.lean
lemma isInt_emod_zero : ∀ {a b r : ℤ}, IsInt a r → IsNat b (nat_lit 0) → IsInt (a % b) r
  | _, _, _, e, ⟨rfl⟩ => by simp [e]

Proof state:
x✝¹ x✝ : ℤ
e : IsInt x✝¹ x✝
⊢ IsInt (x✝¹ % ↑0) x✝

Tactic:
simp [e]

Result:
no goals
-- Mathlib/AlgebraicGeometry/ProjectiveSpectrum/Topology.lean
theorem isOpen_iff (U : Set (ProjectiveSpectrum 𝒜)) : IsOpen U ↔ ∃ s, Uᶜ = zeroLocus 𝒜 s

Proof state:
R : Type u_1
A : Type u_2
inst✝³ : CommSemiring R
inst✝² : CommRing A
inst✝¹ : Algebra R A
𝒜 : ℕ → Submodule R A
inst✝ : GradedAlgebra 𝒜
U : Set (ProjectiveSpectrum 𝒜)
⊢ IsOpen U ↔ ∃ s, zeroLocus 𝒜 s = Uᶜ

Tactic:
rfl

Result:
no goals

Proof state:
R : Type u_1
A : Type u_2
inst✝³ : CommSemiring R
inst✝² : CommRing A
inst✝¹ : Algebra R A
𝒜 : ℕ → Submodule R A
inst✝ : GradedAlgebra 𝒜
U : Set (ProjectiveSpectrum 𝒜)
⊢ IsOpen U ↔ ∃ s, Uᶜ = zeroLocus 𝒜 s

Tactic:
simp only [@eq_comm _ Uᶜ]

Result:
R : Type u_1
A : Type u_2
inst✝³ : CommSemiring R
inst✝² : CommRing A
inst✝¹ : Algebra R A
𝒜 : ℕ → Submodule R A
inst✝ : GradedAlgebra 𝒜
U : Set (ProjectiveSpectrum 𝒜)
⊢ IsOpen U ↔ ∃ s, zeroLocus 𝒜 s = Uᶜ
-- Mathlib/CategoryTheory/ChosenFiniteProducts.lean
@[reassoc (attr := simp)]
lemma μ_fst (X Y : C) : LaxMonoidal.μ F X Y ≫ F.map (fst X Y) = fst (F.obj X) (F.obj Y) :=
  (cancel_epi (μIso _ _ _).inv).1 (by simp)

Proof state:
C : Type u
inst✝⁴ : Category.{v, u} C
inst✝³ : ChosenFiniteProducts C
D : Type u₁
inst✝² : Category.{v₁, u₁} D
inst✝¹ : ChosenFiniteProducts D
F : C ⥤ D
inst✝ : PreservesFiniteProducts F
X Y : C
⊢ (μIso F X Y).inv ≫ LaxMonoidal.μ F X Y ≫ F.map (fst X Y) = (μIso F X Y).inv ≫ fst (F.obj X) (F.obj Y)

Tactic:
simp

Result:
no goals
-- Mathlib/Order/LatticeIntervals.lean
protected lemma eq_top_iff [Preorder α] {x : Iic a} :
    x = ⊤ ↔ (x : α) = a

Proof state:
α : Type u_1
a : α
inst✝ : Preorder α
x : ↑(Iic a)
⊢ x = ⊤ ↔ ↑x = a

Tactic:
simp [Subtype.ext_iff]

Result:
no goals
-- Mathlib/Order/Interval/Finset/Basic.lean
theorem uIcc_subset_uIcc (h₁ : a₁ ∈ [[a₂, b₂]]) (h₂ : b₁ ∈ [[a₂, b₂]]) :
    [[a₁, b₁]] ⊆ [[a₂, b₂]]

Proof state:
α : Type u_2
inst✝¹ : Lattice α
inst✝ : LocallyFiniteOrder α
a₁ a₂ b₁ b₂ : α
h₁ : a₁ ∈ [[a₂, b₂]]
h₂ : b₁ ∈ [[a₂, b₂]]
⊢ [[a₁, b₁]] ⊆ [[a₂, b₂]]

Tactic:
rw [mem_uIcc] at h₁ h₂

Result:
α : Type u_2
inst✝¹ : Lattice α
inst✝ : LocallyFiniteOrder α
a₁ a₂ b₁ b₂ : α
h₁ : a₂ ⊓ b₂ ≤ a₁ ∧ a₁ ≤ a₂ ⊔ b₂
h₂ : a₂ ⊓ b₂ ≤ b₁ ∧ b₁ ≤ a₂ ⊔ b₂
⊢ [[a₁, b₁]] ⊆ [[a₂, b₂]]

Proof state:
α : Type u_2
inst✝¹ : Lattice α
inst✝ : LocallyFiniteOrder α
a₁ a₂ b₁ b₂ : α
h₁ : a₂ ⊓ b₂ ≤ a₁ ∧ a₁ ≤ a₂ ⊔ b₂
h₂ : a₂ ⊓ b₂ ≤ b₁ ∧ b₁ ≤ a₂ ⊔ b₂
⊢ [[a₁, b₁]] ⊆ [[a₂, b₂]]

Tactic:
exact Icc_subset_Icc (_root_.le_inf h₁.1 h₂.1) (_root_.sup_le h₁.2 h₂.2)

Result:
no goals
-- Mathlib/Data/Set/Operations.lean
theorem comp_rangeSplitting (f : α → β) : f ∘ rangeSplitting f = Subtype.val

Proof state:
case h
α : Type u
β : Type v
f : α → β
x✝ : ↑(range f)
⊢ f (rangeSplitting f x✝) = ↑x✝

Tactic:
apply apply_rangeSplitting

Result:
no goals

Proof state:
case h
α : Type u
β : Type v
f : α → β
x✝ : ↑(range f)
⊢ (f ∘ rangeSplitting f) x✝ = ↑x✝

Tactic:
simp only [Function.comp_apply]

Result:
case h
α : Type u
β : Type v
f : α → β
x✝ : ↑(range f)
⊢ f (rangeSplitting f x✝) = ↑x✝

Proof state:
α : Type u
β : Type v
f : α → β
⊢ f ∘ rangeSplitting f = Subtype.val

Tactic:
ext

Result:
case h
α : Type u
β : Type v
f : α → β
x✝ : ↑(range f)
⊢ (f ∘ rangeSplitting f) x✝ = ↑x✝
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Int/DivModLemmas.lean
theorem mul_fmod_left (a b : Int) : (a * b).fmod b = 0 :=
  if h : b = 0 then by simp [h, Int.mul_zero] else by
    rw [Int.fmod_def, Int.mul_fdiv_cancel _ h, Int.mul_comm, Int.sub_self]

Proof state:
a b : Int
h : b = 0
⊢ (a * b).fmod b = 0

Tactic:
simp [h, Int.mul_zero]

Result:
no goals

Proof state:
a b : Int
h : ¬b = 0
⊢ (a * b).fmod b = 0

Tactic:
rw [Int.fmod_def, Int.mul_fdiv_cancel _ h, Int.mul_comm, Int.sub_self]

Result:
no goals
-- Mathlib/.lake/packages/batteries/Batteries/Data/Array/Pairwise.lean
theorem pairwise_iff_getElem {as : Array α} : as.Pairwise R ↔
    ∀ (i j : Nat) (_ : i < as.size) (_ : j < as.size), i < j → R as[i] as[j]

Proof state:
α : Type u_1
R : α → α → Prop
as : Array α
⊢ List.Pairwise R as.toList ↔ ∀ (i j : Nat) (x : i < as.size) (x_1 : j < as.size), i < j → R as[i] as[j]

Tactic:
simp [List.pairwise_iff_getElem, length_toList]

Result:
no goals

Proof state:
α : Type u_1
R : α → α → Prop
as : Array α
⊢ Pairwise R as ↔ ∀ (i j : Nat) (x : i < as.size) (x_1 : j < as.size), i < j → R as[i] as[j]

Tactic:
unfold Pairwise

Result:
α : Type u_1
R : α → α → Prop
as : Array α
⊢ List.Pairwise R as.toList ↔ ∀ (i j : Nat) (x : i < as.size) (x_1 : j < as.size), i < j → R as[i] as[j]
-- Mathlib/AlgebraicGeometry/RationalMap.lean
lemma isOver_iff_eq_restrict [X.Over S] [Y.Over S] {f : X.PartialMap Y} :
    f.IsOver S ↔ f.compHom (Y ↘ S) = (X ↘ S).toPartialMap.restrict _ f.dense_domain (by simp)

Proof state:
X Y Z S : Scheme
sX : X ⟶ S
sY : Y ⟶ S
inst✝¹ : X.Over S
inst✝ : Y.Over S
f : X.PartialMap Y
⊢ f.domain ≤ (Hom.toPartialMap (X ↘ S)).domain

Tactic:
simp

Result:
no goals

Proof state:
X Y S : Scheme
inst✝¹ : X.Over S
inst✝ : Y.Over S
f : X.PartialMap Y
⊢ IsOver S f ↔ f.compHom (Y ↘ S) = (Hom.toPartialMap (X ↘ S)).restrict f.domain ⋯ ⋯

Tactic:
simp [isOver_iff, PartialMap.ext_iff]

Result:
no goals
-- Mathlib/RingTheory/IntegralClosure/IsIntegralClosure/Basic.lean
theorem mk'_mul (x y : B) (hx : IsIntegral R x) (hy : IsIntegral R y) :
    mk' A (x * y) (hx.mul hy) = mk' A x hx * mk' A y hy :=
  algebraMap_injective A R B <| by simp only [algebraMap_mk', RingHom.map_mul]

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
x y : B
hx : IsIntegral R x
hy : IsIntegral R y
⊢ (algebraMap A B) (mk' A (x * y) ⋯) = (algebraMap A B) (mk' A x hx * mk' A y hy)

Tactic:
simp only [algebraMap_mk', RingHom.map_mul]

Result:
no goals
-- Mathlib/LinearAlgebra/Dimension/Constructions.lean
theorem finrank_finsupp {ι : Type v} [Fintype ι] : finrank R (ι →₀ M) = card ι * finrank R M

Proof state:
R : Type u
M : Type v
inst✝⁵ : Semiring R
inst✝⁴ : AddCommMonoid M
inst✝³ : Module R M
inst✝² : StrongRankCondition R
inst✝¹ : Free R M
ι : Type v
inst✝ : Fintype ι
⊢ finrank R (ι →₀ M) = card ι * finrank R M

Tactic:
rw [finrank, finrank, rank_finsupp, ← mk_toNat_eq_card, toNat_mul, toNat_lift, toNat_lift]

Result:
no goals
-- Mathlib/Analysis/Fourier/FourierTransformDeriv.lean
lemma fderiv_fourierChar_neg_bilinear_left_apply (v y : V) (w : W) :
    fderiv ℝ (fun v ↦ (𝐞 (-L v w) : ℂ)) v y = -2 * π * I * L y w * 𝐞 (-L v w)

Proof state:
V : Type u_1
W : Type u_2
inst✝³ : NormedAddCommGroup V
inst✝² : NormedSpace ℝ V
inst✝¹ : NormedAddCommGroup W
inst✝ : NormedSpace ℝ W
L : V →L[ℝ] W →L[ℝ] ℝ
v y : V
w : W
⊢ 2 * ↑π * I * ↑(𝐞 (-(L v) w)) * ↑((L y) w) = 2 * ↑π * I * ↑((L y) w) * ↑(𝐞 (-(L v) w))

Tactic:
ring

Result:
no goals

Proof state:
V : Type u_1
W : Type u_2
inst✝³ : NormedAddCommGroup V
inst✝² : NormedSpace ℝ V
inst✝¹ : NormedAddCommGroup W
inst✝ : NormedSpace ℝ W
L : V →L[ℝ] W →L[ℝ] ℝ
v y : V
w : W
⊢ (fderiv ℝ (fun v => ↑(𝐞 (-(L v) w))) v) y = -2 * ↑π * I * ↑((L y) w) * ↑(𝐞 (-(L v) w))

Tactic:
simp only [(hasFDerivAt_fourierChar_neg_bilinear_left L v w).fderiv, neg_mul,
  ContinuousLinearMap.coe_smul', ContinuousLinearMap.coe_comp', Pi.smul_apply,
  Function.comp_apply, ContinuousLinearMap.flip_apply, ofRealCLM_apply, smul_eq_mul, neg_inj]

Result:
V : Type u_1
W : Type u_2
inst✝³ : NormedAddCommGroup V
inst✝² : NormedSpace ℝ V
inst✝¹ : NormedAddCommGroup W
inst✝ : NormedSpace ℝ W
L : V →L[ℝ] W →L[ℝ] ℝ
v y : V
w : W
⊢ 2 * ↑π * I * ↑(𝐞 (-(L v) w)) * ↑((L y) w) = 2 * ↑π * I * ↑((L y) w) * ↑(𝐞 (-(L v) w))
-- Mathlib/Algebra/Homology/HomotopyCategory/HomComplex.lean
@[simp]
lemma homOf_ofHom_eq_self (φ : F ⟶ G) : homOf (ofHom φ) = φ

Proof state:
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Preadditive C
F G : CochainComplex C ℤ
φ : F ⟶ G
⊢ (ofHom φ).homOf = φ

Tactic:
aesop_cat

Result:
no goals
-- Mathlib/AlgebraicGeometry/EllipticCurve/Jacobian.lean
lemma addX_of_Z_ne_zero {P Q : Fin 3 → F} (hP : W.Equation P) (hQ : W.Equation Q) (hPz : P z ≠ 0)
    (hQz : Q z ≠ 0) (hx : P x * Q z ^ 2 ≠ Q x * P z ^ 2) : W.addX P Q / addZ P Q ^ 2 =
      W.toAffine.addX (P x / P z ^ 2) (Q x / Q z ^ 2)
        (W.toAffine.slope (P x / P z ^ 2) (Q x / Q z ^ 2) (P y / P z ^ 3) (Q y / Q z ^ 3))

Proof state:
F : Type u
inst✝ : Field F
W : Jacobian F
P Q : Fin 3 → F
hP : W.Equation P
hQ : W.Equation Q
hPz : P z ≠ 0
hQz : Q z ≠ 0
hx : P x * Q z ^ 2 ≠ Q x * P z ^ 2
⊢ W.addX P Q / addZ P Q ^ 2 =
    (toAffine W).addX (P x / P z ^ 2) (Q x / Q z ^ 2)
      ((toAffine W).slope (P x / P z ^ 2) (Q x / Q z ^ 2) (P y / P z ^ 3) (Q y / Q z ^ 3))

Tactic:
rw [addX_eq hP hQ hPz hQz, toAffine_slope_of_ne hPz hQz hx,
  toAffine_addX_of_ne hPz hQz <| addZ_ne_zero_of_X_ne hx]

Result:
no goals
-- Mathlib/Logic/Equiv/Set.lean
theorem union_symm_apply_right {α} {s t : Set α} [DecidablePred fun x => x ∈ s] (H : Disjoint s t)
    (a : t) : (Equiv.Set.union H).symm (Sum.inr a) = ⟨a, by simp⟩ :=
  rfl

Proof state:
α✝ : Sort u
β : Sort v
γ : Sort w
α : Type ?u.17390
s t : Set α
inst✝ : DecidablePred fun x => x ∈ s
H : Disjoint s t
a : ↑t
⊢ ↑a ∈ s ∪ t

Tactic:
simp

Result:
no goals
-- Mathlib/CategoryTheory/MorphismProperty/Representable.lean
@[reassoc (attr := simp)]
lemma lift'_fst [Full F] [Faithful F] : hf'.lift' i h hi ≫ hf'.fst' g = i :=
  F.map_injective (by simp [map_fst', lift'])

Proof state:
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
D : Type u₂
inst✝² : Category.{v₂, u₂} D
F : C ⥤ D
Y : D
b : C
f' : F.obj b ⟶ Y
hf' : F.relativelyRepresentable f'
a : C
g : F.obj a ⟶ Y
c : C
i : c ⟶ b
h : c ⟶ a
hi : F.map i ≫ f' = F.map h ≫ g
inst✝¹ : F.Full
inst✝ : F.Faithful
⊢ F.map (hf'.lift' i h hi ≫ hf'.fst' g) = F.map i

Tactic:
simp [map_fst', lift']

Result:
no goals
-- Mathlib/MeasureTheory/Function/LpSpace/Basic.lean
theorem dist_def (f g : Lp E p μ) : dist f g = (eLpNorm (⇑f - ⇑g) p μ).toReal

Proof state:
α : Type u_1
E : Type u_4
m0 : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
inst✝ : NormedAddCommGroup E
f g : ↥(Lp E p μ)
⊢ eLpNorm (↑↑(f - g)) p μ = eLpNorm (↑↑f - ↑↑g) p μ

Tactic:
apply eLpNorm_congr_ae (coeFn_sub _ _)

Result:
no goals

Proof state:
α : Type u_1
E : Type u_4
m0 : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
inst✝ : NormedAddCommGroup E
f g : ↥(Lp E p μ)
⊢ dist f g = (eLpNorm (↑↑f - ↑↑g) p μ).toReal

Tactic:
simp_rw [dist, norm_def]

Result:
α : Type u_1
E : Type u_4
m0 : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
inst✝ : NormedAddCommGroup E
f g : ↥(Lp E p μ)
⊢ (eLpNorm (↑↑(f - g)) p μ).toReal = (eLpNorm (↑↑f - ↑↑g) p μ).toReal

Proof state:
α : Type u_1
E : Type u_4
m0 : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
inst✝ : NormedAddCommGroup E
f g : ↥(Lp E p μ)
⊢ (eLpNorm (↑↑(f - g)) p μ).toReal = (eLpNorm (↑↑f - ↑↑g) p μ).toReal

Tactic:
refine congr_arg _ ?_

Result:
α : Type u_1
E : Type u_4
m0 : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
inst✝ : NormedAddCommGroup E
f g : ↥(Lp E p μ)
⊢ eLpNorm (↑↑(f - g)) p μ = eLpNorm (↑↑f - ↑↑g) p μ
-- Mathlib/LinearAlgebra/Dimension/ErdosKaplansky.lean
theorem lift_rank_lt_rank_dual {K : Type u} {V : Type v} [Field K] [AddCommGroup V] [Module K V]
    (h : ℵ₀ ≤ Module.rank K V) :
    Cardinal.lift.{u} (Module.rank K V) < Module.rank K (V →ₗ[K] K)

Proof state:
K : Type u
V : Type v
inst✝² : Field K
inst✝¹ : AddCommGroup V
inst✝ : Module K V
h : ℵ₀ ≤ Module.rank K V
⊢ lift.{u, v} (Module.rank K V) < Module.rank K (V →ₗ[K] K)

Tactic:
rw [rank_dual_eq_card_dual_of_aleph0_le_rank h, ← rank_dual_eq_card_dual_of_aleph0_le_rank' h]

Result:
K : Type u
V : Type v
inst✝² : Field K
inst✝¹ : AddCommGroup V
inst✝ : Module K V
h : ℵ₀ ≤ Module.rank K V
⊢ lift.{u, v} (Module.rank K V) < Module.rank Kᵐᵒᵖ (V →ₗ[K] K)

Proof state:
K : Type u
V : Type v
inst✝² : Field K
inst✝¹ : AddCommGroup V
inst✝ : Module K V
h : ℵ₀ ≤ Module.rank K V
⊢ lift.{u, v} (Module.rank K V) < Module.rank Kᵐᵒᵖ (V →ₗ[K] K)

Tactic:
exact lift_rank_lt_rank_dual' h

Result:
no goals
-- Mathlib/Algebra/Polynomial/AlgebraMap.lean
theorem aeval_prod_apply (x : A × B) (p : Polynomial R) :
    p.aeval x = (p.aeval x.1, p.aeval x.2)

Proof state:
R : Type u
A : Type z
B : Type u_2
inst✝⁴ : CommSemiring R
inst✝³ : Semiring A
inst✝² : Semiring B
inst✝¹ : Algebra R A
inst✝ : Algebra R B
x : A × B
p : R[X]
⊢ (aeval x) p = ((aeval x.1) p, (aeval x.2) p)

Tactic:
simp [aeval_prod]

Result:
no goals
-- Mathlib/Algebra/DirectSum/Internal.lean
theorem DirectSum.coeAlgHom_of [AddMonoid ι] [CommSemiring S] [Semiring R] [Algebra S R]
    (A : ι → Submodule S R) [SetLike.GradedMonoid A] (i : ι) (x : A i) :
    DirectSum.coeAlgHom A (DirectSum.of (fun i => A i) i x) = x :=
  DirectSum.toSemiring_of _ (by rfl) (fun _ _ => (by rfl)) _ _

Proof state:
ι : Type u_1
S : Type u_3
R : Type u_4
inst✝⁵ : DecidableEq ι
inst✝⁴ : AddMonoid ι
inst✝³ : CommSemiring S
inst✝² : Semiring R
inst✝¹ : Algebra S R
A : ι → Submodule S R
inst✝ : SetLike.GradedMonoid A
i : ι
x : ↥(A i)
i✝ j✝ : ι
x✝¹ : (fun i => ↥(A i)) i✝
x✝ : (fun i => ↥(A i)) j✝
⊢ ((fun i => (A i).subtype) (i✝ + j✝)).toAddMonoidHom (GradedMonoid.GMul.mul x✝¹ x✝) =
    ((fun i => (A i).subtype) i✝).toAddMonoidHom x✝¹ * ((fun i => (A i).subtype) j✝).toAddMonoidHom x✝

Tactic:
rfl

Result:
no goals

Proof state:
ι : Type u_1
S : Type u_3
R : Type u_4
inst✝⁵ : DecidableEq ι
inst✝⁴ : AddMonoid ι
inst✝³ : CommSemiring S
inst✝² : Semiring R
inst✝¹ : Algebra S R
A : ι → Submodule S R
inst✝ : SetLike.GradedMonoid A
i : ι
x : ↥(A i)
⊢ ((fun i => (A i).subtype) 0).toAddMonoidHom GradedMonoid.GOne.one = 1

Tactic:
rfl

Result:
no goals
-- Mathlib/Algebra/Ring/Periodic.lean
theorem Antiperiodic.odd_nsmul_antiperiodic [AddMonoid α] [InvolutiveNeg β] (h : Antiperiodic f c)
    (n : ℕ) : Antiperiodic f ((2 * n + 1) • c) := fun x => by
  rw [add_nsmul, one_nsmul, ← add_assoc, h, h.even_nsmul_periodic]

Proof state:
α : Type u_1
β : Type u_2
f : α → β
c : α
inst✝¹ : AddMonoid α
inst✝ : InvolutiveNeg β
h : Antiperiodic f c
n : ℕ
x : α
⊢ f (x + (2 * n + 1) • c) = -f x

Tactic:
rw [add_nsmul, one_nsmul, ← add_assoc, h, h.even_nsmul_periodic]

Result:
no goals
-- Mathlib/Analysis/Calculus/ContDiff/Defs.lean
theorem contDiffAt_infty : ContDiffAt 𝕜 ∞ f x ↔ ∀ n : ℕ, ContDiffAt 𝕜 n f x

Proof state:
𝕜 : Type u
inst✝⁴ : NontriviallyNormedField 𝕜
E : Type uE
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
F : Type uF
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
f : E → F
x : E
⊢ ContDiffAt 𝕜 ∞ f x ↔ ∀ (n : ℕ), ContDiffAt 𝕜 (↑n) f x

Tactic:
simp [← contDiffWithinAt_univ, contDiffWithinAt_infty]

Result:
no goals
-- Mathlib/Algebra/Polynomial/Derivation.lean
lemma mkDerivation_apply (a : A) (f : R[X]) :
    mkDerivation R a f = derivative f • a

Proof state:
R : Type u_1
A : Type u_2
inst✝⁴ : CommSemiring R
inst✝³ : AddCommMonoid A
inst✝² : Module R A
inst✝¹ : Module R[X] A
inst✝ : IsScalarTower R R[X] A
a : A
f : R[X]
⊢ ((mkDerivation R) a) f = derivative f • a

Tactic:
rfl

Result:
no goals
-- Mathlib/Geometry/Manifold/MFDeriv/FDeriv.lean
theorem mdifferentiable_iff_differentiable :
    MDifferentiable 𝓘(𝕜, E) 𝓘(𝕜, E') f ↔ Differentiable 𝕜 f

Proof state:
𝕜 : Type u_1
inst✝⁴ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
E' : Type u_3
inst✝¹ : NormedAddCommGroup E'
inst✝ : NormedSpace 𝕜 E'
f : E → E'
⊢ MDifferentiable 𝓘(𝕜, E) 𝓘(𝕜, E') f ↔ Differentiable 𝕜 f

Tactic:
simp only [MDifferentiable, Differentiable, mdifferentiableAt_iff_differentiableAt]

Result:
no goals