harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/.lake/packages/lean4/src/lean/Std/Data/DHashMap/RawLemmas.lean
theorem getKey_alter [EquivBEq α] [LawfulHashable α] [Inhabited α] {k k' : α}
    {f : Option β → Option β} (h : m.WF) {hc : k' ∈ Const.alter m k f} :
    (Const.alter m k f).getKey k' hc =
      if heq : k == k' then
        k
      else
        haveI h' : k' ∈ m := mem_alter_of_beq_eq_false h (Bool.not_eq_true _ ▸ heq) |>.mp hc
        m.getKey k' h'

Proof state:
α : Type u
inst✝⁴ : BEq α
inst✝³ : Hashable α
β : Type v
m : Raw α fun x => β
inst✝² : EquivBEq α
inst✝¹ : LawfulHashable α
inst✝ : Inhabited α
k k' : α
f : Option β → Option β
h : m.WF
hc : k' ∈ alter m k f
⊢ (alter m k f).contains k' = true → (alter m k f).getKey k' hc = if heq : (k == k') = true then k else m.getKey k' ⋯

Tactic:
simp_to_raw using Raw₀.Const.getKey_alter

Result:
no goals

Proof state:
α : Type u
inst✝⁴ : BEq α
inst✝³ : Hashable α
β : Type v
m : Raw α fun x => β
inst✝² : EquivBEq α
inst✝¹ : LawfulHashable α
inst✝ : Inhabited α
k k' : α
f : Option β → Option β
h : m.WF
hc : k' ∈ alter m k f
⊢ (alter m k f).getKey k' hc = if heq : (k == k') = true then k else m.getKey k' ⋯

Tactic:
simp only [mem_iff_contains] at hc

Result:
α : Type u
inst✝⁴ : BEq α
inst✝³ : Hashable α
β : Type v
m : Raw α fun x => β
inst✝² : EquivBEq α
inst✝¹ : LawfulHashable α
inst✝ : Inhabited α
k k' : α
f : Option β → Option β
h : m.WF
hc✝ : k' ∈ alter m k f
hc : (alter m k f).contains k' = true
⊢ (alter m k f).getKey k' hc✝ = if heq : (k == k') = true then k else m.getKey k' ⋯

Proof state:
α : Type u
inst✝⁴ : BEq α
inst✝³ : Hashable α
β : Type v
m : Raw α fun x => β
inst✝² : EquivBEq α
inst✝¹ : LawfulHashable α
inst✝ : Inhabited α
k k' : α
f : Option β → Option β
h : m.WF
hc✝ : k' ∈ alter m k f
hc : (alter m k f).contains k' = true
⊢ (alter m k f).getKey k' hc✝ = if heq : (k == k') = true then k else m.getKey k' ⋯

Tactic:
revert hc

