harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/Topology/Instances/ENNReal/Lemmas.lean
theorem Summable.of_nonneg_of_le {f g : β → ℝ} (hg : ∀ b, 0 ≤ g b) (hgf : ∀ b, g b ≤ f b)
    (hf : Summable f) : Summable g

Proof state:
β : Type u_2
f g : β → ℝ
hg : ∀ (b : β), 0 ≤ g b
hgf : ∀ (b : β), g b ≤ f b
hf : Summable f
⊢ Summable g

Tactic:
lift f to β → ℝ≥0 using fun b => (hg b).trans (hgf b)

Result:
case intro
β : Type u_2
g : β → ℝ
hg : ∀ (b : β), 0 ≤ g b
f : β → ℝ≥0
hgf : ∀ (b : β), g b ≤ (fun i => ↑(f i)) b
hf : Summable fun i => ↑(f i)
⊢ Summable g

Proof state:
case intro.intro
β : Type u_2
f : β → ℝ≥0
hf : Summable fun i => ↑(f i)
g : β → ℝ≥0
hgf : ∀ (b : β), (fun i => ↑(g i)) b ≤ (fun i => ↑(f i)) b
⊢ Summable fun i => ↑(g i)

Tactic:
rw [NNReal.summable_coe] at hf ⊢

Result:
case intro.intro
β : Type u_2
f : β → ℝ≥0
hf : Summable f
g : β → ℝ≥0
hgf : ∀ (b : β), (fun i => ↑(g i)) b ≤ (fun i => ↑(f i)) b
⊢ Summable g

Proof state:
case intro.intro
β : Type u_2
f : β → ℝ≥0
hf : Summable f
g : β → ℝ≥0
hgf : ∀ (b : β), (fun i => ↑(g i)) b ≤ (fun i => ↑(f i)) b
⊢ Summable g

Tactic:
exact NNReal.summable_of_le (fun b => NNReal.coe_le_coe.1 (hgf b)) hf

Result:
no goals

Proof state:
case intro
β : Type u_2
g : β → ℝ
hg : ∀ (b : β), 0 ≤ g b
f : β → ℝ≥0
hgf : ∀ (b : β), g b ≤ (fun i => ↑(f i)) b
hf : Summable fun i => ↑(f i)
⊢ Summable g

Tactic:
lift g to β → ℝ≥0 using hg

Result:
case intro.intro
β : Type u_2
f : β → ℝ≥0
hf : Summable fun i => ↑(f i)
g : β → ℝ≥0
hgf : ∀ (b : β), (fun i => ↑(g i)) b ≤ (fun i => ↑(f i)) b
⊢ Summable fun i => ↑(g i)
-- Mathlib/Algebra/Homology/HomotopyCategory/HomComplex.lean
@[simp]
lemma comp_assoc_of_second_degree_eq_neg_third_degree {n₁ n₂ n₁₂ : ℤ}
    (z₁ : Cochain F G n₁) (z₂ : Cochain G K (-n₂)) (z₃ : Cochain K L n₂) (h₁₂ : n₁ + (-n₂) = n₁₂) :
    (z₁.comp z₂ h₁₂).comp z₃
      (show n₁₂ + n₂ = n₁ by rw [← h₁₂, add_assoc, neg_add_cancel, add_zero]) =
      z₁.comp (z₂.comp z₃ (neg_add_cancel n₂)) (add_zero n₁) :=
  comp_assoc _ _ _ _ _ (by omega)

Proof state:
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Preadditive C
F G K L : CochainComplex C ℤ
n₁ n₂ n₁₂ : ℤ
z₁ : Cochain F G n₁
z₂ : Cochain G K (-n₂)
z₃ : Cochain K L n₂
h₁₂ : n₁ + -n₂ = n₁₂
⊢ n₁ + -n₂ + n₂ = n₁

Tactic:
omega

Result:
no goals

Proof state:
C : Type u
inst✝³ : Category.{v, u} C
inst✝² : Preadditive C
R : Type u_1
inst✝¹ : Ring R
inst✝ : Linear R C
F G K L : CochainComplex C ℤ
n m n₁ n₂ n₁₂ : ℤ
z₁ : Cochain F G n₁
z₂ : Cochain G K (-n₂)
z₃ : Cochain K L n₂
h₁₂ : n₁ + -n₂ = n₁₂
⊢ n₁₂ + n₂ = n₁

Tactic:
rw [← h₁₂, add_assoc, neg_add_cancel, add_zero]

Result:
no goals
-- Mathlib/Analysis/SpecialFunctions/Log/Basic.lean
theorem tendsto_log_atTop : Tendsto log atTop atTop :=
  tendsto_comp_exp_atTop.1 <| by simpa only [log_exp] using tendsto_id

Proof state:
⊢ Tendsto (fun x => log (rexp x)) atTop atTop

Tactic:
simpa only [log_exp] using tendsto_id

Result:
no goals
-- Mathlib/Data/List/Sort.lean
theorem sublist_of_subperm_of_sorted [IsAntisymm α r] {l₁ l₂ : List α} (hp : l₁ <+~ l₂)
    (hs₁ : l₁.Sorted r) (hs₂ : l₂.Sorted r) : l₁ <+ l₂

Proof state:
α : Type u
r : α → α → Prop
inst✝ : IsAntisymm α r
l₁ l₂ : List α
hp : l₁ <+~ l₂
hs₁ : Sorted r l₁
hs₂ : Sorted r l₂
⊢ l₁ <+ l₂

