harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Int/Order.lean
theorem lt_neg_add_of_add_lt {a b c : Int} (h : a + b < c) : b < -a + c

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

Tactic:
have h := Int.add_lt_add_left h (-a)

Result:
a b c : Int
h✝ : a + b < c
h : -a + (a + b) < -a + c
⊢ b < -a + c

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

Tactic:
rwa [Int.neg_add_cancel_left] at h

Result:
no goals
-- Mathlib/Topology/Basic.lean
theorem ClusterPt.of_le_nhds {f : Filter X} (H : f ≤ 𝓝 x) [NeBot f] : ClusterPt x f

Proof state:
X : Type u
x : X
inst✝¹ : TopologicalSpace X
f : Filter X
H : f ≤ 𝓝 x
inst✝ : f.NeBot
⊢ ClusterPt x f

Tactic:
rwa [ClusterPt, inf_eq_right.mpr H]

Result:
no goals
-- Mathlib/GroupTheory/Perm/Centralizer.lean
theorem card_of_cycleType_eq_zero_iff {m : Multiset ℕ} :
    ({g | g.cycleType = m} : Finset (Perm α)).card = 0
      ↔ ¬ ((m.sum ≤ Fintype.card α ∧ ∀ a ∈ m, 2 ≤ a))

Proof state:
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
m : Multiset ℕ
⊢ (Finset.filter (fun g => g.cycleType = m) Finset.univ).card = 0 ↔ ¬(m.sum ≤ Fintype.card α ∧ ∀ a ∈ m, 2 ≤ a)

Tactic:
rw [Finset.card_eq_zero, Finset.filter_eq_empty_iff,
  ← exists_with_cycleType_iff, not_exists]

Result:
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
m : Multiset ℕ
⊢ (∀ ⦃x : Perm α⦄, x ∈ Finset.univ → ¬x.cycleType = m) ↔ ∀ (x : Perm α), ¬x.cycleType = m

Proof state:
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
m : Multiset ℕ
⊢ (∀ ⦃x : Perm α⦄, x ∈ Finset.univ → ¬x.cycleType = m) ↔ ∀ (x : Perm α), ¬x.cycleType = m

Tactic:
aesop