Result:
α : Type u
inst✝⁴ : BEq α
inst✝³ : Hashable α
β : Type v
m : Raw α fun x => β
inst✝² : EquivBEq α
inst✝¹ : LawfulHashable α
inst✝ : Inhabited α
k k' : α
f : Option β → Option β
h : m.WF
hc : k' ∈ alter m k f
⊢ (alter m k f).contains k' = true → (alter m k f).getKey k' hc = if heq : (k == k') = true then k else m.getKey k' ⋯
-- Mathlib/.lake/packages/lean4/src/lean/Std/Data/DHashMap/RawLemmas.lean
theorem mem_of_mem_insert [EquivBEq α] [LawfulHashable α] (h : m.WF) {k a : α} {v : β k} :
    a ∈ m.insert k v → (k == a) = false → a ∈ m

Proof state:
α : Type u
β : α → Type v
m : Raw α β
inst✝³ : BEq α
inst✝² : Hashable α
inst✝¹ : EquivBEq α
inst✝ : LawfulHashable α
h : m.WF
k a : α
v : β k
⊢ a ∈ m.insert k v → (k == a) = false → a ∈ m

Tactic:
simpa [mem_iff_contains] using contains_of_contains_insert h

Result:
no goals
-- Mathlib/Data/List/Basic.lean
theorem ext_getElem?_iff' {l₁ l₂ : List α} : l₁ = l₂ ↔
    ∀ n < max l₁.length l₂.length, l₁[n]? = l₂[n]? :=
  ⟨by rintro rfl _ _; rfl, ext_getElem?'⟩

Proof state:
α : Type u
l₁ : List α
n✝ : ℕ
a✝ : n✝ < l₁.length ⊔ l₁.length
⊢ l₁[n✝]? = l₁[n✝]?

Tactic:
rfl

Result:
no goals

Proof state:
α : Type u
l₁ l₂ : List α
⊢ l₁ = l₂ → ∀ (n : ℕ), n < l₁.length ⊔ l₂.length → l₁[n]? = l₂[n]?

Tactic:
rintro rfl _ _

Result:
α : Type u
l₁ : List α
n✝ : ℕ
a✝ : n✝ < l₁.length ⊔ l₁.length
⊢ l₁[n✝]? = l₁[n✝]?
-- Mathlib/Analysis/SpecialFunctions/PolarCoord.lean
theorem norm_polarCoord_symm (p : ℝ × ℝ) :
    ‖Complex.polarCoord.symm p‖ = |p.1|

Proof state:
p : ℝ × ℝ
⊢ ‖↑Complex.polarCoord.symm p‖ = |p.1|

Tactic:
simp

Result:
no goals
-- Mathlib/Algebra/Azumaya/Matrix.lean
theorem matrix [Nonempty n] : IsAzumaya R (Matrix n n R) where
  eq_of_smul_eq_smul

Proof state:
R : Type u_1
n : Type u_2
inst✝³ : CommSemiring R
inst✝² : Fintype n
inst✝¹ : DecidableEq n
inst✝ : Nonempty n
a✝ : Nontrivial R
⊢ ∀ {m₁ m₂ : R}, (∀ (a : Matrix n n R), m₁ • a = m₂ • a) → m₁ = m₂

Tactic:
exact eq_of_smul_eq_smul

Result:
no goals

Proof state:
R : Type u_1
n : Type u_2
inst✝³ : CommSemiring R
inst✝² : Fintype n
inst✝¹ : DecidableEq n
inst✝ : Nonempty n
⊢ ∀ {m₁ m₂ : R}, (∀ (a : Matrix n n R), m₁ • a = m₂ • a) → m₁ = m₂

Tactic:
nontriviality R

Result:
R : Type u_1
n : Type u_2
inst✝³ : CommSemiring R
inst✝² : Fintype n
inst✝¹ : DecidableEq n
inst✝ : Nonempty n
a✝ : Nontrivial R
⊢ ∀ {m₁ m₂ : R}, (∀ (a : Matrix n n R), m₁ • a = m₂ • a) → m₁ = m₂
-- Mathlib/Algebra/BigOperators/Finsupp.lean
@[to_additive (attr := simp)]
lemma prod_indicator_index_eq_prod_attach [Zero M] [CommMonoid N]
    {s : Finset α} (f : ∀ a ∈ s, M) {h : α → M → N} (h_zero : ∀ a ∈ s, h a 0 = 1) :
    (indicator s f).prod h = ∏ x ∈ s.attach, h ↑x (f x x.2)

Proof state:
α : Type u_1
M : Type u_8
N : Type u_10
inst✝¹ : Zero M
inst✝ : CommMonoid N
s : Finset α
f : (a : α) → a ∈ s → M
h : α → M → N
h_zero : ∀ a ∈ s, h a 0 = 1
x✝¹ : { x // x ∈ s }
x✝ : x✝¹ ∈ s.attach
⊢ h (↑x✝¹) ((indicator s f) ↑x✝¹) = h (↑x✝¹) (f ↑x✝¹ ⋯)

Tactic:
rw [indicator_of_mem]

Result:
no goals

Proof state:
α : Type u_1
M : Type u_8
N : Type u_10
inst✝¹ : Zero M
inst✝ : CommMonoid N
s : Finset α
f : (a : α) → a ∈ s → M
h : α → M → N
h_zero : ∀ a ∈ s, h a 0 = 1
⊢ ∏ x ∈ s.attach, h (↑x) ((indicator s f) ↑x) = ∏ x ∈ s.attach, h (↑x) (f ↑x ⋯)

Tactic:
refine Finset.prod_congr rfl (fun _ _ => ?_)

Result:
α : Type u_1
M : Type u_8
N : Type u_10
inst✝¹ : Zero M
inst✝ : CommMonoid N
s : Finset α
f : (a : α) → a ∈ s → M
h : α → M → N
h_zero : ∀ a ∈ s, h a 0 = 1
x✝¹ : { x // x ∈ s }
x✝ : x✝¹ ∈ s.attach
⊢ h (↑x✝¹) ((indicator s f) ↑x✝¹) = h (↑x✝¹) (f ↑x✝¹ ⋯)

Proof state:
α : Type u_1
M : Type u_8
N : Type u_10
inst✝¹ : Zero M
inst✝ : CommMonoid N
s : Finset α
f : (a : α) → a ∈ s → M
h : α → M → N
h_zero : ∀ a ∈ s, h a 0 = 1
⊢ (indicator s f).prod h = ∏ x ∈ s.attach, h (↑x) (f ↑x ⋯)

Tactic:
rw [prod_of_support_subset _ (support_indicator_subset _ _) h h_zero, ← prod_attach]

Result:
α : Type u_1
M : Type u_8
N : Type u_10
inst✝¹ : Zero M
inst✝ : CommMonoid N
s : Finset α
f : (a : α) → a ∈ s → M
h : α → M → N
h_zero : ∀ a ∈ s, h a 0 = 1
⊢ ∏ x ∈ s.attach, h (↑x) ((indicator s f) ↑x) = ∏ x ∈ s.attach, h (↑x) (f ↑x ⋯)
-- Mathlib/Probability/Kernel/CondDistrib.lean
theorem integrable_toReal_condDistrib (hX : AEMeasurable X μ) (hs : MeasurableSet s) :
    Integrable (fun a => (condDistrib Y X μ (X a) s).toReal) μ

Proof state:
case refine_1
α : Type u_1
β : Type u_2
Ω : Type u_3
inst✝³ : MeasurableSpace Ω
inst✝² : StandardBorelSpace Ω
inst✝¹ : Nonempty Ω
mα : MeasurableSpace α
μ : Measure α
inst✝ : IsFiniteMeasure μ
X : α → β
Y : α → Ω
mβ : MeasurableSpace β
s : Set Ω
hX : AEMeasurable X μ
hs : MeasurableSet s
⊢ AEMeasurable (fun a => ((condDistrib Y X μ) (X a)) s) μ

Tactic:
exact Measurable.comp_aemeasurable (Kernel.measurable_coe _ hs) hX

Result:
no goals

Proof state:
case refine_2
α : Type u_1
β : Type u_2
Ω : Type u_3
inst✝³ : MeasurableSpace Ω
inst✝² : StandardBorelSpace Ω
inst✝¹ : Nonempty Ω
mα : MeasurableSpace α
μ : Measure α
inst✝ : IsFiniteMeasure μ
X : α → β
Y : α → Ω
mβ : MeasurableSpace β
s : Set Ω
hX : AEMeasurable X μ
hs : MeasurableSet s
⊢ ∫⁻ (x : α), ((condDistrib Y X μ) (X x)) s ∂μ ≠ ⊤

Tactic:
refine ne_of_lt ?_

Result:
case refine_2
α : Type u_1
β : Type u_2
Ω : Type u_3
inst✝³ : MeasurableSpace Ω
inst✝² : StandardBorelSpace Ω
inst✝¹ : Nonempty Ω
mα : MeasurableSpace α
μ : Measure α
inst✝ : IsFiniteMeasure μ
X : α → β
Y : α → Ω
mβ : MeasurableSpace β
s : Set Ω
hX : AEMeasurable X μ
hs : MeasurableSet s
⊢ ∫⁻ (x : α), ((condDistrib Y X μ) (X x)) s ∂μ < ⊤

Proof state:
case refine_2
α : Type u_1
β : Type u_2
Ω : Type u_3
inst✝³ : MeasurableSpace Ω
inst✝² : StandardBorelSpace Ω
inst✝¹ : Nonempty Ω
mα : MeasurableSpace α
μ : Measure α
inst✝ : IsFiniteMeasure μ
X : α → β
Y : α → Ω
mβ : MeasurableSpace β
s : Set Ω
hX : AEMeasurable X μ
hs : MeasurableSet s
⊢ ∫⁻ (x : α), ((condDistrib Y X μ) (X x)) s ∂μ < ⊤

Tactic:
calc
  ∫⁻ a, condDistrib Y X μ (X a) s ∂μ ≤ ∫⁻ _, 1 ∂μ := lintegral_mono fun a => prob_le_one
  _ = μ univ := lintegral_one
  _ < ∞ := measure_lt_top _ _

Result:
no goals

Proof state:
α : Type u_1
β : Type u_2
Ω : Type u_3
inst✝³ : MeasurableSpace Ω
inst✝² : StandardBorelSpace Ω
inst✝¹ : Nonempty Ω
mα : MeasurableSpace α
μ : Measure α
inst✝ : IsFiniteMeasure μ
X : α → β
Y : α → Ω
mβ : MeasurableSpace β
s : Set Ω
hX : AEMeasurable X μ
hs : MeasurableSet s
⊢ Integrable (fun a => (((condDistrib Y X μ) (X a)) s).toReal) μ

Tactic:
refine integrable_toReal_of_lintegral_ne_top ?_ ?_

Result:
case refine_1
α : Type u_1
β : Type u_2
Ω : Type u_3
inst✝³ : MeasurableSpace Ω
inst✝² : StandardBorelSpace Ω
inst✝¹ : Nonempty Ω
mα : MeasurableSpace α
μ : Measure α
inst✝ : IsFiniteMeasure μ
X : α → β
Y : α → Ω
mβ : MeasurableSpace β
s : Set Ω
hX : AEMeasurable X μ
hs : MeasurableSet s
⊢ AEMeasurable (fun a => ((condDistrib Y X μ) (X a)) s) μ

case refine_2
α : Type u_1
β : Type u_2
Ω : Type u_3
inst✝³ : MeasurableSpace Ω
inst✝² : StandardBorelSpace Ω
inst✝¹ : Nonempty Ω
mα : MeasurableSpace α
μ : Measure α
inst✝ : IsFiniteMeasure μ
X : α → β
Y : α → Ω
mβ : MeasurableSpace β
s : Set Ω
hX : AEMeasurable X μ
hs : MeasurableSet s
⊢ ∫⁻ (x : α), ((condDistrib Y X μ) (X x)) s ∂μ ≠ ⊤
-- Mathlib/Order/Filter/Lift.lean
theorem lift'_pure {a : α} (hh : Monotone h) : (pure a : Filter α).lift' h = 𝓟 (h {a})

Proof state:
α : Type u_1
β : Type u_2
h : Set α → Set β
a : α
hh : Monotone h
⊢ (pure a).lift' h = 𝓟 (h {a})

Tactic:
rw [← principal_singleton, lift'_principal hh]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Std/Data/DHashMap/Internal/RawLemmas.lean
theorem get_insertManyIfNewUnit_list
    {l : List α} {k : α} {h} :
    get (insertManyIfNewUnit m l).1 k h = ()

Proof state:
α : Type u
inst✝¹ : BEq α
inst✝ : Hashable α
m : Raw₀ α fun x => Unit
l : List α
k : α
h : (insertManyIfNewUnit m l).val.contains k = true
⊢ get (insertManyIfNewUnit m l).val k h = ()

Tactic:
simp

Result:
no goals
-- Mathlib/Order/Directed.lean
theorem IsMin.not_isMax [IsDirected β (· ≥ ·)] {b : β} (hb : IsMin b) : ¬ IsMax b

Proof state:
β : Type v
inst✝² : PartialOrder β
inst✝¹ : Nontrivial β
inst✝ : IsDirected β fun x1 x2 => x1 ≥ x2
b : β
hb : IsMin b
⊢ ¬IsMax b

Tactic:
intro hb'

Result:
β : Type v
inst✝² : PartialOrder β
inst✝¹ : Nontrivial β
inst✝ : IsDirected β fun x1 x2 => x1 ≥ x2
b : β
hb : IsMin b
hb' : IsMax b
⊢ False

Proof state:
β : Type v
inst✝² : PartialOrder β
inst✝¹ : Nontrivial β
inst✝ : IsDirected β fun x1 x2 => x1 ≥ x2
b : β
hb : IsMin b
hb' : IsMax b
⊢ False

Tactic:
obtain ⟨a, c, hac⟩ := exists_lt_of_directed_ge β

Result:
case intro.intro
β : Type v
inst✝² : PartialOrder β
inst✝¹ : Nontrivial β
inst✝ : IsDirected β fun x1 x2 => x1 ≥ x2
b : β
hb : IsMin b
hb' : IsMax b
a c : β
hac : a < c
⊢ False

Proof state:
case intro.intro
β : Type v
inst✝² : PartialOrder β
inst✝¹ : Nontrivial β
inst✝ : IsDirected β fun x1 x2 => x1 ≥ x2
a c : β
hac : a < c
hb : IsMin a
hb' : IsMax a
this : a ≤ a
⊢ False

Tactic:
exact hb'.not_lt hac

Result:
no goals

Proof state:
case intro.intro
β : Type v
inst✝² : PartialOrder β
inst✝¹ : Nontrivial β
inst✝ : IsDirected β fun x1 x2 => x1 ≥ x2
b : β
hb : IsMin b
hb' : IsMax b
a c : β
hac : a < c
⊢ False

Tactic:
have := hb.isBot a

Result:
case intro.intro
β : Type v
inst✝² : PartialOrder β
inst✝¹ : Nontrivial β
inst✝ : IsDirected β fun x1 x2 => x1 ≥ x2
b : β
hb : IsMin b
hb' : IsMax b
a c : β
hac : a < c
this : b ≤ a
⊢ False

Proof state:
case intro.intro
β : Type v
inst✝² : PartialOrder β
inst✝¹ : Nontrivial β
inst✝ : IsDirected β fun x1 x2 => x1 ≥ x2
b : β
hb : IsMin b
hb' : IsMax b
a c : β
hac : a < c
this : b ≤ a
⊢ False

Tactic:
obtain rfl := (hb' <| this).antisymm this

Result:
case intro.intro
β : Type v
inst✝² : PartialOrder β
inst✝¹ : Nontrivial β
inst✝ : IsDirected β fun x1 x2 => x1 ≥ x2
a c : β
hac : a < c
hb : IsMin a
hb' : IsMax a
this : a ≤ a
⊢ False
-- Mathlib/Topology/Algebra/Algebra/Equiv.lean
theorem symm_comp_self (e : A ≃A[R] B) : (e.symm : B → A) ∘ e = id

Proof state:
R : Type u_1
A : Type u_2
B : Type u_3
inst✝⁶ : CommSemiring R
inst✝⁵ : Semiring A
inst✝⁴ : TopologicalSpace A
inst✝³ : Semiring B
inst✝² : TopologicalSpace B
inst✝¹ : Algebra R A
inst✝ : Algebra R B
e : A ≃A[R] B
⊢ ⇑e.symm ∘ ⇑e = id

Tactic:
exact funext <| e.symm_apply_apply

Result:
no goals
-- Mathlib/NumberTheory/LegendreSymbol/ZModChar.lean
theorem χ₄_nat_one_mod_four {n : ℕ} (hn : n % 4 = 1) : χ₄ n = 1

Proof state:
n : ℕ
hn : n % 4 = 1
⊢ χ₄ ↑n = 1

Tactic:
rw [χ₄_nat_mod_four, hn]

Result:
n : ℕ
hn : n % 4 = 1
⊢ χ₄ ↑1 = 1

Proof state:
n : ℕ
hn : n % 4 = 1
⊢ χ₄ ↑1 = 1

Tactic:
rfl

Result:
no goals
-- Mathlib/Data/Finsupp/Single.lean
theorem single_eq_same : (single a b : α →₀ M) a = b

Proof state:
α : Type u_1
M : Type u_5
inst✝ : Zero M
a : α
b : M
⊢ (single a b) a = b

Tactic:
classical exact Pi.single_eq_same (f := fun _ ↦ M) a b

Result:
no goals

Proof state:
α : Type u_1
M : Type u_5
inst✝ : Zero M
a : α
b : M
⊢ (single a b) a = b

Tactic:
exact Pi.single_eq_same (f := fun _ ↦ M) a b

Result:
no goals
-- Mathlib/RingTheory/Support.lean
lemma Module.support_eq_empty_iff :
    Module.support R M = ∅ ↔ Subsingleton M

Proof state:
R : Type u_1
M : Type u_2
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
⊢ support R M = ∅ ↔ Subsingleton M

Tactic:
rw [← Set.subset_empty_iff, ← PrimeSpectrum.zeroLocus_singleton_one,
  ← LocalizedModule.subsingleton_iff_support_subset, LocalizedModule.subsingleton_iff,
  subsingleton_iff_forall_eq 0]

Result:
R : Type u_1
M : Type u_2
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
⊢ (∀ (m : M), ∃ r ∈ Submonoid.powers 1, r • m = 0) ↔ ∀ (y : M), y = 0

Proof state:
R : Type u_1
M : Type u_2
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
⊢ (∀ (m : M), ∃ r ∈ Submonoid.powers 1, r • m = 0) ↔ ∀ (y : M), y = 0

Tactic:
simp only [Submonoid.powers_one, Submonoid.mem_bot, exists_eq_left, one_smul]

Result:
no goals
-- Mathlib/LinearAlgebra/PerfectPairing/Basic.lean
@[simp]
lemma toLin_apply (p : PerfectPairing R M N) {x : M} : p.toLin x = p x

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
p : PerfectPairing R M N
x : M
⊢ p.toLin x = p x

Tactic:
rfl

Result:
no goals
-- Mathlib/CategoryTheory/Sites/NonabelianCohomology/H1.lean
@[simp]
lemma ev_refl (γ : OneCocycle G U) (i : I) ⦃T : C⦄ (a : T ⟶ U i) :
    γ.ev i i a a = 1

Proof state:
C : Type u
inst✝ : Category.{v, u} C
G : Cᵒᵖ ⥤ Grp
I : Type w'
U : I → C
γ : OneCocycle G U
i : I
T : C
a : T ⟶ U i
⊢ γ.ev i i a a = 1

Tactic:
simpa using γ.ev_trans i i i a a a

Result:
no goals
-- Mathlib/Algebra/Homology/DerivedCategory/Ext/ExactSequences.lean
lemma preadditiveCoyoneda_homologySequenceδ_singleTriangle_apply
    [HasDerivedCategory.{w'} C] {X : C} {n₀ : ℕ} (x : Ext X S.X₃ n₀)
    {n₁ : ℕ} (h : n₀ + 1 = n₁) :
    (preadditiveCoyoneda.obj (op ((singleFunctor C 0).obj X))).homologySequenceδ
      hS.singleTriangle n₀ n₁ (by omega) x.hom =
        (x.comp hS.extClass h).hom

Proof state:
C : Type u
inst✝³ : Category.{v, u} C
inst✝² : Abelian C
inst✝¹ : HasExt C
S : ShortComplex C
hS : S.ShortExact
inst✝ : HasDerivedCategory C
X : C
n₀ : ℕ
x : Ext X S.X₃ n₀
n₁ : ℕ
h : n₀ + 1 = n₁
⊢ x.hom ≫
      (shiftFunctor (DerivedCategory C) ↑n₀).map hS.singleTriangle.mor₃ ≫
        (shiftFunctorAdd' (DerivedCategory C) 1 ↑n₀ ↑n₁ ⋯).inv.app hS.singleTriangle.obj₁ =
    x.hom ≫
      (shiftFunctor (DerivedCategory C) ↑n₀).map hS.singleδ ≫
        (shiftFunctorAdd' (DerivedCategory C) ↑1 ↑n₀ ↑n₁ ⋯).inv.app ((singleFunctor C 0).obj S.X₁)

Tactic:
rfl

Result:
no goals

Proof state:
C : Type u
inst✝³ : Category.{v, u} C
inst✝² : Abelian C
inst✝¹ : HasExt C
S : ShortComplex C
hS : S.ShortExact
inst✝ : HasDerivedCategory C
X : C
n₀ : ℕ
x : Ext X S.X₃ n₀
n₁ : ℕ
h : n₀ + 1 = n₁
⊢ (ConcreteCategory.hom
        ((preadditiveCoyoneda.obj (op ((singleFunctor C 0).obj X))).homologySequenceδ hS.singleTriangle ↑n₀ ↑n₁ ⋯))
      x.hom =
    (x.comp hS.extClass h).hom

Tactic:
rw [Pretriangulated.preadditiveCoyoneda_homologySequenceδ_apply,
  comp_hom, hS.extClass_hom, ShiftedHom.comp]

Result:
C : Type u
inst✝³ : Category.{v, u} C
inst✝² : Abelian C
inst✝¹ : HasExt C
S : ShortComplex C
hS : S.ShortExact
inst✝ : HasDerivedCategory C
X : C
n₀ : ℕ
x : Ext X S.X₃ n₀
n₁ : ℕ
h : n₀ + 1 = n₁
⊢ x.hom ≫
      (shiftFunctor (DerivedCategory C) ↑n₀).map hS.singleTriangle.mor₃ ≫
        (shiftFunctorAdd' (DerivedCategory C) 1 ↑n₀ ↑n₁ ⋯).inv.app hS.singleTriangle.obj₁ =
    x.hom ≫
      (shiftFunctor (DerivedCategory C) ↑n₀).map hS.singleδ ≫
        (shiftFunctorAdd' (DerivedCategory C) ↑1 ↑n₀ ↑n₁ ⋯).inv.app ((singleFunctor C 0).obj S.X₁)

Proof state:
C : Type u
inst✝³ : Category.{v, u} C
inst✝² : Abelian C
inst✝¹ : HasExt C
X✝ : C
S : ShortComplex C
hS : S.ShortExact
inst✝ : HasDerivedCategory C
X : C
n₀ : ℕ
x : Ext X S.X₃ n₀
n₁ : ℕ
h : n₀ + 1 = n₁
⊢ ↑n₀ + 1 = ↑n₁

Tactic:
omega

Result:
no goals
-- Mathlib/Order/SuccPred/Basic.lean
lemma not_pred_mem_iff_isMin [PredOrder α] [NoMinOrder α] {a : s} :
    pred ↑a ∉ s ↔ IsMin a where
  mp := isMin_of_not_pred_mem
  mpr h nh

Proof state:
α : Type u_3
inst✝³ : PartialOrder α
s : Set α
inst✝² : s.OrdConnected
inst✝¹ : PredOrder α
inst✝ : NoMinOrder α
a : ↑s
h : IsMin a
nh : pred ↑a ∈ s
⊢ False

Tactic:
replace h := congr($h.pred_eq.1)

Result:
α : Type u_3
inst✝³ : PartialOrder α
s : Set α
inst✝² : s.OrdConnected
inst✝¹ : PredOrder α
inst✝ : NoMinOrder α
a : ↑s
nh : pred ↑a ∈ s
h : ↑(pred a) = ↑a
⊢ False

Proof state:
α : Type u_3
inst✝³ : PartialOrder α
s : Set α
inst✝² : s.OrdConnected
inst✝¹ : PredOrder α
inst✝ : NoMinOrder α
a : ↑s
nh : pred ↑a ∈ s
h : pred ↑a = ↑a
⊢ False

Tactic:
simp at h

Result:
no goals

Proof state:
α : Type u_3
inst✝³ : PartialOrder α
s : Set α
inst✝² : s.OrdConnected
inst✝¹ : PredOrder α
inst✝ : NoMinOrder α
a : ↑s
nh : pred ↑a ∈ s
h : ↑(pred a) = ↑a
⊢ False

Tactic:
rw [coe_pred_of_mem nh] at h

Result:
α : Type u_3
inst✝³ : PartialOrder α
s : Set α
inst✝² : s.OrdConnected
inst✝¹ : PredOrder α
inst✝ : NoMinOrder α
a : ↑s
nh : pred ↑a ∈ s
h : pred ↑a = ↑a
⊢ False
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/List/Lemmas.lean
theorem head_append_right {l₁ l₂ : List α} (w : l₁ ++ l₂ ≠ []) (h : l₁ = []) :
    head (l₁ ++ l₂) w = head l₂ (by simp_all)

Proof state:
α : Type ?u.202107
l₁ l₂ : List α
w : l₁ ++ l₂ ≠ []
h : l₁ = []
⊢ l₂ ≠ []

Tactic:
simp_all

Result:
no goals

Proof state:
α : Type u_1
l₁ l₂ : List α
w : l₁ ++ l₂ ≠ []
h : l₁ = []
⊢ (l₁ ++ l₂).head w = l₂.head ⋯

Tactic:
rw [head_append, dif_pos (by simp_all)]

Result:
no goals

Proof state:
α : Type u_1
l₁ l₂ : List α
w : l₁ ++ l₂ ≠ []
h : l₁ = []
⊢ l₁.isEmpty = true

Tactic:
simp_all

Result:
no goals
-- Mathlib/Analysis/SpecialFunctions/Trigonometric/Angle.lean
theorem two_zsmul_toReal_eq_two_mul_sub_two_pi {θ : Angle} :
    ((2 : ℤ) • θ).toReal = 2 * θ.toReal - 2 * π ↔ π / 2 < θ.toReal

Proof state:
θ : Angle
⊢ (2 • θ).toReal = 2 * θ.toReal - 2 * π ↔ π / 2 < θ.toReal

Tactic:
rw [two_zsmul, ← two_nsmul, two_nsmul_toReal_eq_two_mul_sub_two_pi]

Result:
no goals
-- Mathlib/Geometry/Manifold/Instances/Real.lean
lemma IccRightChart_extend_top :
    (IccRightChart x y).extend (𝓡∂ 1) ⊤ = 0

Proof state:
x y : ℝ
hxy : Fact (x < y)
⊢ ↑(𝓡∂ 1) ⟨fun x => 0, ⋯⟩ = 0

Tactic:
congr

Result:
no goals

Proof state:
x y : ℝ
hxy : Fact (x < y)
⊢ ↑((IccRightChart x y).extend (𝓡∂ 1)) ⊤ = 0

Tactic:
norm_num [IccRightChart, modelWithCornersEuclideanHalfSpace_zero]

Result:
x y : ℝ
hxy : Fact (x < y)
⊢ ↑(𝓡∂ 1) ⟨fun x => 0, ⋯⟩ = 0
-- Mathlib/RingTheory/Spectrum/Prime/Topology.lean
theorem isRadical_vanishingIdeal (s : Set (PrimeSpectrum R)) : (vanishingIdeal s).IsRadical

Proof state:
R : Type u
inst✝ : CommSemiring R
s : Set (PrimeSpectrum R)
⊢ (vanishingIdeal s).IsRadical

Tactic:
rw [← vanishingIdeal_closure, ← zeroLocus_vanishingIdeal_eq_closure,
  vanishingIdeal_zeroLocus_eq_radical]

Result:
R : Type u
inst✝ : CommSemiring R
s : Set (PrimeSpectrum R)
⊢ (vanishingIdeal s).radical.IsRadical

Proof state:
R : Type u
inst✝ : CommSemiring R
s : Set (PrimeSpectrum R)
⊢ (vanishingIdeal s).radical.IsRadical

Tactic:
apply Ideal.radical_isRadical

Result:
no goals
-- Mathlib/Probability/Kernel/MeasurableIntegral.lean
theorem ProbabilityTheory.measurableSet_kernel_integrable ⦃f : α → β → E⦄
    (hf : StronglyMeasurable (uncurry f)) :
    MeasurableSet {x | Integrable (f x) (κ x)}

Proof state:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ : Kernel α β
E : Type u_4
inst✝¹ : NormedAddCommGroup E
inst✝ : IsSFiniteKernel κ
f : α → β → E
hf : StronglyMeasurable (uncurry f)
⊢ MeasurableSet {x | HasFiniteIntegral (f x) (κ x)}

Tactic:
exact measurableSet_lt (Measurable.lintegral_kernel_prod_right hf.enorm) measurable_const

Result:
no goals

Proof state:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ : Kernel α β
E : Type u_4
inst✝¹ : NormedAddCommGroup E
inst✝ : IsSFiniteKernel κ
f : α → β → E
hf : StronglyMeasurable (uncurry f)
⊢ MeasurableSet {x | Integrable (f x) (κ x)}

Tactic:
simp_rw [Integrable, hf.of_uncurry_left.aestronglyMeasurable, true_and]

Result:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ : Kernel α β
E : Type u_4
inst✝¹ : NormedAddCommGroup E
inst✝ : IsSFiniteKernel κ
f : α → β → E
hf : StronglyMeasurable (uncurry f)
⊢ MeasurableSet {x | HasFiniteIntegral (f x) (κ x)}
-- Mathlib/Algebra/Homology/ShortComplex/RightHomology.lean
lemma leftHomologyMap_op (φ : S₁ ⟶ S₂) [S₁.HasLeftHomology] [S₂.HasLeftHomology] :
    (leftHomologyMap φ).op = S₂.rightHomologyOpIso.inv ≫ rightHomologyMap (opMap φ) ≫
      S₁.rightHomologyOpIso.hom

Proof state:
C : Type u_1
inst✝³ : Category.{u_2, u_1} C
inst✝² : HasZeroMorphisms C
S₁ S₂ : ShortComplex C
φ : S₁ ⟶ S₂
inst✝¹ : S₁.HasLeftHomology
inst✝ : S₂.HasLeftHomology
⊢ (leftHomologyMap φ).op = S₂.rightHomologyOpIso.inv ≫ rightHomologyMap (opMap φ) ≫ S₁.rightHomologyOpIso.hom

Tactic:
dsimp [rightHomologyOpIso, RightHomologyData.rightHomologyIso, rightHomologyMap,
  leftHomologyMap]

Result:
C : Type u_1
inst✝³ : Category.{u_2, u_1} C
inst✝² : HasZeroMorphisms C
S₁ S₂ : ShortComplex C
φ : S₁ ⟶ S₂
inst✝¹ : S₁.HasLeftHomology
inst✝ : S₂.HasLeftHomology
⊢ (leftHomologyMap' φ S₁.leftHomologyData S₂.leftHomologyData).op =
    rightHomologyMap' (𝟙 S₂.op) S₂.leftHomologyData.op S₂.op.rightHomologyData ≫
      rightHomologyMap' (opMap φ) S₂.op.rightHomologyData S₁.op.rightHomologyData ≫
        rightHomologyMap' (𝟙 S₁.op) S₁.op.rightHomologyData S₁.leftHomologyData.op

Proof state:
C : Type u_1
inst✝³ : Category.{u_2, u_1} C
inst✝² : HasZeroMorphisms C
S₁ S₂ : ShortComplex C
φ : S₁ ⟶ S₂
inst✝¹ : S₁.HasLeftHomology
inst✝ : S₂.HasLeftHomology
⊢ (leftHomologyMap' φ S₁.leftHomologyData S₂.leftHomologyData).op =
    rightHomologyMap' (𝟙 S₂.op) S₂.leftHomologyData.op S₂.op.rightHomologyData ≫
      rightHomologyMap' (opMap φ) S₂.op.rightHomologyData S₁.op.rightHomologyData ≫
        rightHomologyMap' (𝟙 S₁.op) S₁.op.rightHomologyData S₁.leftHomologyData.op

Tactic:
simp only [← rightHomologyMap'_comp, comp_id, id_comp, leftHomologyMap'_op]

Result:
no goals
-- Mathlib/Topology/Algebra/Monoid.lean
theorem continuousMul_inf {t₁ t₂ : TopologicalSpace M} (h₁ : @ContinuousMul M t₁ _)
    (h₂ : @ContinuousMul M t₂ _) : @ContinuousMul M (t₁ ⊓ t₂) _

Proof state:
M : Type u_3
inst✝ : Mul M
t₁ t₂ : TopologicalSpace M
h₁ : ContinuousMul M
h₂ : ContinuousMul M
⊢ ContinuousMul M

Tactic:
refine continuousMul_iInf fun b => ?_

Result:
M : Type u_3
inst✝ : Mul M
t₁ t₂ : TopologicalSpace M
h₁ : ContinuousMul M
h₂ : ContinuousMul M
b : Bool
⊢ ContinuousMul M

Proof state:
M : Type u_3
inst✝ : Mul M
t₁ t₂ : TopologicalSpace M
h₁ : ContinuousMul M
h₂ : ContinuousMul M
b : Bool
⊢ ContinuousMul M

Tactic:
cases b <;> assumption

Result:
no goals