Tactic:
let ⟨_, h, h'⟩ := hp

Result:
α : Type u
r : α → α → Prop
inst✝ : IsAntisymm α r
l₁ l₂ : List α
hp : l₁ <+~ l₂
hs₁ : Sorted r l₁
hs₂ : Sorted r l₂
w✝ : List α
h : w✝ ~ l₁
h' : w✝ <+ l₂
⊢ l₁ <+ l₂

Proof state:
α : Type u
r : α → α → Prop
inst✝ : IsAntisymm α r
l₁ l₂ : List α
hp : l₁ <+~ l₂
hs₁ : Sorted r l₁
hs₂ : Sorted r l₂
w✝ : List α
h : w✝ ~ l₁
h' : w✝ <+ l₂
⊢ l₁ <+ l₂

Tactic:
rwa [← eq_of_perm_of_sorted h (hs₂.sublist h') hs₁]

Result:
no goals
-- Mathlib/Combinatorics/SetFamily/LYM.lean
theorem IsAntichain.disjoint_slice_shadow_falling {m n : ℕ}
    (h𝒜 : IsAntichain (· ⊆ ·) (𝒜 : Set (Finset α))) : Disjoint (𝒜 # m) (∂ (falling n 𝒜)) :=
  disjoint_right.2 fun s h₁ h₂ => by
    simp_rw [mem_shadow_iff, mem_falling] at h₁
    obtain ⟨s, ⟨⟨t, ht, hst⟩, _⟩, a, ha, rfl⟩ := h₁
    refine h𝒜 (slice_subset h₂) ht ?_ ((erase_subset _ _).trans hst)
    rintro rfl
    exact not_mem_erase _ _ (hst ha)

Proof state:
case intro.intro.intro.intro.intro.intro.intro
α : Type u_2
inst✝ : DecidableEq α
𝒜 : Finset (Finset α)
m n : ℕ
h𝒜 : IsAntichain (fun x1 x2 => x1 ⊆ x2) ↑𝒜
s : Finset α
right✝ : #s = n
t : Finset α
ht : t ∈ 𝒜
hst : s ⊆ t
a : α
ha : a ∈ s
h₂ : s.erase a ∈ 𝒜 # m
⊢ s.erase a ≠ t

Tactic:
rintro rfl

Result:
case intro.intro.intro.intro.intro.intro.intro
α : Type u_2
inst✝ : DecidableEq α
𝒜 : Finset (Finset α)
m n : ℕ
h𝒜 : IsAntichain (fun x1 x2 => x1 ⊆ x2) ↑𝒜
s : Finset α
right✝ : #s = n
a : α
ha : a ∈ s
h₂ : s.erase a ∈ 𝒜 # m
ht : s.erase a ∈ 𝒜
hst : s ⊆ s.erase a
⊢ False

Proof state:
α : Type u_2
inst✝ : DecidableEq α
𝒜 : Finset (Finset α)
m n : ℕ
h𝒜 : IsAntichain (fun x1 x2 => x1 ⊆ x2) ↑𝒜
s : Finset α
h₁ : s ∈ ∂ (falling n 𝒜)
h₂ : s ∈ 𝒜 # m
⊢ False

Tactic:
simp_rw [mem_shadow_iff, mem_falling] at h₁

Result:
α : Type u_2
inst✝ : DecidableEq α
𝒜 : Finset (Finset α)
m n : ℕ
h𝒜 : IsAntichain (fun x1 x2 => x1 ⊆ x2) ↑𝒜
s : Finset α
h₂ : s ∈ 𝒜 # m
h₁ : ∃ s_1, ((∃ t ∈ 𝒜, s_1 ⊆ t) ∧ #s_1 = n) ∧ ∃ a ∈ s_1, s_1.erase a = s
⊢ False

Proof state:
case intro.intro.intro.intro.intro.intro.intro
α : Type u_2
inst✝ : DecidableEq α
𝒜 : Finset (Finset α)
m n : ℕ
h𝒜 : IsAntichain (fun x1 x2 => x1 ⊆ x2) ↑𝒜
s : Finset α
right✝ : #s = n
a : α
ha : a ∈ s
h₂ : s.erase a ∈ 𝒜 # m
ht : s.erase a ∈ 𝒜
hst : s ⊆ s.erase a
⊢ False

Tactic:
exact not_mem_erase _ _ (hst ha)

Result:
no goals

Proof state:
α : Type u_2
inst✝ : DecidableEq α
𝒜 : Finset (Finset α)
m n : ℕ
h𝒜 : IsAntichain (fun x1 x2 => x1 ⊆ x2) ↑𝒜
s : Finset α
h₂ : s ∈ 𝒜 # m
h₁ : ∃ s_1, ((∃ t ∈ 𝒜, s_1 ⊆ t) ∧ #s_1 = n) ∧ ∃ a ∈ s_1, s_1.erase a = s
⊢ False

Tactic:
obtain ⟨s, ⟨⟨t, ht, hst⟩, _⟩, a, ha, rfl⟩ := h₁

Result:
case intro.intro.intro.intro.intro.intro.intro
α : Type u_2
inst✝ : DecidableEq α
𝒜 : Finset (Finset α)
m n : ℕ
h𝒜 : IsAntichain (fun x1 x2 => x1 ⊆ x2) ↑𝒜
s : Finset α
right✝ : #s = n
t : Finset α
ht : t ∈ 𝒜
hst : s ⊆ t
a : α
ha : a ∈ s
h₂ : s.erase a ∈ 𝒜 # m
⊢ False

Proof state:
case intro.intro.intro.intro.intro.intro.intro
α : Type u_2
inst✝ : DecidableEq α
𝒜 : Finset (Finset α)
m n : ℕ
h𝒜 : IsAntichain (fun x1 x2 => x1 ⊆ x2) ↑𝒜
s : Finset α
right✝ : #s = n
t : Finset α
ht : t ∈ 𝒜
hst : s ⊆ t
a : α
ha : a ∈ s
h₂ : s.erase a ∈ 𝒜 # m
⊢ False

Tactic:
refine h𝒜 (slice_subset h₂) ht ?_ ((erase_subset _ _).trans hst)

Result:
case intro.intro.intro.intro.intro.intro.intro
α : Type u_2
inst✝ : DecidableEq α
𝒜 : Finset (Finset α)
m n : ℕ
h𝒜 : IsAntichain (fun x1 x2 => x1 ⊆ x2) ↑𝒜
s : Finset α
right✝ : #s = n
t : Finset α
ht : t ∈ 𝒜
hst : s ⊆ t
a : α
ha : a ∈ s
h₂ : s.erase a ∈ 𝒜 # m
⊢ s.erase a ≠ t
-- Mathlib/CategoryTheory/GradedObject.lean
@[reassoc (attr := simp)]
lemma ιMapObjOrZero_mapMap :
    X.ιMapObjOrZero p i j ≫ mapMap φ p j = φ i ≫ Y.ιMapObjOrZero p i j

Proof state:
case pos
I : Type u_1
J : Type u_2
C : Type u_4
inst✝⁴ : Category.{u_5, u_4} C
X Y : GradedObject I C
φ : X ⟶ Y
p : I → J
inst✝³ : X.HasMap p
inst✝² : Y.HasMap p
inst✝¹ : HasZeroMorphisms C
inst✝ : DecidableEq J
i : I
j : J
h : p i = j
⊢ X.ιMapObjOrZero p i j ≫ mapMap φ p j = φ i ≫ Y.ιMapObjOrZero p i j

Tactic:
simp only [ιMapObjOrZero_eq _ _ _ _ h, ι_mapMap]

Result:
no goals

Proof state:
case neg
I : Type u_1
J : Type u_2
C : Type u_4
inst✝⁴ : Category.{u_5, u_4} C
X Y : GradedObject I C
φ : X ⟶ Y
p : I → J
inst✝³ : X.HasMap p
inst✝² : Y.HasMap p
inst✝¹ : HasZeroMorphisms C
inst✝ : DecidableEq J
i : I
j : J
h : ¬p i = j
⊢ X.ιMapObjOrZero p i j ≫ mapMap φ p j = φ i ≫ Y.ιMapObjOrZero p i j

Tactic:
simp only [ιMapObjOrZero_eq_zero _ _ _ _ h, zero_comp, comp_zero]

Result:
no goals

Proof state:
I : Type u_1
J : Type u_2
C : Type u_4
inst✝⁴ : Category.{u_5, u_4} C
X Y : GradedObject I C
φ : X ⟶ Y
p : I → J
inst✝³ : X.HasMap p
inst✝² : Y.HasMap p
inst✝¹ : HasZeroMorphisms C
inst✝ : DecidableEq J
i : I
j : J
⊢ X.ιMapObjOrZero p i j ≫ mapMap φ p j = φ i ≫ Y.ιMapObjOrZero p i j

Tactic:
by_cases h : p i = j

Result:
case pos
I : Type u_1
J : Type u_2
C : Type u_4
inst✝⁴ : Category.{u_5, u_4} C
X Y : GradedObject I C
φ : X ⟶ Y
p : I → J
inst✝³ : X.HasMap p
inst✝² : Y.HasMap p
inst✝¹ : HasZeroMorphisms C
inst✝ : DecidableEq J
i : I
j : J
h : p i = j
⊢ X.ιMapObjOrZero p i j ≫ mapMap φ p j = φ i ≫ Y.ιMapObjOrZero p i j

case neg
I : Type u_1
J : Type u_2
C : Type u_4
inst✝⁴ : Category.{u_5, u_4} C
X Y : GradedObject I C
φ : X ⟶ Y
p : I → J
inst✝³ : X.HasMap p
inst✝² : Y.HasMap p
inst✝¹ : HasZeroMorphisms C
inst✝ : DecidableEq J
i : I
j : J
h : ¬p i = j
⊢ X.ιMapObjOrZero p i j ≫ mapMap φ p j = φ i ≫ Y.ιMapObjOrZero p i j
-- Mathlib/Analysis/CStarAlgebra/ContinuousFunctionalCalculus/Order.lean
lemma le_inv_iff {a b : Aˣ} (ha : 0 ≤ (a : A)) (hb : 0 ≤ (↑b : A)) :
    a ≤ (↑b⁻¹ : A) ↔ b ≤ (↑a⁻¹ : A)

Proof state:
A : Type u_1
inst✝² : CStarAlgebra A
inst✝¹ : PartialOrder A
inst✝ : StarOrderedRing A
a b : Aˣ
ha : 0 ≤ ↑a
hb : 0 ≤ ↑b
⊢ ↑a ≤ ↑b⁻¹ ↔ ↑b ≤ ↑a⁻¹

Tactic:
simpa using CStarAlgebra.inv_le_inv_iff (inv_nonneg_of_nonneg a ha) hb

Result:
no goals
-- Mathlib/Algebra/Homology/HomologySequence.lean
@[reassoc (attr := simp)]
lemma pOpcycles_opcyclesToCycles :
    K.pOpcycles i ≫ K.opcyclesToCycles i j = K.toCycles i j

Proof state:
C : Type u_1
ι : Type u_2
inst✝³ : Category.{u_3, u_1} C
inst✝² : HasZeroMorphisms C
c : ComplexShape ι
K : HomologicalComplex C c
i j : ι
inst✝¹ : K.HasHomology i
inst✝ : K.HasHomology j
⊢ K.pOpcycles i ≫ K.opcyclesToCycles i j = K.toCycles i j

Tactic:
simp only [← cancel_mono (K.iCycles j), assoc, opcyclesToCycles_iCycles,
  p_fromOpcycles, toCycles_i]

Result:
no goals
-- Mathlib/SetTheory/Game/Ordinal.lean
theorem toPGame_moveLeft {o : Ordinal} (i) :
    o.toPGame.moveLeft (toLeftMovesToPGame i) = i.val.toPGame

Proof state:
o : Ordinal.{u_1}
i : ↑(Set.Iio o)
⊢ o.toPGame.moveLeft (toLeftMovesToPGame i) = (↑i).toPGame

Tactic:
simp

Result:
no goals
-- Mathlib/Algebra/Polynomial/Laurent.lean
theorem induction_on' {M : R[T;T⁻¹] → Prop} (p : R[T;T⁻¹])
    (h_add : ∀ p q, M p → M q → M (p + q)) (h_C_mul_T : ∀ (n : ℤ) (a : R), M (C a * T n)) :
    M p

Proof state:
case h.e'_1
R : Type u_1
inst✝ : Semiring R
M : R[T;T⁻¹] → Prop
p : R[T;T⁻¹]
h_add : ∀ (p q : R[T;T⁻¹]), M p → M q → M (p + q)
h_C_mul_T : ∀ (n : ℤ) (a : R), M (C a * T n)
a : R
⊢ C a = C a * T 0

Tactic:
exact (mul_one _).symm

Result:
no goals

Proof state:
case refine_1
R : Type u_1
inst✝ : Semiring R
M : R[T;T⁻¹] → Prop
p : R[T;T⁻¹]
h_add : ∀ (p q : R[T;T⁻¹]), M p → M q → M (p + q)
h_C_mul_T : ∀ (n : ℤ) (a : R), M (C a * T n)
a : R
⊢ M (C a)

Tactic:
convert h_C_mul_T 0 a

Result:
case h.e'_1
R : Type u_1
inst✝ : Semiring R
M : R[T;T⁻¹] → Prop
p : R[T;T⁻¹]
h_add : ∀ (p q : R[T;T⁻¹]), M p → M q → M (p + q)
h_C_mul_T : ∀ (n : ℤ) (a : R), M (C a * T n)
a : R
⊢ C a = C a * T 0

Proof state:
R : Type u_1
inst✝ : Semiring R
M : R[T;T⁻¹] → Prop
p : R[T;T⁻¹]
h_add : ∀ (p q : R[T;T⁻¹]), M p → M q → M (p + q)
h_C_mul_T : ∀ (n : ℤ) (a : R), M (C a * T n)
⊢ M p

Tactic:
refine p.induction_on (fun a => ?_) (fun {p q} => h_add p q) ?_ ?_ <;>
    try exact fun n f _ => h_C_mul_T _ f

Result:
case refine_1
R : Type u_1
inst✝ : Semiring R
M : R[T;T⁻¹] → Prop
p : R[T;T⁻¹]
h_add : ∀ (p q : R[T;T⁻¹]), M p → M q → M (p + q)
h_C_mul_T : ∀ (n : ℤ) (a : R), M (C a * T n)
a : R
⊢ M (C a)

Proof state:
case refine_3
R : Type u_1
inst✝ : Semiring R
M : R[T;T⁻¹] → Prop
p : R[T;T⁻¹]
h_add : ∀ (p q : R[T;T⁻¹]), M p → M q → M (p + q)
h_C_mul_T : ∀ (n : ℤ) (a : R), M (C a * T n)
⊢ ∀ (n : ℕ) (a : R), M (C a * T (-↑n)) → M (C a * T (-↑n - 1))

Tactic:
exact fun n f _ => h_C_mul_T _ f

Result:
no goals
-- Mathlib/Topology/MetricSpace/Pseudo/Defs.lean
theorem ball_subset (h : dist x y ≤ ε₂ - ε₁) : ball x ε₁ ⊆ ball y ε₂ := fun z zx => by
  rw [← add_sub_cancel ε₁ ε₂]
  exact lt_of_le_of_lt (dist_triangle z x y) (add_lt_add_of_lt_of_le zx h)

Proof state:
α : Type u
inst✝ : PseudoMetricSpace α
x y : α
ε₁ ε₂ : ℝ
h : dist x y ≤ ε₂ - ε₁
z : α
zx : z ∈ ball x ε₁
⊢ z ∈ ball y (ε₁ + (ε₂ - ε₁))

Tactic:
exact lt_of_le_of_lt (dist_triangle z x y) (add_lt_add_of_lt_of_le zx h)

Result:
no goals

Proof state:
α : Type u
inst✝ : PseudoMetricSpace α
x y : α
ε₁ ε₂ : ℝ
h : dist x y ≤ ε₂ - ε₁
z : α
zx : z ∈ ball x ε₁
⊢ z ∈ ball y ε₂

Tactic:
rw [← add_sub_cancel ε₁ ε₂]

Result:
α : Type u
inst✝ : PseudoMetricSpace α
x y : α
ε₁ ε₂ : ℝ
h : dist x y ≤ ε₂ - ε₁
z : α
zx : z ∈ ball x ε₁
⊢ z ∈ ball y (ε₁ + (ε₂ - ε₁))
-- Mathlib/Data/Matroid/Closure.lean
lemma Indep.not_mem_closure_iff (hI : M.Indep I) (he : e ∈ M.E

Proof state:
α : Type u_2
M : Matroid α
e : α
I : Set α
hI : M.Indep I
he : autoParam (e ∈ M.E) _auto✝
⊢ ¬(¬M.Indep (insert e I) ∨ e ∈ I) ↔ M.Indep (insert e I) ∧ e ∉ I

Tactic:
tauto

Result:
no goals

Proof state:
α : Type u_2
M : Matroid α
e : α
I : Set α
hI : M.Indep I
he : autoParam (e ∈ M.E) _auto✝
⊢ e ∉ M.closure I ↔ M.Indep (insert e I) ∧ e ∉ I

Tactic:
rw [hI.mem_closure_iff, dep_iff, insert_subset_iff, and_iff_right he,
  and_iff_left hI.subset_ground]

Result:
α : Type u_2
M : Matroid α
e : α
I : Set α
hI : M.Indep I
he : autoParam (e ∈ M.E) _auto✝
⊢ ¬(¬M.Indep (insert e I) ∨ e ∈ I) ↔ M.Indep (insert e I) ∧ e ∉ I
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Int/Order.lean
theorem neg_lt_sub_left_of_lt_add {a b c : Int} (h : c < a + b) : -a < b - c

Proof state:
a b c : Int
h✝ : c < a + b
h : -a < -c + b
⊢ -a < b - c

Tactic:
rwa [Int.add_comm] at h

Result:
no goals

Proof state:
a b c : Int
h : c < a + b
⊢ -a < b - c

Tactic:
have h := Int.lt_neg_add_of_add_lt (Int.sub_left_lt_of_lt_add h)

Result:
a b c : Int
h✝ : c < a + b
h : -a < -c + b
⊢ -a < b - c
-- Mathlib/Combinatorics/Additive/Corner/Defs.lean
lemma isCornerFree_image (hf : IsAddFreimanIso 2 s t f) (hAs : A ⊆ s ×ˢ s) :
    IsCornerFree (Prod.map f f '' A) ↔ IsCornerFree A

Proof state:
G : Type u_1
H : Type u_2
inst✝¹ : AddCommMonoid G
inst✝ : AddCommMonoid H
A : Set (G × G)
s : Set G
t : Set H
f : G → H
hf : IsAddFreimanIso 2 s t f
hAs : A ⊆ s ×ˢ s
this : Prod.map f f '' A ⊆ t ×ˢ t
⊢ (∀ ⦃x₁ : H⦄,
      x₁ ∈ t →
        ∀ ⦃y₁ : H⦄,
          y₁ ∈ t → ∀ ⦃x₂ : H⦄, x₂ ∈ t → ∀ ⦃y₂ : H⦄, y₂ ∈ t → IsCorner (Prod.map f f '' A) x₁ y₁ x₂ y₂ → x₁ = x₂) ↔
    ∀ ⦃x₁ : G⦄, x₁ ∈ s → ∀ ⦃y₁ : G⦄, y₁ ∈ s → ∀ ⦃x₂ : G⦄, x₂ ∈ s → ∀ ⦃y₂ : G⦄, y₂ ∈ s → IsCorner A x₁ y₁ x₂ y₂ → x₁ = x₂

Tactic:
simp +contextual only [hf.bijOn.forall, isCorner_image hf hAs, hf.bijOn.injOn.eq_iff]

Result:
no goals

Proof state:
G : Type u_1
H : Type u_2
inst✝¹ : AddCommMonoid G
inst✝ : AddCommMonoid H
A : Set (G × G)
s : Set G
t : Set H
f : G → H
hf : IsAddFreimanIso 2 s t f
hAs : A ⊆ s ×ˢ s
⊢ IsCornerFree (Prod.map f f '' A) ↔ IsCornerFree A

Tactic:
have : Prod.map f f '' A ⊆ t ×ˢ t :=
  ((hf.bijOn.mapsTo.prodMap hf.bijOn.mapsTo).mono hAs Subset.rfl).image_subset

Result:
G : Type u_1
H : Type u_2
inst✝¹ : AddCommMonoid G
inst✝ : AddCommMonoid H
A : Set (G × G)
s : Set G
t : Set H
f : G → H
hf : IsAddFreimanIso 2 s t f
hAs : A ⊆ s ×ˢ s
this : Prod.map f f '' A ⊆ t ×ˢ t
⊢ IsCornerFree (Prod.map f f '' A) ↔ IsCornerFree A

Proof state:
G : Type u_1
H : Type u_2
inst✝¹ : AddCommMonoid G
inst✝ : AddCommMonoid H
A : Set (G × G)
s : Set G
t : Set H
f : G → H
hf : IsAddFreimanIso 2 s t f
hAs : A ⊆ s ×ˢ s
this : Prod.map f f '' A ⊆ t ×ˢ t
⊢ IsCornerFree (Prod.map f f '' A) ↔ IsCornerFree A

Tactic:
rw [isCornerFree_iff hAs, isCornerFree_iff this]

Result:
G : Type u_1
H : Type u_2
inst✝¹ : AddCommMonoid G
inst✝ : AddCommMonoid H
A : Set (G × G)
s : Set G
t : Set H
f : G → H
hf : IsAddFreimanIso 2 s t f
hAs : A ⊆ s ×ˢ s
this : Prod.map f f '' A ⊆ t ×ˢ t
⊢ (∀ ⦃x₁ : H⦄,
      x₁ ∈ t →
        ∀ ⦃y₁ : H⦄,
          y₁ ∈ t → ∀ ⦃x₂ : H⦄, x₂ ∈ t → ∀ ⦃y₂ : H⦄, y₂ ∈ t → IsCorner (Prod.map f f '' A) x₁ y₁ x₂ y₂ → x₁ = x₂) ↔
    ∀ ⦃x₁ : G⦄, x₁ ∈ s → ∀ ⦃y₁ : G⦄, y₁ ∈ s → ∀ ⦃x₂ : G⦄, x₂ ∈ s → ∀ ⦃y₂ : G⦄, y₂ ∈ s → IsCorner A x₁ y₁ x₂ y₂ → x₁ = x₂
-- Mathlib/Topology/Basic.lean
theorem isOpen_setOf_eventually_nhds {p : X → Prop} : IsOpen { x | ∀ᶠ y in 𝓝 x, p y }

Proof state:
X : Type u
inst✝ : TopologicalSpace X
p : X → Prop
⊢ IsOpen {x | ∀ᶠ (y : X) in 𝓝 x, p y}

Tactic:
simp only [← interior_setOf_eq, isOpen_interior]

Result:
no goals
-- Mathlib/Algebra/Homology/ShortComplex/Exact.lean
@[reassoc (attr := simp, nolint unusedHavesSuffices)]
lemma Exact.comp_descToInjective
    (hS : S.Exact) {J : C} (f : S.X₂ ⟶ J) [Injective J] (hf : S.f ≫ f = 0) :
    S.g ≫ hS.descToInjective f hf = f

Proof state:
C : Type u_1
inst✝² : Category.{u_3, u_1} C
inst✝¹ : Abelian C
S : ShortComplex C
hS : S.Exact
J : C
f : S.X₂ ⟶ J
inst✝ : Injective J
hf : S.f ≫ f = 0
⊢ S.g ≫ hS.descToInjective f hf = f

Tactic:
have := hS.mono_fromOpcycles

Result:
C : Type u_1
inst✝² : Category.{u_3, u_1} C
inst✝¹ : Abelian C
S : ShortComplex C
hS : S.Exact
J : C
f : S.X₂ ⟶ J
inst✝ : Injective J
hf : S.f ≫ f = 0
this : Mono S.fromOpcycles
⊢ S.g ≫ hS.descToInjective f hf = f

Proof state:
C : Type u_1
inst✝² : Category.{u_3, u_1} C
inst✝¹ : Abelian C
S : ShortComplex C
hS : S.Exact
J : C
f : S.X₂ ⟶ J
inst✝ : Injective J
hf : S.f ≫ f = 0
this : Mono S.fromOpcycles
⊢ S.g ≫ Injective.factorThru (S.descOpcycles f hf) S.fromOpcycles = f

Tactic:
simp only [← p_fromOpcycles, assoc, Injective.comp_factorThru, p_descOpcycles]

Result:
no goals

Proof state:
C : Type u_1
inst✝² : Category.{u_3, u_1} C
inst✝¹ : Abelian C
S : ShortComplex C
hS : S.Exact
J : C
f : S.X₂ ⟶ J
inst✝ : Injective J
hf : S.f ≫ f = 0
this : Mono S.fromOpcycles
⊢ S.g ≫ hS.descToInjective f hf = f

Tactic:
dsimp [descToInjective]

Result:
C : Type u_1
inst✝² : Category.{u_3, u_1} C
inst✝¹ : Abelian C
S : ShortComplex C
hS : S.Exact
J : C
f : S.X₂ ⟶ J
inst✝ : Injective J
hf : S.f ≫ f = 0
this : Mono S.fromOpcycles
⊢ S.g ≫ Injective.factorThru (S.descOpcycles f hf) S.fromOpcycles = f
-- Mathlib/AlgebraicGeometry/IdealSheaf.lean
lemma support_inter (I : IdealSheafData X) (U : X.affineOpens) :
    I.support ∩ U = X.zeroLocus (U := U.1) (I.ideal U) ∩ U

Proof state:
case neg
X : Scheme
I : X.IdealSheafData
U : ↑X.affineOpens
x : ↑↑X.toPresheafedSpace
hxU : x ∉ ↑U
⊢ x ∈ I.support ∩ ↑↑U ↔ x ∈ X.zeroLocus ↑(I.ideal U) ∩ ↑↑U

Tactic:
simp [hxU]

Result:
no goals

Proof state:
case h
X : Scheme
I : X.IdealSheafData
U : ↑X.affineOpens
x : ↑↑X.toPresheafedSpace
⊢ x ∈ I.support ∩ ↑↑U ↔ x ∈ X.zeroLocus ↑(I.ideal U) ∩ ↑↑U

Tactic:
by_cases hxU : x ∈ U.1

Result:
case pos
X : Scheme
I : X.IdealSheafData
U : ↑X.affineOpens
x : ↑↑X.toPresheafedSpace
hxU : x ∈ ↑U
⊢ x ∈ I.support ∩ ↑↑U ↔ x ∈ X.zeroLocus ↑(I.ideal U) ∩ ↑↑U

case neg
X : Scheme
I : X.IdealSheafData
U : ↑X.affineOpens
x : ↑↑X.toPresheafedSpace
hxU : x ∉ ↑U
⊢ x ∈ I.support ∩ ↑↑U ↔ x ∈ X.zeroLocus ↑(I.ideal U) ∩ ↑↑U

Proof state:
case pos
X : Scheme
I : X.IdealSheafData
U : ↑X.affineOpens
x : ↑↑X.toPresheafedSpace
hxU : x ∈ ↑U
⊢ x ∈ I.support ∩ ↑↑U ↔ x ∈ X.zeroLocus ↑(I.ideal U) ∩ ↑↑U

Tactic:
simp [hxU, mem_support_iff_of_mem hxU]

Result:
no goals

Proof state:
X : Scheme
I : X.IdealSheafData
U : ↑X.affineOpens
⊢ I.support ∩ ↑↑U = X.zeroLocus ↑(I.ideal U) ∩ ↑↑U

Tactic:
ext x

Result:
case h
X : Scheme
I : X.IdealSheafData
U : ↑X.affineOpens
x : ↑↑X.toPresheafedSpace
⊢ x ∈ I.support ∩ ↑↑U ↔ x ∈ X.zeroLocus ↑(I.ideal U) ∩ ↑↑U
-- Mathlib/Computability/Partrec.lean
theorem rfind_min' {p : ℕ → Bool} {m : ℕ} (pm : p m) : ∃ n ∈ rfind p, n ≤ m :=
  have : true ∈ (p : ℕ →. Bool) m := ⟨trivial, pm⟩
  let ⟨n, hn⟩ := dom_iff_mem.1 <| (@rfind_dom p).2 ⟨m, this, fun {_} _ => ⟨⟩⟩
  ⟨n, hn, not_lt.1 fun h => by injection mem_unique this (rfind_min hn h)⟩

Proof state:
p : ℕ → Bool
m : ℕ
pm : p m = true
this : true ∈ ↑p m
n : ℕ
hn : n ∈ rfind ↑p
h : m < n
⊢ False

Tactic:
injection mem_unique this (rfind_min hn h)

Result:
no goals
-- Mathlib/Data/List/Sort.lean
theorem Sorted.le_head! [Inhabited α] [Preorder α] {a : α} {l : List α} (h : Sorted (· > ·) l)
    (ha : a ∈ l) : a ≤ l.head!

Proof state:
α : Type u
inst✝¹ : Inhabited α
inst✝ : Preorder α
a : α
l : List α
h : Sorted (fun x1 x2 => x1 > x2) (l.head! :: l.tail)
ha : a ∈ l.head! :: l.tail
⊢ a ≤ l.head!

Tactic:
cases ha

Result:
case head
α : Type u
inst✝¹ : Inhabited α
inst✝ : Preorder α
l : List α
h : Sorted (fun x1 x2 => x1 > x2) (l.head! :: l.tail)
⊢ l.head! ≤ l.head!

case tail
α : Type u
inst✝¹ : Inhabited α
inst✝ : Preorder α
a : α
l : List α
h : Sorted (fun x1 x2 => x1 > x2) (l.head! :: l.tail)
a✝ : Mem a l.tail
⊢ a ≤ l.head!

Proof state:
α : Type u
inst✝¹ : Inhabited α
inst✝ : Preorder α
a : α
l : List α
h : Sorted (fun x1 x2 => x1 > x2) l
ha : a ∈ l
⊢ a ≤ l.head!

Tactic:
rw [← List.cons_head!_tail (List.ne_nil_of_mem ha)] at h ha

Result:
α : Type u
inst✝¹ : Inhabited α
inst✝ : Preorder α
a : α
l : List α
h : Sorted (fun x1 x2 => x1 > x2) (l.head! :: l.tail)
ha : a ∈ l.head! :: l.tail
⊢ a ≤ l.head!

Proof state:
case head
α : Type u
inst✝¹ : Inhabited α
inst✝ : Preorder α
l : List α
h : Sorted (fun x1 x2 => x1 > x2) (l.head! :: l.tail)
⊢ l.head! ≤ l.head!

Tactic:
exact le_rfl

Result:
no goals

Proof state:
case tail
α : Type u
inst✝¹ : Inhabited α
inst✝ : Preorder α
a : α
l : List α
h : Sorted (fun x1 x2 => x1 > x2) (l.head! :: l.tail)
a✝ : Mem a l.tail
⊢ a ≤ l.head!

Tactic:
exact le_of_lt (rel_of_sorted_cons h a (by assumption))

Result:
no goals

Proof state:
α : Type u
inst✝¹ : Inhabited α
inst✝ : Preorder α
a : α
l : List α
h : Sorted (fun x1 x2 => x1 > x2) (l.head! :: l.tail)
a✝ : Mem a l.tail
⊢ a ∈ l.tail

Tactic:
assumption

Result:
no goals
-- Mathlib/Algebra/Group/Pointwise/Set/Basic.lean
@[to_additive]
lemma Nontrivial.mul_right : s.Nontrivial → t.Nonempty → (s * t).Nontrivial

Proof state:
α : Type u_2
inst✝¹ : Mul α
inst✝ : IsRightCancelMul α
s t : Set α
⊢ s.Nontrivial → t.Nonempty → (s * t).Nontrivial

Tactic:
rintro ⟨a, ha, b, hb, hab⟩ ⟨c, hc⟩

Result:
case intro.intro.intro.intro.intro
α : Type u_2
inst✝¹ : Mul α
inst✝ : IsRightCancelMul α
s t : Set α
a : α
ha : a ∈ s
b : α
hb : b ∈ s
hab : a ≠ b
c : α
hc : c ∈ t
⊢ (s * t).Nontrivial

Proof state:
case intro.intro.intro.intro.intro
α : Type u_2
inst✝¹ : Mul α
inst✝ : IsRightCancelMul α
s t : Set α
a : α
ha : a ∈ s
b : α
hb : b ∈ s
hab : a ≠ b
c : α
hc : c ∈ t
⊢ (s * t).Nontrivial

Tactic:
exact ⟨a * c, mul_mem_mul ha hc, b * c, mul_mem_mul hb hc, by simpa⟩

Result:
no goals

Proof state:
α : Type u_2
inst✝¹ : Mul α
inst✝ : IsRightCancelMul α
s t : Set α
a : α
ha : a ∈ s
b : α
hb : b ∈ s
hab : a ≠ b
c : α
hc : c ∈ t
⊢ a * c ≠ b * c

Tactic:
simpa

Result:
no goals
-- Mathlib/Analysis/SpecialFunctions/Trigonometric/Angle.lean
theorem toReal_neg_iff_sign_neg {θ : Angle} : θ.toReal < 0 ↔ θ.sign = -1

Proof state:
case inl
θ : Angle
h : θ.toReal < 0
⊢ θ.toReal < 0 ↔ Real.sin θ.toReal < 0

Tactic:
exact ⟨fun _ => Real.sin_neg_of_neg_of_neg_pi_lt h (neg_pi_lt_toReal θ), fun _ => h⟩

Result:
no goals

Proof state:
θ : Angle
⊢ θ.toReal < 0 ↔ θ.sign = -1

Tactic:
rw [sign, ← sin_toReal, sign_eq_neg_one_iff]

Result:
θ : Angle
⊢ θ.toReal < 0 ↔ Real.sin θ.toReal < 0

Proof state:
case inr.inl
θ : Angle
h : θ.toReal = 0
⊢ θ.toReal < 0 ↔ Real.sin θ.toReal < 0

Tactic:
simp [h]

Result:
no goals

Proof state:
θ : Angle
⊢ θ.toReal < 0 ↔ Real.sin θ.toReal < 0

Tactic:
rcases lt_trichotomy θ.toReal 0 with (h | h | h)

Result:
case inl
θ : Angle
h : θ.toReal < 0
⊢ θ.toReal < 0 ↔ Real.sin θ.toReal < 0

case inr.inl
θ : Angle
h : θ.toReal = 0
⊢ θ.toReal < 0 ↔ Real.sin θ.toReal < 0

case inr.inr
θ : Angle
h : 0 < θ.toReal
⊢ θ.toReal < 0 ↔ Real.sin θ.toReal < 0

Proof state:
case inr.inr
θ : Angle
h : 0 < θ.toReal
⊢ θ.toReal < 0 ↔ Real.sin θ.toReal < 0

Tactic:
exact
  ⟨fun hn => False.elim (h.asymm hn), fun hn =>
    False.elim (hn.not_le (sin_nonneg_of_nonneg_of_le_pi h.le (toReal_le_pi θ)))⟩

Result:
no goals
-- Mathlib/Topology/Category/TopCat/Opens.lean
theorem map_id_eq : map (𝟙 X) = 𝟭 (Opens X)

Proof state:
X : TopCat
⊢ map (𝟙 X) = 𝟭 (Opens ↑X)

Tactic:
rfl

Result:
no goals
-- Mathlib/SetTheory/ZFC/Basic.lean
theorem ofSet.inj {x y : ZFSet.{u}} (h : (x : Class.{u}) = y) : x = y :=
  ZFSet.ext fun z => by
    change (x : Class.{u}) z ↔ (y : Class.{u}) z
    rw [h]

Proof state:
x y : ZFSet.{u}
h : ↑x = ↑y
z : ZFSet.{u}
⊢ ↑x z ↔ ↑y z

Tactic:
rw [h]

Result:
no goals

Proof state:
x y : ZFSet.{u}
h : ↑x = ↑y
z : ZFSet.{u}
⊢ z ∈ x ↔ z ∈ y

Tactic:
change (x : Class.{u}) z ↔ (y : Class.{u}) z

Result:
x y : ZFSet.{u}
h : ↑x = ↑y
z : ZFSet.{u}
⊢ ↑x z ↔ ↑y z