Result:
no goals
-- Mathlib/Data/Matroid/Restrict.lean
theorem Indep.exists_insert_of_not_isBasis (hI : M.Indep I) (hIX : I ⊆ X) (hI' : ¬M.IsBasis I X)
    (hJ : M.IsBasis J X) : ∃ e ∈ J \ I, M.Indep (insert e I)

Proof state:
case intro.intro
α : Type u_1
M : Matroid α
I X J : Set α
hI : M.Indep I
hIX : I ⊆ X
hI' : ¬(M ↾ X).IsBase I
hJ : (M ↾ X).IsBase J
e : α
he : e ∈ J \ I
hi : (M ↾ X).Indep (insert e I)
⊢ ∃ e ∈ J \ I, M.Indep (insert e I)

Tactic:
exact ⟨e, he, (restrict_indep_iff.mp hi).1⟩

Result:
no goals

Proof state:
α : Type u_1
M : Matroid α
I X J : Set α
hI : M.Indep I
hIX : I ⊆ X
hI' : ¬(M ↾ X).IsBase I
hJ : (M ↾ X).IsBase J
⊢ ∃ e ∈ J \ I, M.Indep (insert e I)

Tactic:
obtain ⟨e, he, hi⟩ := (hI.indep_restrict_of_subset hIX).exists_insert_of_not_isBase hI' hJ

Result:
case intro.intro
α : Type u_1
M : Matroid α
I X J : Set α
hI : M.Indep I
hIX : I ⊆ X
hI' : ¬(M ↾ X).IsBase I
hJ : (M ↾ X).IsBase J
e : α
he : e ∈ J \ I
hi : (M ↾ X).Indep (insert e I)
⊢ ∃ e ∈ J \ I, M.Indep (insert e I)

Proof state:
α : Type u_1
M : Matroid α
I X J : Set α
hI : M.Indep I
hIX : I ⊆ X
hI' : ¬(M ↾ X).IsBase I
hJ : M.IsBasis J X
⊢ ∃ e ∈ J \ I, M.Indep (insert e I)

Tactic:
rw [← isBase_restrict_iff] at hJ

Result:
α : Type u_1
M : Matroid α
I X J : Set α
hI : M.Indep I
hIX : I ⊆ X
hI' : ¬(M ↾ X).IsBase I
hJ : (M ↾ X).IsBase J
⊢ ∃ e ∈ J \ I, M.Indep (insert e I)

Proof state:
α : Type u_1
M : Matroid α
I X J : Set α
hI : M.Indep I
hIX : I ⊆ X
hI' : ¬M.IsBasis I X
hJ : M.IsBasis J X
⊢ ∃ e ∈ J \ I, M.Indep (insert e I)

Tactic:
rw [← isBase_restrict_iff] at hI'

Result:
α : Type u_1
M : Matroid α
I X J : Set α
hI : M.Indep I
hIX : I ⊆ X
hI' : ¬(M ↾ X).IsBase I
hJ : M.IsBasis J X
⊢ ∃ e ∈ J \ I, M.Indep (insert e I)
-- Mathlib/Algebra/Order/Rearrangement.lean
theorem MonovaryOn.sum_smul_comp_perm_eq_sum_smul_iff (hfg : MonovaryOn f g s)
    (hσ : {x | σ x ≠ x} ⊆ s) :
    ∑ i ∈ s, f i • g (σ i) = ∑ i ∈ s, f i • g i ↔ MonovaryOn f (g ∘ σ) s

Proof state:
case refine_2
ι : Type u_1
α : Type u_2
β : Type u_3
inst✝⁴ : LinearOrderedSemiring α
inst✝³ : ExistsAddOfLE α
inst✝² : LinearOrderedCancelAddCommMonoid β
inst✝¹ : Module α β
inst✝ : PosSMulStrictMono α β
s : Finset ι
σ : Perm ι
f : ι → α
g : ι → β
hfg : MonovaryOn f g ↑s
hσ : {x | σ x ≠ x} ⊆ ↑s
h : MonovaryOn f (g ∘ ⇑σ) ↑s
⊢ ∑ i ∈ s, f i • g i ≤ ∑ i ∈ s, f i • g (σ i)

Tactic:
convert h.sum_smul_comp_perm_le_sum_smul ((set_support_inv_eq _).subset.trans hσ) using 1

Result:
case h.e'_3
ι : Type u_1
α : Type u_2
β : Type u_3
inst✝⁴ : LinearOrderedSemiring α
inst✝³ : ExistsAddOfLE α
inst✝² : LinearOrderedCancelAddCommMonoid β
inst✝¹ : Module α β
inst✝ : PosSMulStrictMono α β
s : Finset ι
σ : Perm ι
f : ι → α
g : ι → β
hfg : MonovaryOn f g ↑s
hσ : {x | σ x ≠ x} ⊆ ↑s
h : MonovaryOn f (g ∘ ⇑σ) ↑s
⊢ ∑ i ∈ s, f i • g i = ∑ i ∈ s, f i • (g ∘ ⇑σ) (σ⁻¹ i)

Proof state:
ι : Type u_1
α : Type u_2
β : Type u_3
inst✝⁴ : LinearOrderedSemiring α
inst✝³ : ExistsAddOfLE α
inst✝² : LinearOrderedCancelAddCommMonoid β
inst✝¹ : Module α β
inst✝ : PosSMulStrictMono α β
s : Finset ι
σ : Perm ι
f : ι → α
g : ι → β
hfg : MonovaryOn f g ↑s
hσ : {x | σ x ≠ x} ⊆ ↑s
⊢ ∑ i ∈ s, f i • g (σ i) = ∑ i ∈ s, f i • g i ↔ MonovaryOn f (g ∘ ⇑σ) ↑s

Tactic:
refine ⟨not_imp_not.1 fun h ↦ ?_, fun h ↦ (hfg.sum_smul_comp_perm_le_sum_smul hσ).antisymm ?_⟩

Result:
case refine_1
ι : Type u_1
α : Type u_2
β : Type u_3
inst✝⁴ : LinearOrderedSemiring α
inst✝³ : ExistsAddOfLE α
inst✝² : LinearOrderedCancelAddCommMonoid β
inst✝¹ : Module α β
inst✝ : PosSMulStrictMono α β
s : Finset ι
σ : Perm ι
f : ι → α
g : ι → β
hfg : MonovaryOn f g ↑s
hσ : {x | σ x ≠ x} ⊆ ↑s
h : ¬MonovaryOn f (g ∘ ⇑σ) ↑s
⊢ ¬∑ i ∈ s, f i • g (σ i) = ∑ i ∈ s, f i • g i

case refine_2
ι : Type u_1
α : Type u_2
β : Type u_3
inst✝⁴ : LinearOrderedSemiring α
inst✝³ : ExistsAddOfLE α
inst✝² : LinearOrderedCancelAddCommMonoid β
inst✝¹ : Module α β
inst✝ : PosSMulStrictMono α β
s : Finset ι
σ : Perm ι
f : ι → α
g : ι → β
hfg : MonovaryOn f g ↑s
hσ : {x | σ x ≠ x} ⊆ ↑s
h : MonovaryOn f (g ∘ ⇑σ) ↑s
⊢ ∑ i ∈ s, f i • g i ≤ ∑ i ∈ s, f i • g (σ i)
-- Mathlib/RingTheory/Spectrum/Prime/Topology.lean
theorem isClosed_range_comap_of_surjective (hf : Surjective f) :
    IsClosed (Set.range (comap f))

Proof state:
R : Type u
S : Type v
inst✝¹ : CommRing R
inst✝ : CommRing S
f : R →+* S
hf : Surjective ⇑f
⊢ IsClosed (zeroLocus ↑(ker f))

Tactic:
exact isClosed_zeroLocus _

Result:
no goals

Proof state:
R : Type u
S : Type v
inst✝¹ : CommRing R
inst✝ : CommRing S
f : R →+* S
hf : Surjective ⇑f
⊢ IsClosed (Set.range ⇑(comap f))

Tactic:
rw [range_comap_of_surjective _ f hf]

Result:
R : Type u
S : Type v
inst✝¹ : CommRing R
inst✝ : CommRing S
f : R →+* S
hf : Surjective ⇑f
⊢ IsClosed (zeroLocus ↑(ker f))
-- Mathlib/Data/ZMod/Units.lean
/-- Any element of `ZMod N` has the form `u * d` where `u` is a unit and `d` is a divisor of `N`. -/
lemma eq_unit_mul_divisor {N : ℕ} (a : ZMod N) :
    ∃ d : ℕ, d ∣ N ∧ ∃ (u : ZMod N), IsUnit u ∧ a = u * d

Proof state:
case inr.intro.intro
N : ℕ
a : ZMod N
hN : N ≠ 0
this : NeZero N
d : ℕ := a.val.gcd N
hd : d ≠ 0
a₀ : ℕ
ha₀ : a.val = d * a₀
N₀ : ℕ
hN₀ : N = d * N₀
⊢ ∃ u, IsUnit u ∧ a = u * ↑d

Tactic:
have hu₀ : IsUnit (a₀ : ZMod N₀) := by
  refine (isUnit_iff_coprime _ _).mpr (Nat.isCoprime_iff_coprime.mp ?_)
  obtain ⟨p, q, hpq⟩ : ∃ (p q : ℤ), d = a.val * p + N * q := ⟨_, _, Nat.gcd_eq_gcd_ab _ _⟩
  rw [ha₀, hN₀, Nat.cast_mul, Nat.cast_mul, mul_assoc, mul_assoc, ← mul_add, eq_comm,
    mul_comm _ p, mul_comm _ q] at hpq
  exact ⟨p, q, Int.eq_one_of_mul_eq_self_right (Nat.cast_ne_zero.mpr hd) hpq⟩

Result:
case inr.intro.intro
N : ℕ
a : ZMod N
hN : N ≠ 0
this : NeZero N
d : ℕ := a.val.gcd N
hd : d ≠ 0
a₀ : ℕ
ha₀ : a.val = d * a₀
N₀ : ℕ
hN₀ : N = d * N₀
hu₀ : IsUnit ↑a₀
⊢ ∃ u, IsUnit u ∧ a = u * ↑d

Proof state:
case inl.inr.inr
a : ℤ
ha : a ≠ 0
h : a > 0
⊢ IsUnit a.sign

Tactic:
simp only [Int.sign_eq_one_of_pos h, isUnit_one]

Result:
no goals

Proof state:
⊢ 0 = 1 * ↑0

Tactic:
rw [Nat.cast_zero, mul_zero]

Result:
no goals

Proof state:
case inr.intro.intro.intro
N : ℕ
a : ZMod N
hN : N ≠ 0
this : NeZero N
d : ℕ := a.val.gcd N
hd : d ≠ 0
a₀ : ℕ
ha₀ : a.val = d * a₀
N₀ : ℕ
hN₀ : N = d * N₀
hu₀ : IsUnit ↑a₀
u : (ZMod N)ˣ
hu : (castHom ⋯ (ZMod N₀)) ↑u = ↑a₀
⊢ d * a₀ % N = d * (↑u).val % N

Tactic:
simp only [hN₀, Nat.mul_mod_mul_left, Nat.mul_right_inj hd]

Result:
case inr.intro.intro.intro
N : ℕ
a : ZMod N
hN : N ≠ 0
this : NeZero N
d : ℕ := a.val.gcd N
hd : d ≠ 0
a₀ : ℕ
ha₀ : a.val = d * a₀
N₀ : ℕ
hN₀ : N = d * N₀
hu₀ : IsUnit ↑a₀
u : (ZMod N)ˣ
hu : (castHom ⋯ (ZMod N₀)) ↑u = ↑a₀
⊢ a₀ % N₀ = (↑u).val % N₀

Proof state:
case inr
N : ℕ
a : ZMod N
hN : N ≠ 0
⊢ ∃ d, d ∣ N ∧ ∃ u, IsUnit u ∧ a = u * ↑d

Tactic:
have : NeZero N := ⟨hN⟩

Result:
case inr
N : ℕ
a : ZMod N
hN : N ≠ 0
this : NeZero N
⊢ ∃ d, d ∣ N ∧ ∃ u, IsUnit u ∧ a = u * ↑d

Proof state:
case inr
N : ℕ
a : ZMod N
hN : N ≠ 0
this : NeZero N
d : ℕ := a.val.gcd N
hd : d ≠ 0
⊢ ∃ d, d ∣ N ∧ ∃ u, IsUnit u ∧ a = u * ↑d

Tactic:
obtain ⟨a₀, (ha₀ : _ = d * _)⟩ := a.val.gcd_dvd_left N

Result:
case inr.intro
N : ℕ
a : ZMod N
hN : N ≠ 0
this : NeZero N
d : ℕ := a.val.gcd N
hd : d ≠ 0
a₀ : ℕ
ha₀ : a.val = d * a₀
⊢ ∃ d, d ∣ N ∧ ∃ u, IsUnit u ∧ a = u * ↑d
-- Mathlib/Data/List/Sigma.lean
theorem nodupKeys_flatten {L : List (List (Sigma β))} :
    NodupKeys (flatten L) ↔ (∀ l ∈ L, NodupKeys l) ∧ Pairwise Disjoint (L.map keys)

Proof state:
α : Type u
β : α → Type v
L : List (List (Sigma β))
⊢ (∀ l ∈ L, Pairwise (fun s s' => s.fst ≠ s'.fst) l) ∧ Pairwise (fun l₁ l₂ => ∀ x ∈ l₁, ∀ y ∈ l₂, x.fst ≠ y.fst) L ↔
    (∀ l ∈ L, l.NodupKeys) ∧ Pairwise (fun a b => a.keys.Disjoint b.keys) L

Tactic:
refine and_congr (forall₂_congr fun l _ => by simp [nodupKeys_iff_pairwise]) ?_

Result:
α : Type u
β : α → Type v
L : List (List (Sigma β))
⊢ Pairwise (fun l₁ l₂ => ∀ x ∈ l₁, ∀ y ∈ l₂, x.fst ≠ y.fst) L ↔ Pairwise (fun a b => a.keys.Disjoint b.keys) L

Proof state:
α : Type u
β : α → Type v
L : List (List (Sigma β))
⊢ Pairwise (fun l₁ l₂ => ∀ x ∈ l₁, ∀ y ∈ l₂, x.fst ≠ y.fst) L ↔ Pairwise (fun a b => a.keys.Disjoint b.keys) L

Tactic:
apply iff_of_eq

Result:
case a
α : Type u
β : α → Type v
L : List (List (Sigma β))
⊢ Pairwise (fun l₁ l₂ => ∀ x ∈ l₁, ∀ y ∈ l₂, x.fst ≠ y.fst) L = Pairwise (fun a b => a.keys.Disjoint b.keys) L

Proof state:
α : Type u
β : α → Type v
L : List (List (Sigma β))
l : List (Sigma β)
x✝ : l ∈ L
⊢ Pairwise (fun s s' => s.fst ≠ s'.fst) l ↔ l.NodupKeys

Tactic:
simp [nodupKeys_iff_pairwise]

Result:
no goals

Proof state:
case a.e_R.h.h.a
α : Type u
β : α → Type v
L : List (List (Sigma β))
l₁ l₂ : List (Sigma β)
⊢ (∀ x ∈ l₁, ∀ y ∈ l₂, x.fst ≠ y.fst) ↔ l₁.keys.Disjoint l₂.keys

Tactic:
simp [keys, disjoint_iff_ne, Sigma.forall]

Result:
no goals

Proof state:
α : Type u
β : α → Type v
L : List (List (Sigma β))
⊢ L.flatten.NodupKeys ↔ (∀ l ∈ L, l.NodupKeys) ∧ Pairwise Disjoint (map keys L)

Tactic:
rw [nodupKeys_iff_pairwise, pairwise_flatten, pairwise_map]

Result:
α : Type u
β : α → Type v
L : List (List (Sigma β))
⊢ (∀ l ∈ L, Pairwise (fun s s' => s.fst ≠ s'.fst) l) ∧ Pairwise (fun l₁ l₂ => ∀ x ∈ l₁, ∀ y ∈ l₂, x.fst ≠ y.fst) L ↔
    (∀ l ∈ L, l.NodupKeys) ∧ Pairwise (fun a b => a.keys.Disjoint b.keys) L

Proof state:
case a
α : Type u
β : α → Type v
L : List (List (Sigma β))
⊢ Pairwise (fun l₁ l₂ => ∀ x ∈ l₁, ∀ y ∈ l₂, x.fst ≠ y.fst) L = Pairwise (fun a b => a.keys.Disjoint b.keys) L

Tactic:
congr with (l₁ l₂)

Result:
case a.e_R.h.h.a
α : Type u
β : α → Type v
L : List (List (Sigma β))
l₁ l₂ : List (Sigma β)
⊢ (∀ x ∈ l₁, ∀ y ∈ l₂, x.fst ≠ y.fst) ↔ l₁.keys.Disjoint l₂.keys
-- Mathlib/GroupTheory/Perm/Support.lean
theorem Disjoint.mul_right (H1 : Disjoint f g) (H2 : Disjoint f h) : Disjoint f (g * h)

Proof state:
α : Type u_1
f g h : Perm α
H1 : f.Disjoint g
H2 : f.Disjoint h
⊢ f.Disjoint (g * h)

Tactic:
rw [disjoint_comm]

Result:
α : Type u_1
f g h : Perm α
H1 : f.Disjoint g
H2 : f.Disjoint h
⊢ (g * h).Disjoint f

Proof state:
α : Type u_1
f g h : Perm α
H1 : f.Disjoint g
H2 : f.Disjoint h
⊢ (g * h).Disjoint f

Tactic:
exact H1.symm.mul_left H2.symm

Result:
no goals
-- Mathlib/Computability/Ackermann.lean
theorem ack_three (n : ℕ) : ack 3 n = 2 ^ (n + 3) - 3

Proof state:
case succ
n : ℕ
IH : ack 3 n = 2 ^ (n + 3) - 3
H : 2 * 3 ≤ 2 * 2 ^ 3
⊢ 2 ^ 3 ≤ 2 ^ (n + 3)

Tactic:
exact pow_right_mono₀ one_le_two (Nat.le_add_left 3 n)

Result:
no goals

Proof state:
n : ℕ
⊢ ack 3 n = 2 ^ (n + 3) - 3

Tactic:
induction' n with n IH

Result:
case zero

⊢ ack 3 0 = 2 ^ (0 + 3) - 3

case succ
n : ℕ
IH : ack 3 n = 2 ^ (n + 3) - 3
⊢ ack 3 (n + 1) = 2 ^ (n + 1 + 3) - 3

Proof state:
case succ
n : ℕ
IH : ack 3 n = 2 ^ (n + 3) - 3
H : 2 * 3 ≤ 2 * 2 ^ 3
⊢ 2 * 3 ≤ 2 * 2 ^ (n + 3)

Tactic:
apply H.trans

Result:
case succ
n : ℕ
IH : ack 3 n = 2 ^ (n + 3) - 3
H : 2 * 3 ≤ 2 * 2 ^ 3
⊢ 2 * 2 ^ 3 ≤ 2 * 2 ^ (n + 3)

Proof state:
n : ℕ
IH : ack 3 n = 2 ^ (n + 3) - 3
⊢ 2 * 3 ≤ 2 * 2 ^ 3

Tactic:
norm_num

Result:
no goals

Proof state:
case succ
n : ℕ
IH : ack 3 n = 2 ^ (n + 3) - 3
⊢ ack 3 (n + 1) = 2 ^ (n + 1 + 3) - 3

Tactic:
rw [ack_succ_succ, IH, ack_two, Nat.succ_add, Nat.pow_succ 2 (n + 3), mul_comm _ 2,
    Nat.mul_sub_left_distrib, ← Nat.sub_add_comm, two_mul 3, Nat.add_sub_add_right]

Result:
case succ
n : ℕ
IH : ack 3 n = 2 ^ (n + 3) - 3
⊢ 2 * 3 ≤ 2 * 2 ^ (n + 3)

Proof state:
case succ
n : ℕ
IH : ack 3 n = 2 ^ (n + 3) - 3
⊢ 2 * 3 ≤ 2 * 2 ^ (n + 3)

Tactic:
have H : 2 * 3 ≤ 2 * 2 ^ 3 := by norm_num

Result:
case succ
n : ℕ
IH : ack 3 n = 2 ^ (n + 3) - 3
H : 2 * 3 ≤ 2 * 2 ^ 3
⊢ 2 * 3 ≤ 2 * 2 ^ (n + 3)

Proof state:
case succ
n : ℕ
IH : ack 3 n = 2 ^ (n + 3) - 3
H : 2 * 3 ≤ 2 * 2 ^ 3
⊢ 2 * 2 ^ 3 ≤ 2 * 2 ^ (n + 3)

Tactic:
rw [_root_.mul_le_mul_left two_pos]

Result:
case succ
n : ℕ
IH : ack 3 n = 2 ^ (n + 3) - 3
H : 2 * 3 ≤ 2 * 2 ^ 3
⊢ 2 ^ 3 ≤ 2 ^ (n + 3)

Proof state:
case zero

⊢ ack 3 0 = 2 ^ (0 + 3) - 3

Tactic:
simp

Result:
no goals
-- Mathlib/Data/Finset/Insert.lean
theorem pairwise_cons' {a : α} (ha : a ∉ s) (r : β → β → Prop) (f : α → β) :
    Pairwise (r on fun a : s.cons a ha => f a) ↔
    Pairwise (r on fun a : s => f a) ∧ ∀ b ∈ s, r (f a) (f b) ∧ r (f b) (f a)

Proof state:
α : Type u_1
β : Type u_2
s : Finset α
a : α
ha : a ∉ s
r : β → β → Prop
f : α → β
x✝ : (↑s).Pairwise (r on f)
h : ∀ b ∈ s, a ≠ b → (r on f) a b ∧ (r on f) b a
hb : a ∈ s
⊢ False

Tactic:
contradiction

Result:
no goals

Proof state:
α : Type u_1
β : Type u_2
s : Finset α
a : α
ha : a ∉ s
r : β → β → Prop
f : α → β
⊢ _root_.Pairwise (r on fun a_1 => f ↑a_1) ↔
    _root_.Pairwise (r on fun a => f ↑a) ∧ ∀ b ∈ s, r (f a) (f b) ∧ r (f b) (f a)

Tactic:
simp only [pairwise_subtype_iff_pairwise_finset', Finset.coe_cons, Set.pairwise_insert,
  Finset.mem_coe, and_congr_right_iff]

Result:
α : Type u_1
β : Type u_2
s : Finset α
a : α
ha : a ∉ s
r : β → β → Prop
f : α → β
⊢ (↑s).Pairwise (r on f) → ((∀ b ∈ s, a ≠ b → (r on f) a b ∧ (r on f) b a) ↔ ∀ b ∈ s, r (f a) (f b) ∧ r (f b) (f a))

Proof state:
α : Type u_1
β : Type u_2
s : Finset α
a : α
ha : a ∉ s
r : β → β → Prop
f : α → β
⊢ (↑s).Pairwise (r on f) → ((∀ b ∈ s, a ≠ b → (r on f) a b ∧ (r on f) b a) ↔ ∀ b ∈ s, r (f a) (f b) ∧ r (f b) (f a))

Tactic:
exact fun _ =>
  ⟨fun h b hb =>
    h b hb <| by
      rintro rfl
      contradiction,
    fun h b hb _ => h b hb⟩

Result:
no goals

Proof state:
α : Type u_1
β : Type u_2
s : Finset α
a : α
ha : a ∉ s
r : β → β → Prop
f : α → β
x✝ : (↑s).Pairwise (r on f)
h : ∀ b ∈ s, a ≠ b → (r on f) a b ∧ (r on f) b a
b : α
hb : b ∈ s
⊢ a ≠ b

Tactic:
rintro rfl

Result:
α : Type u_1
β : Type u_2
s : Finset α
a : α
ha : a ∉ s
r : β → β → Prop
f : α → β
x✝ : (↑s).Pairwise (r on f)
h : ∀ b ∈ s, a ≠ b → (r on f) a b ∧ (r on f) b a
hb : a ∈ s
⊢ False
-- Mathlib/CategoryTheory/Idempotents/Basic.lean
theorem isIdempotentComplete_iff_opposite : IsIdempotentComplete Cᵒᵖ ↔ IsIdempotentComplete C

Proof state:
case mpr.h
C : Type u_1
inst✝ : Category.{u_2, u_1} C
h : IsIdempotentComplete C
⊢ IsIdempotentComplete Cᵒᵖᵒᵖ

Tactic:
rw [isIdempotentComplete_iff_of_equivalence (opOpEquivalence C)]

Result:
case mpr.h
C : Type u_1
inst✝ : Category.{u_2, u_1} C
h : IsIdempotentComplete C
⊢ IsIdempotentComplete C

Proof state:
case mpr
C : Type u_1
inst✝ : Category.{u_2, u_1} C
h : IsIdempotentComplete C
⊢ IsIdempotentComplete Cᵒᵖ

Tactic:
apply isIdempotentComplete_of_isIdempotentComplete_opposite

Result:
case mpr.h
C : Type u_1
inst✝ : Category.{u_2, u_1} C
h : IsIdempotentComplete C
⊢ IsIdempotentComplete Cᵒᵖᵒᵖ

Proof state:
C : Type u_1
inst✝ : Category.{u_2, u_1} C
⊢ IsIdempotentComplete Cᵒᵖ ↔ IsIdempotentComplete C

Tactic:
constructor

Result:
case mp
C : Type u_1
inst✝ : Category.{u_2, u_1} C
⊢ IsIdempotentComplete Cᵒᵖ → IsIdempotentComplete C

case mpr
C : Type u_1
inst✝ : Category.{u_2, u_1} C
⊢ IsIdempotentComplete C → IsIdempotentComplete Cᵒᵖ

Proof state:
case mpr
C : Type u_1
inst✝ : Category.{u_2, u_1} C
⊢ IsIdempotentComplete C → IsIdempotentComplete Cᵒᵖ

Tactic:
intro h

Result:
case mpr
C : Type u_1
inst✝ : Category.{u_2, u_1} C
h : IsIdempotentComplete C
⊢ IsIdempotentComplete Cᵒᵖ

Proof state:
case mpr.h
C : Type u_1
inst✝ : Category.{u_2, u_1} C
h : IsIdempotentComplete C
⊢ IsIdempotentComplete C

Tactic:
exact h

Result:
no goals

Proof state:
case mp
C : Type u_1
inst✝ : Category.{u_2, u_1} C
⊢ IsIdempotentComplete Cᵒᵖ → IsIdempotentComplete C

Tactic:
exact isIdempotentComplete_of_isIdempotentComplete_opposite

Result:
no goals
-- Mathlib/LinearAlgebra/DFinsupp.lean
theorem lsum_comp_mapRange_toSpanSingleton [∀ m : R, Decidable (m ≠ 0)] (p : ι → Submodule R N)
    {v : ι → N} (hv : ∀ i : ι, v i ∈ p i) :
    (lsum ℕ (M := fun i ↦ ↥(p i)) fun i => (p i).subtype : _ →ₗ[R] _).comp
        ((mapRange.linearMap fun i => LinearMap.toSpanSingleton R (↥(p i)) ⟨v i, hv i⟩ :
              _ →ₗ[R] _).comp
          (finsuppLequivDFinsupp R : (ι →₀ R) ≃ₗ[R] _).toLinearMap) =
      Finsupp.linearCombination R v

Proof state:
ι : Type u_1
R : Type u_2
N : Type u_5
inst✝⁴ : DecidableEq ι
inst✝³ : Semiring R
inst✝² : AddCommMonoid N
inst✝¹ : Module R N
inst✝ : (m : R) → Decidable (m ≠ 0)
p : ι → Submodule R N
v : ι → N
hv : ∀ (i : ι), v i ∈ p i
⊢ ((lsum ℕ) fun i => (p i).subtype) ∘ₗ
      (mapRange.linearMap fun i => LinearMap.toSpanSingleton R ↥(p i) ⟨v i, ⋯⟩) ∘ₗ ↑(finsuppLequivDFinsupp R) =
    Finsupp.linearCombination R v

Tactic:
ext

Result:
case h.h
ι : Type u_1
R : Type u_2
N : Type u_5
inst✝⁴ : DecidableEq ι
inst✝³ : Semiring R
inst✝² : AddCommMonoid N
inst✝¹ : Module R N
inst✝ : (m : R) → Decidable (m ≠ 0)
p : ι → Submodule R N
v : ι → N
hv : ∀ (i : ι), v i ∈ p i
a✝ : ι
⊢ ((((lsum ℕ) fun i => (p i).subtype) ∘ₗ
          (mapRange.linearMap fun i => LinearMap.toSpanSingleton R ↥(p i) ⟨v i, ⋯⟩) ∘ₗ ↑(finsuppLequivDFinsupp R)) ∘ₗ
        Finsupp.lsingle a✝)
      1 =
    (Finsupp.linearCombination R v ∘ₗ Finsupp.lsingle a✝) 1

Proof state:
case h.h
ι : Type u_1
R : Type u_2
N : Type u_5
inst✝⁴ : DecidableEq ι
inst✝³ : Semiring R
inst✝² : AddCommMonoid N
inst✝¹ : Module R N
inst✝ : (m : R) → Decidable (m ≠ 0)
p : ι → Submodule R N
v : ι → N
hv : ∀ (i : ι), v i ∈ p i
a✝ : ι
⊢ ((((lsum ℕ) fun i => (p i).subtype) ∘ₗ
          (mapRange.linearMap fun i => LinearMap.toSpanSingleton R ↥(p i) ⟨v i, ⋯⟩) ∘ₗ ↑(finsuppLequivDFinsupp R)) ∘ₗ
        Finsupp.lsingle a✝)
      1 =
    (Finsupp.linearCombination R v ∘ₗ Finsupp.lsingle a✝) 1

Tactic:
simp

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/List/Nat/Range.lean
theorem mk_mem_zipIdx_iff_le_and_getElem?_sub {k i : Nat} {x : α} {l : List α} :
    (x, i) ∈ zipIdx l k ↔ k ≤ i ∧ l[i - k]? = some x

Proof state:
α : Type u_1
k : Nat
x : α
l : List α
m✝ : Nat
h : ¬k ≤ k + m✝
⊢ False

Tactic:
simp at h

Result:
no goals

Proof state:
α : Type u_1
k i : Nat
x : α
l : List α
h : ¬k ≤ i
⊢ (x, i) ∈ l.zipIdx k ↔ k ≤ i ∧ l[i - k]? = some x

Tactic:
have : ∀ m, k + m ≠ i := by rintro _ rfl; simp at h

Result:
α : Type u_1
k i : Nat
x : α
l : List α
h : ¬k ≤ i
this : ∀ (m : Nat), k + m ≠ i
⊢ (x, i) ∈ l.zipIdx k ↔ k ≤ i ∧ l[i - k]? = some x

Proof state:
α : Type u_1
k i : Nat
x : α
l : List α
h : ¬k ≤ i
this : ∀ (m : Nat), k + m ≠ i
⊢ (x, i) ∈ l.zipIdx k ↔ k ≤ i ∧ l[i - k]? = some x

Tactic:
simp [h, mem_iff_get?, this]

Result:
no goals

Proof state:
α : Type u_1
k i : Nat
x : α
l : List α
⊢ (x, i) ∈ l.zipIdx k ↔ k ≤ i ∧ l[i - k]? = some x

Tactic:
if h : k ≤ i then
  rcases Nat.exists_eq_add_of_le h with ⟨i, rfl⟩
  simp [mk_add_mem_zipIdx_iff_getElem?, Nat.add_sub_cancel_left]
else
  have : ∀ m, k + m ≠ i := by rintro _ rfl; simp at h
  simp [h, mem_iff_get?, this]

Result:
no goals

Proof state:
case intro
α : Type u_1
k : Nat
x : α
l : List α
i : Nat
h : k ≤ k + i
⊢ (x, k + i) ∈ l.zipIdx k ↔ k ≤ k + i ∧ l[k + i - k]? = some x

Tactic:
simp [mk_add_mem_zipIdx_iff_getElem?, Nat.add_sub_cancel_left]

Result:
no goals

Proof state:
α : Type u_1
k i : Nat
x : α
l : List α
h : ¬k ≤ i
⊢ ∀ (m : Nat), k + m ≠ i

Tactic:
rintro _ rfl

Result:
α : Type u_1
k : Nat
x : α
l : List α
m✝ : Nat
h : ¬k ≤ k + m✝
⊢ False

Proof state:
α : Type u_1
k i : Nat
x : α
l : List α
h : k ≤ i
⊢ (x, i) ∈ l.zipIdx k ↔ k ≤ i ∧ l[i - k]? = some x

Tactic:
rcases Nat.exists_eq_add_of_le h with ⟨i, rfl⟩

Result:
case intro
α : Type u_1
k : Nat
x : α
l : List α
i : Nat
h : k ≤ k + i
⊢ (x, k + i) ∈ l.zipIdx k ↔ k ≤ k + i ∧ l[k + i - k]? = some x
-- Mathlib/AlgebraicGeometry/IdealSheaf.lean
lemma map_ideal {U V : X.affineOpens} (h : U ≤ V) :
    (I.ideal V).map (X.presheaf.map (homOfLE h).op).hom = I.ideal U

Proof state:
case intro.intro.intro
X : Scheme
I : X.IdealSheafData
U V : ↑X.affineOpens
h : U ≤ V
x : ↑↑X.toPresheafedSpace
hxU : x ∈ ↑U
f : ↑Γ(X, ↑U)
g : ↑Γ(X, ↑V)
hfg : X.basicOpen f = X.basicOpen g
hxf : x ∈ X.basicOpen f
this :
  Ideal.map (CommRingCat.Hom.hom (X.presheaf.map (homOfLE ⋯).op)) (I.ideal U) =
    Ideal.map (CommRingCat.Hom.hom (X.presheaf.map (homOfLE ⋯).op)) (I.ideal V)
⊢ Ideal.map (CommRingCat.Hom.hom (X.presheaf.germ (↑U) x hxU))
      (Ideal.map (CommRingCat.Hom.hom (X.presheaf.map (homOfLE h).op)) (I.ideal V)) =
    Ideal.map (CommRingCat.Hom.hom (X.presheaf.germ (↑U) x hxU)) (I.ideal U)

Tactic:
apply_fun Ideal.map (X.presheaf.germ (X.basicOpen g) x (hfg ▸ hxf)).hom at this

Result:
case intro.intro.intro
X : Scheme
I : X.IdealSheafData
U V : ↑X.affineOpens
h : U ≤ V
x : ↑↑X.toPresheafedSpace
hxU : x ∈ ↑U
f : ↑Γ(X, ↑U)
g : ↑Γ(X, ↑V)
hfg : X.basicOpen f = X.basicOpen g
hxf : x ∈ X.basicOpen f
this :
  Ideal.map (CommRingCat.Hom.hom (X.presheaf.germ (X.basicOpen g) x ⋯))
      (Ideal.map (CommRingCat.Hom.hom (X.presheaf.map (homOfLE ⋯).op)) (I.ideal U)) =
    Ideal.map (CommRingCat.Hom.hom (X.presheaf.germ (X.basicOpen g) x ⋯))
      (Ideal.map (CommRingCat.Hom.hom (X.presheaf.map (homOfLE ⋯).op)) (I.ideal V))
⊢ Ideal.map (CommRingCat.Hom.hom (X.presheaf.germ (↑U) x hxU))
      (Ideal.map (CommRingCat.Hom.hom (X.presheaf.map (homOfLE h).op)) (I.ideal V)) =
    Ideal.map (CommRingCat.Hom.hom (X.presheaf.germ (↑U) x hxU)) (I.ideal U)