harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/Topology/Category/Profinite/Nobeling.lean
theorem one_sub_e_mem_of_false {x y : (π C (· ∈ s))} {a : I} (ha : y.val a = true)
    (hx : x.val a = false) : 1 - e (π C (· ∈ s)) a ∈ factors C s x

Proof state:
case h.mk.intro.intro
I : Type u
C : Set (I → Bool)
inst✝ : LinearOrder I
s : Finset I
x : ↑(π C fun x => x ∈ s)
a : I
hx : ↑x a = false
z : I → Bool
hz : z ∈ C
ha : ↑⟨Proj (fun x => x ∈ s) z, ⋯⟩ a = true
⊢ a ∈ s ∧
    (if false = true then e (π C fun x => x ∈ s) a else 1 - e (π C fun x => x ∈ s) a) = 1 - e (π C fun x => x ∈ s) a

Tactic:
aesop (add simp Proj)

Result:
no goals

Proof state:
case h
I : Type u
C : Set (I → Bool)
inst✝ : LinearOrder I
s : Finset I
x y : ↑(π C fun x => x ∈ s)
a : I
ha : ↑y a = true
hx : ↑x a = false
⊢ a ∈ s ∧
    (if ↑x a = true then e (π C fun x => x ∈ s) a else 1 - e (π C fun x => x ∈ s) a) = 1 - e (π C fun x => x ∈ s) a

Tactic:
simp only [hx, ite_false, and_true]

Result:
case h
I : Type u
C : Set (I → Bool)
inst✝ : LinearOrder I
s : Finset I
x y : ↑(π C fun x => x ∈ s)
a : I
ha : ↑y a = true
hx : ↑x a = false
⊢ a ∈ s ∧
    (if false = true then e (π C fun x => x ∈ s) a else 1 - e (π C fun x => x ∈ s) a) = 1 - e (π C fun x => x ∈ s) a

Proof state:
I : Type u
C : Set (I → Bool)
inst✝ : LinearOrder I
s : Finset I
x y : ↑(π C fun x => x ∈ s)
a : I
ha : ↑y a = true
hx : ↑x a = false
⊢ 1 - e (π C fun x => x ∈ s) a ∈ factors C s x

Tactic:
simp only [factors, List.mem_map, Finset.mem_sort]

Result:
I : Type u
C : Set (I → Bool)
inst✝ : LinearOrder I
s : Finset I
x y : ↑(π C fun x => x ∈ s)
a : I
ha : ↑y a = true
hx : ↑x a = false
⊢ ∃ a_1 ∈ s,
    (if ↑x a_1 = true then e (π C fun x => x ∈ s) a_1 else 1 - e (π C fun x => x ∈ s) a_1) =
      1 - e (π C fun x => x ∈ s) a

Proof state:
case h
I : Type u
C : Set (I → Bool)
inst✝ : LinearOrder I
s : Finset I
x y : ↑(π C fun x => x ∈ s)
a : I
ha : ↑y a = true
hx : ↑x a = false
⊢ a ∈ s ∧
    (if false = true then e (π C fun x => x ∈ s) a else 1 - e (π C fun x => x ∈ s) a) = 1 - e (π C fun x => x ∈ s) a

Tactic:
rcases y with ⟨_, z, hz, rfl⟩

Result:
case h.mk.intro.intro
I : Type u
C : Set (I → Bool)
inst✝ : LinearOrder I
s : Finset I
x : ↑(π C fun x => x ∈ s)
a : I
hx : ↑x a = false
z : I → Bool
hz : z ∈ C
ha : ↑⟨Proj (fun x => x ∈ s) z, ⋯⟩ a = true
⊢ a ∈ s ∧
    (if false = true then e (π C fun x => x ∈ s) a else 1 - e (π C fun x => x ∈ s) a) = 1 - e (π C fun x => x ∈ s) a

Proof state:
I : Type u
C : Set (I → Bool)
inst✝ : LinearOrder I
s : Finset I
x y : ↑(π C fun x => x ∈ s)
a : I
ha : ↑y a = true
hx : ↑x a = false
⊢ ∃ a_1 ∈ s,
    (if ↑x a_1 = true then e (π C fun x => x ∈ s) a_1 else 1 - e (π C fun x => x ∈ s) a_1) =
      1 - e (π C fun x => x ∈ s) a

Tactic:
use a

Result:
case h
I : Type u
C : Set (I → Bool)
inst✝ : LinearOrder I
s : Finset I
x y : ↑(π C fun x => x ∈ s)
a : I
ha : ↑y a = true
hx : ↑x a = false
⊢ a ∈ s ∧
    (if ↑x a = true then e (π C fun x => x ∈ s) a else 1 - e (π C fun x => x ∈ s) a) = 1 - e (π C fun x => x ∈ s) a
-- Mathlib/Analysis/Convex/Basic.lean
theorem Convex.add_smul_sub_mem (h : Convex 𝕜 s) {x y : E} (hx : x ∈ s) (hy : y ∈ s) {t : 𝕜}
    (ht : t ∈ Icc (0 : 𝕜) 1) : x + t • (y - x) ∈ s

Proof state:
𝕜 : Type u_1
E : Type u_2
inst✝² : OrderedRing 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
s : Set E
h : Convex 𝕜 s
x y : E
hx : x ∈ s
hy : y ∈ s
t : 𝕜
ht : t ∈ Icc 0 1
⊢ t • (y - x) + x ∈ s

Tactic:
exact h.lineMap_mem hx hy ht

Result:
no goals

Proof state:
𝕜 : Type u_1
E : Type u_2
inst✝² : OrderedRing 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
s : Set E
h : Convex 𝕜 s
x y : E
hx : x ∈ s
hy : y ∈ s
t : 𝕜
ht : t ∈ Icc 0 1
⊢ x + t • (y - x) ∈ s

Tactic:
rw [add_comm]

Result:
𝕜 : Type u_1
E : Type u_2
inst✝² : OrderedRing 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
s : Set E
h : Convex 𝕜 s
x y : E
hx : x ∈ s
hy : y ∈ s
t : 𝕜
ht : t ∈ Icc 0 1
⊢ t • (y - x) + x ∈ s
-- Mathlib/Geometry/Euclidean/Angle/Unoriented/Basic.lean
theorem angle_eq_zero_iff {x y : V} : angle x y = 0 ↔ x ≠ 0 ∧ ∃ r : ℝ, 0 < r ∧ y = r • x

Proof state:
V : Type u_1
inst✝¹ : NormedAddCommGroup V
inst✝ : InnerProductSpace ℝ V
x y : V
⊢ inner x y / (‖x‖ * ‖y‖) ≤ 1

Tactic:
exact (abs_le.mp (abs_real_inner_div_norm_mul_norm_le_one x y)).2

Result:
no goals

Proof state:
V : Type u_1
inst✝¹ : NormedAddCommGroup V
inst✝ : InnerProductSpace ℝ V
x y : V
⊢ angle x y = 0 ↔ x ≠ 0 ∧ ∃ r, 0 < r ∧ y = r • x

Tactic:
rw [angle, ← real_inner_div_norm_mul_norm_eq_one_iff, Real.arccos_eq_zero, LE.le.le_iff_eq,
  eq_comm]

Result:
V : Type u_1
inst✝¹ : NormedAddCommGroup V
inst✝ : InnerProductSpace ℝ V
x y : V
⊢ inner x y / (‖x‖ * ‖y‖) ≤ 1
-- Mathlib/Data/Num/Lemmas.lean
theorem mul_to_int : ∀ m n, ((m * n : ZNum) : ℤ) = m * n
  | 0, a => by cases a <;> exact (zero_mul _).symm
  | b, 0 => by cases b <;> exact (mul_zero _).symm
  | pos a, pos b => PosNum.cast_mul a b
  | pos a, neg b => show -↑(a * b) = ↑a * -↑b by rw [PosNum.cast_mul, neg_mul_eq_mul_neg]
  | neg a, pos b => show -↑(a * b) = -↑a * ↑b by rw [PosNum.cast_mul, neg_mul_eq_neg_mul]
  | neg a, neg b => show ↑(a * b) = -↑a * -↑b by rw [PosNum.cast_mul, neg_mul_neg]

Proof state:
a : ZNum
⊢ ↑(0 * a) = ↑0 * ↑a

Tactic:
cases a <;> exact (zero_mul _).symm

Result:
no goals

Proof state:
a b : PosNum
⊢ ↑(a * b) = -↑a * -↑b

Tactic:
rw [PosNum.cast_mul, neg_mul_neg]

Result:
no goals

Proof state:
a b : PosNum
⊢ -↑(a * b) = -↑a * ↑b

Tactic:
rw [PosNum.cast_mul, neg_mul_eq_neg_mul]

Result:
no goals

Proof state:
a b : PosNum
⊢ -↑(a * b) = ↑a * -↑b

Tactic:
rw [PosNum.cast_mul, neg_mul_eq_mul_neg]

Result:
no goals

Proof state:
b : ZNum
⊢ ↑(b * 0) = ↑b * ↑0

Tactic:
cases b <;> exact (mul_zero _).symm

Result:
no goals
-- Mathlib/Algebra/BigOperators/Group/Multiset/Basic.lean
theorem sum_map_tsub [AddCommMonoid α] [PartialOrder α] [ExistsAddOfLE α]
    [CovariantClass α α (· + ·) (· ≤ ·)] [ContravariantClass α α (· + ·) (· ≤ ·)] [Sub α]
    [OrderedSub α] (l : Multiset ι) {f g : ι → α} (hfg : ∀ x ∈ l, g x ≤ f x) :
    (l.map fun x ↦ f x - g x).sum = (l.map f).sum - (l.map g).sum :=
  eq_tsub_of_add_eq <| by
    rw [← sum_map_add]
    congr 1
    exact map_congr rfl fun x hx => tsub_add_cancel_of_le <| hfg _ hx

Proof state:
ι : Type u_2
α : Type u_3
inst✝⁶ : AddCommMonoid α
inst✝⁵ : PartialOrder α
inst✝⁴ : ExistsAddOfLE α
inst✝³ : CovariantClass α α (fun x1 x2 => x1 + x2) fun x1 x2 => x1 ≤ x2
inst✝² : ContravariantClass α α (fun x1 x2 => x1 + x2) fun x1 x2 => x1 ≤ x2
inst✝¹ : Sub α
inst✝ : OrderedSub α
l : Multiset ι
f g : ι → α
hfg : ∀ x ∈ l, g x ≤ f x
⊢ (map (fun i => f i - g i + g i) l).sum = (map f l).sum

Tactic:
congr 1

Result:
case e_a
ι : Type u_2
α : Type u_3
inst✝⁶ : AddCommMonoid α
inst✝⁵ : PartialOrder α
inst✝⁴ : ExistsAddOfLE α
inst✝³ : CovariantClass α α (fun x1 x2 => x1 + x2) fun x1 x2 => x1 ≤ x2
inst✝² : ContravariantClass α α (fun x1 x2 => x1 + x2) fun x1 x2 => x1 ≤ x2
inst✝¹ : Sub α
inst✝ : OrderedSub α
l : Multiset ι
f g : ι → α
hfg : ∀ x ∈ l, g x ≤ f x
⊢ map (fun i => f i - g i + g i) l = map f l

Proof state:
case e_a
ι : Type u_2
α : Type u_3
inst✝⁶ : AddCommMonoid α
inst✝⁵ : PartialOrder α
inst✝⁴ : ExistsAddOfLE α
inst✝³ : CovariantClass α α (fun x1 x2 => x1 + x2) fun x1 x2 => x1 ≤ x2
inst✝² : ContravariantClass α α (fun x1 x2 => x1 + x2) fun x1 x2 => x1 ≤ x2
inst✝¹ : Sub α
inst✝ : OrderedSub α
l : Multiset ι
f g : ι → α
hfg : ∀ x ∈ l, g x ≤ f x
⊢ map (fun i => f i - g i + g i) l = map f l

Tactic:
exact map_congr rfl fun x hx => tsub_add_cancel_of_le <| hfg _ hx

Result:
no goals

Proof state:
ι : Type u_2
α : Type u_3
inst✝⁶ : AddCommMonoid α
inst✝⁵ : PartialOrder α
inst✝⁴ : ExistsAddOfLE α
inst✝³ : CovariantClass α α (fun x1 x2 => x1 + x2) fun x1 x2 => x1 ≤ x2
inst✝² : ContravariantClass α α (fun x1 x2 => x1 + x2) fun x1 x2 => x1 ≤ x2
inst✝¹ : Sub α
inst✝ : OrderedSub α
l : Multiset ι
f g : ι → α
hfg : ∀ x ∈ l, g x ≤ f x
⊢ (map (fun x => f x - g x) l).sum + (map g l).sum = (map f l).sum

Tactic:
rw [← sum_map_add]

Result:
ι : Type u_2
α : Type u_3
inst✝⁶ : AddCommMonoid α
inst✝⁵ : PartialOrder α
inst✝⁴ : ExistsAddOfLE α
inst✝³ : CovariantClass α α (fun x1 x2 => x1 + x2) fun x1 x2 => x1 ≤ x2
inst✝² : ContravariantClass α α (fun x1 x2 => x1 + x2) fun x1 x2 => x1 ≤ x2
inst✝¹ : Sub α
inst✝ : OrderedSub α
l : Multiset ι
f g : ι → α
hfg : ∀ x ∈ l, g x ≤ f x
⊢ (map (fun i => f i - g i + g i) l).sum = (map f l).sum
-- Mathlib/Combinatorics/SimpleGraph/DegreeSum.lean
theorem dart_card_eq_twice_card_edges : Fintype.card G.Dart = 2 * #G.edgeFinset

Proof state:
V : Type u
G : SimpleGraph V
inst✝¹ : Fintype V
inst✝ : DecidableRel G.Adj
⊢ Fintype.card G.Dart = 2 * #G.edgeFinset

Tactic:
classical
rw [← card_univ]
rw [@card_eq_sum_card_fiberwise _ _ _ Dart.edge _ G.edgeFinset fun d _h =>
    by rw [mem_edgeFinset]; apply Dart.edge_mem]
rw [← mul_comm, sum_const_nat]
intro e h
apply G.dart_edge_fiber_card e
rwa [← mem_edgeFinset]

Result:
no goals

Proof state:
V : Type u
G : SimpleGraph V
inst✝¹ : Fintype V
inst✝ : DecidableRel G.Adj
⊢ ∀ x ∈ G.edgeFinset, #(filter (fun a => a.edge = x) univ) = 2

Tactic:
intro e h

Result:
V : Type u
G : SimpleGraph V
inst✝¹ : Fintype V
inst✝ : DecidableRel G.Adj
e : Sym2 V
h : e ∈ G.edgeFinset
⊢ #(filter (fun a => a.edge = e) univ) = 2

Proof state:
V : Type u
G : SimpleGraph V
inst✝¹ : Fintype V
inst✝ : DecidableRel G.Adj
d : G.Dart
_h : d ∈ univ
⊢ d.edge ∈ G.edgeFinset

Tactic:
rw [mem_edgeFinset]

Result:
V : Type u
G : SimpleGraph V
inst✝¹ : Fintype V
inst✝ : DecidableRel G.Adj
d : G.Dart
_h : d ∈ univ
⊢ d.edge ∈ G.edgeSet

Proof state:
V : Type u
G : SimpleGraph V
inst✝¹ : Fintype V
inst✝ : DecidableRel G.Adj
⊢ Fintype.card G.Dart = 2 * #G.edgeFinset

Tactic:
rw [← card_univ]

Result:
V : Type u
G : SimpleGraph V
inst✝¹ : Fintype V
inst✝ : DecidableRel G.Adj
⊢ #univ = 2 * #G.edgeFinset

Proof state:
V : Type u
G : SimpleGraph V
inst✝¹ : Fintype V
inst✝ : DecidableRel G.Adj
⊢ ∑ b ∈ G.edgeFinset, #(filter (fun a => a.edge = b) univ) = 2 * #G.edgeFinset

Tactic:
rw [← mul_comm, sum_const_nat]

Result:
V : Type u
G : SimpleGraph V
inst✝¹ : Fintype V
inst✝ : DecidableRel G.Adj
⊢ ∀ x ∈ G.edgeFinset, #(filter (fun a => a.edge = x) univ) = 2

Proof state:
V : Type u
G : SimpleGraph V
inst✝¹ : Fintype V
inst✝ : DecidableRel G.Adj
e : Sym2 V
h : e ∈ G.edgeFinset
⊢ e ∈ G.edgeSet

Tactic:
rwa [← mem_edgeFinset]

Result:
no goals

Proof state:
V : Type u
G : SimpleGraph V
inst✝¹ : Fintype V
inst✝ : DecidableRel G.Adj
⊢ #univ = 2 * #G.edgeFinset

Tactic:
rw [@card_eq_sum_card_fiberwise _ _ _ Dart.edge _ G.edgeFinset fun d _h =>
    by rw [mem_edgeFinset]; apply Dart.edge_mem]

Result:
V : Type u
G : SimpleGraph V
inst✝¹ : Fintype V
inst✝ : DecidableRel G.Adj
⊢ ∑ b ∈ G.edgeFinset, #(filter (fun a => a.edge = b) univ) = 2 * #G.edgeFinset

Proof state:
V : Type u
G : SimpleGraph V
inst✝¹ : Fintype V
inst✝ : DecidableRel G.Adj
d : G.Dart
_h : d ∈ univ
⊢ d.edge ∈ G.edgeSet

Tactic:
apply Dart.edge_mem

Result:
no goals

Proof state:
V : Type u
G : SimpleGraph V
inst✝¹ : Fintype V
inst✝ : DecidableRel G.Adj
e : Sym2 V
h : e ∈ G.edgeFinset
⊢ #(filter (fun a => a.edge = e) univ) = 2

Tactic:
apply G.dart_edge_fiber_card e

Result:
V : Type u
G : SimpleGraph V
inst✝¹ : Fintype V
inst✝ : DecidableRel G.Adj
e : Sym2 V
h : e ∈ G.edgeFinset
⊢ e ∈ G.edgeSet
-- Mathlib/Algebra/Homology/ShortComplex/QuasiIso.lean
lemma quasiIso_iff (φ : S₁ ⟶ S₂) :
    QuasiIso φ ↔ IsIso (homologyMap φ)

Proof state:
case mp
C : Type u_2
inst✝³ : Category.{u_1, u_2} C
inst✝² : HasZeroMorphisms C
S₁ S₂ : ShortComplex C
inst✝¹ : S₁.HasHomology
inst✝ : S₂.HasHomology
φ : S₁ ⟶ S₂
h : QuasiIso φ
⊢ IsIso (homologyMap φ)

Tactic:
infer_instance

Result:
no goals

Proof state:
case mpr
C : Type u_2
inst✝³ : Category.{u_1, u_2} C
inst✝² : HasZeroMorphisms C
S₁ S₂ : ShortComplex C
inst✝¹ : S₁.HasHomology
inst✝ : S₂.HasHomology
φ : S₁ ⟶ S₂
h : IsIso (homologyMap φ)
⊢ QuasiIso φ

Tactic:
exact ⟨h⟩

Result:
no goals

Proof state:
C : Type u_2
inst✝³ : Category.{u_1, u_2} C
inst✝² : HasZeroMorphisms C
S₁ S₂ : ShortComplex C
inst✝¹ : S₁.HasHomology
inst✝ : S₂.HasHomology
φ : S₁ ⟶ S₂
⊢ QuasiIso φ ↔ IsIso (homologyMap φ)

Tactic:
constructor

Result:
case mp
C : Type u_2
inst✝³ : Category.{u_1, u_2} C
inst✝² : HasZeroMorphisms C
S₁ S₂ : ShortComplex C
inst✝¹ : S₁.HasHomology
inst✝ : S₂.HasHomology
φ : S₁ ⟶ S₂
⊢ QuasiIso φ → IsIso (homologyMap φ)

case mpr
C : Type u_2
inst✝³ : Category.{u_1, u_2} C
inst✝² : HasZeroMorphisms C
S₁ S₂ : ShortComplex C
inst✝¹ : S₁.HasHomology
inst✝ : S₂.HasHomology
φ : S₁ ⟶ S₂
⊢ IsIso (homologyMap φ) → QuasiIso φ

Proof state:
case mpr
C : Type u_2
inst✝³ : Category.{u_1, u_2} C
inst✝² : HasZeroMorphisms C
S₁ S₂ : ShortComplex C
inst✝¹ : S₁.HasHomology
inst✝ : S₂.HasHomology
φ : S₁ ⟶ S₂
⊢ IsIso (homologyMap φ) → QuasiIso φ

Tactic:
intro h

Result:
case mpr
C : Type u_2
inst✝³ : Category.{u_1, u_2} C
inst✝² : HasZeroMorphisms C
S₁ S₂ : ShortComplex C
inst✝¹ : S₁.HasHomology
inst✝ : S₂.HasHomology
φ : S₁ ⟶ S₂
h : IsIso (homologyMap φ)
⊢ QuasiIso φ

Proof state:
case mp
C : Type u_2
inst✝³ : Category.{u_1, u_2} C
inst✝² : HasZeroMorphisms C
S₁ S₂ : ShortComplex C
inst✝¹ : S₁.HasHomology
inst✝ : S₂.HasHomology
φ : S₁ ⟶ S₂
⊢ QuasiIso φ → IsIso (homologyMap φ)

Tactic:
intro h

Result:
case mp
C : Type u_2
inst✝³ : Category.{u_1, u_2} C
inst✝² : HasZeroMorphisms C
S₁ S₂ : ShortComplex C
inst✝¹ : S₁.HasHomology
inst✝ : S₂.HasHomology
φ : S₁ ⟶ S₂
h : QuasiIso φ
⊢ IsIso (homologyMap φ)
-- Mathlib/AlgebraicTopology/SimplexCategory/Basic.lean
lemma const_subinterval_eq {n} (j l : ℕ) (hjl : j + l ≤ n) (i : Fin (l + 1)) :
    ⦋0⦌.const ⦋l⦌ i ≫ subinterval j l hjl =
    ⦋0⦌.const ⦋n⦌ ⟨j + i.1, lt_add_of_lt_add_right (Nat.add_lt_add_left i.2 j) hjl⟩

Proof state:
case e_i.h
n j l : ℕ
hjl : j + l ≤ n
i : Fin (l + 1)
⊢ ↑((Hom.toOrderHom (subinterval j l hjl)) i) = ↑⟨j + ↑i, ⋯⟩

Tactic:
dsimp [subinterval]

Result:
case e_i.h
n j l : ℕ
hjl : j + l ≤ n
i : Fin (l + 1)
⊢ ↑i + j = j + ↑i

Proof state:
n j l : ℕ
hjl : j + l ≤ n
i : Fin (l + 1)
⊢ ⦋0⦌.const ⦋n⦌ ((Hom.toOrderHom (subinterval j l hjl)) i) = ⦋0⦌.const ⦋n⦌ ⟨j + ↑i, ⋯⟩

Tactic:
congr

Result:
case e_i
n j l : ℕ
hjl : j + l ≤ n
i : Fin (l + 1)
⊢ (Hom.toOrderHom (subinterval j l hjl)) i = ⟨j + ↑i, ⋯⟩

Proof state:
n j l : ℕ
hjl : j + l ≤ n
i : Fin (l + 1)
⊢ ⦋0⦌.const ⦋l⦌ i ≫ subinterval j l hjl = ⦋0⦌.const ⦋n⦌ ⟨j + ↑i, ⋯⟩

Tactic:
rw [const_comp]

Result:
n j l : ℕ
hjl : j + l ≤ n
i : Fin (l + 1)
⊢ ⦋0⦌.const ⦋n⦌ ((Hom.toOrderHom (subinterval j l hjl)) i) = ⦋0⦌.const ⦋n⦌ ⟨j + ↑i, ⋯⟩

Proof state:
case e_i
n j l : ℕ
hjl : j + l ≤ n
i : Fin (l + 1)
⊢ (Hom.toOrderHom (subinterval j l hjl)) i = ⟨j + ↑i, ⋯⟩

Tactic:
ext

Result:
case e_i.h
n j l : ℕ
hjl : j + l ≤ n
i : Fin (l + 1)
⊢ ↑((Hom.toOrderHom (subinterval j l hjl)) i) = ↑⟨j + ↑i, ⋯⟩

Proof state:
case e_i.h
n j l : ℕ
hjl : j + l ≤ n
i : Fin (l + 1)
⊢ ↑i + j = j + ↑i

Tactic:
rw [add_comm]

Result:
no goals
-- Mathlib/Order/SymmDiff.lean
theorem sup_himp_bihimp : a ⊔ b ⇨ a ⇔ b = a ⇔ b

Proof state:
α : Type u_2
inst✝ : GeneralizedHeytingAlgebra α
a b : α
⊢ ((a ⊔ b) ⊓ b ⇨ a) ⊓ ((a ⊔ b) ⊓ a ⇨ b) = a ⇔ b

Tactic:
simp [bihimp]

Result:
no goals

Proof state:
α : Type u_2
inst✝ : GeneralizedHeytingAlgebra α
a b : α
⊢ a ⊔ b ⇨ a ⇔ b = a ⇔ b

Tactic:
rw [himp_bihimp]

Result:
α : Type u_2
inst✝ : GeneralizedHeytingAlgebra α
a b : α
⊢ ((a ⊔ b) ⊓ b ⇨ a) ⊓ ((a ⊔ b) ⊓ a ⇨ b) = a ⇔ b
-- Mathlib/Analysis/Convex/Radon.lean
theorem helly_theorem_set_compact' [TopologicalSpace E] [T2Space E] {F : Set (Set E)}
    (h_convex : ∀ X ∈ F, Convex 𝕜 X) (h_compact : ∀ X ∈ F, IsCompact X)
    (h_inter : ∀ G : Finset (Set E), (G : Set (Set E)) ⊆ F → #G ≤ finrank 𝕜 E + 1 →
    (⋂₀ G : Set E).Nonempty) :
    (⋂₀ (F : Set (Set E))).Nonempty

Proof state:
𝕜 : Type u_2
E : Type u_3
inst✝⁵ : LinearOrderedField 𝕜
inst✝⁴ : AddCommGroup E
inst✝³ : Module 𝕜 E
inst✝² : FiniteDimensional 𝕜 E
inst✝¹ : TopologicalSpace E
inst✝ : T2Space E
F : Set (Set E)
h_convex : ∀ X ∈ F, Convex 𝕜 X
h_compact : ∀ X ∈ F, IsCompact X
h_inter : ∀ (G : Finset (Set E)), ↑G ⊆ F → #G ≤ finrank 𝕜 E + 1 → (⋂₀ ↑G).Nonempty
⊢ (⋂ X, ↑X).Nonempty

Tactic:
refine helly_theorem_compact' (F := fun x : F ↦ x.val)
  (fun X ↦ h_convex X (by simp)) (fun X ↦ h_compact X (by simp)) ?_

Result:
𝕜 : Type u_2
E : Type u_3
inst✝⁵ : LinearOrderedField 𝕜
inst✝⁴ : AddCommGroup E
inst✝³ : Module 𝕜 E
inst✝² : FiniteDimensional 𝕜 E
inst✝¹ : TopologicalSpace E
inst✝ : T2Space E
F : Set (Set E)
h_convex : ∀ X ∈ F, Convex 𝕜 X
h_compact : ∀ X ∈ F, IsCompact X
h_inter : ∀ (G : Finset (Set E)), ↑G ⊆ F → #G ≤ finrank 𝕜 E + 1 → (⋂₀ ↑G).Nonempty
⊢ ∀ (I : Finset ↑F), #I ≤ finrank 𝕜 E + 1 → (⋂ i ∈ I, (fun x => ↑x) i).Nonempty

Proof state:
case a
𝕜 : Type u_2
E : Type u_3
inst✝⁵ : LinearOrderedField 𝕜
inst✝⁴ : AddCommGroup E
inst✝³ : Module 𝕜 E
inst✝² : FiniteDimensional 𝕜 E
inst✝¹ : TopologicalSpace E
inst✝ : T2Space E
F : Set (Set E)
h_convex : ∀ X ∈ F, Convex 𝕜 X
h_compact : ∀ X ∈ F, IsCompact X
h_inter : ∀ (G : Finset (Set E)), ↑G ⊆ F → #G ≤ finrank 𝕜 E + 1 → (⋂₀ ↑G).Nonempty
G : Finset ↑F
a✝ : #G ≤ finrank 𝕜 E + 1
G' : Finset (Set E) := Finset.image Subtype.val G
⊢ ↑G' ⊆ F

Tactic:
simp [G']

Result:
no goals

Proof state:
𝕜 : Type u_2
E : Type u_3
inst✝⁵ : LinearOrderedField 𝕜
inst✝⁴ : AddCommGroup E
inst✝³ : Module 𝕜 E
inst✝² : FiniteDimensional 𝕜 E
inst✝¹ : TopologicalSpace E
inst✝ : T2Space E
F : Set (Set E)
h_convex : ∀ X ∈ F, Convex 𝕜 X
h_compact : ∀ X ∈ F, IsCompact X
h_inter : ∀ (G : Finset (Set E)), ↑G ⊆ F → #G ≤ finrank 𝕜 E + 1 → (⋂₀ ↑G).Nonempty
X : ↑F
⊢ ↑X ∈ F

Tactic:
simp

Result:
no goals

Proof state:
case a
𝕜 : Type u_2
E : Type u_3
inst✝⁵ : LinearOrderedField 𝕜
inst✝⁴ : AddCommGroup E
inst✝³ : Module 𝕜 E
inst✝² : FiniteDimensional 𝕜 E
inst✝¹ : TopologicalSpace E
inst✝ : T2Space E
F : Set (Set E)
h_convex : ∀ X ∈ F, Convex 𝕜 X
h_compact : ∀ X ∈ F, IsCompact X
h_inter : ∀ (G : Finset (Set E)), ↑G ⊆ F → #G ≤ finrank 𝕜 E + 1 → (⋂₀ ↑G).Nonempty
G : Finset ↑F
a✝ : #G ≤ finrank 𝕜 E + 1
G' : Finset (Set E) := Finset.image Subtype.val G
⊢ #G' ≤ finrank 𝕜 E + 1

Tactic:
apply le_trans card_image_le

Result:
case a
𝕜 : Type u_2
E : Type u_3
inst✝⁵ : LinearOrderedField 𝕜
inst✝⁴ : AddCommGroup E
inst✝³ : Module 𝕜 E
inst✝² : FiniteDimensional 𝕜 E
inst✝¹ : TopologicalSpace E
inst✝ : T2Space E
F : Set (Set E)
h_convex : ∀ X ∈ F, Convex 𝕜 X
h_compact : ∀ X ∈ F, IsCompact X
h_inter : ∀ (G : Finset (Set E)), ↑G ⊆ F → #G ≤ finrank 𝕜 E + 1 → (⋂₀ ↑G).Nonempty
G : Finset ↑F
a✝ : #G ≤ finrank 𝕜 E + 1
G' : Finset (Set E) := Finset.image Subtype.val G
⊢ #G ≤ finrank 𝕜 E + 1
-- Mathlib/CategoryTheory/Closed/Monoidal.lean
/-- `curry'` and `uncurry`' are inverse bijections. -/
@[simp]
lemma curry'_uncurry' {X Y : C} [Closed X] (g : 𝟙_ C ⟶ (ihom X).obj Y) :
    curry' (uncurry' g) = g

Proof state:
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : MonoidalCategory C
X Y : C
inst✝ : Closed X
g : 𝟙_ C ⟶ (ihom X).obj Y
⊢ curry' (uncurry' g) = g

Tactic:
simp [curry', uncurry']

Result:
no goals
-- Mathlib/Data/Set/Card.lean
theorem two_lt_ncard (hs : s.Finite

Proof state:
α : Type u_1
s : Set α
hs : autoParam s.Finite _auto✝
⊢ 2 < s.ncard ↔ ∃ a ∈ s, ∃ b ∈ s, ∃ c ∈ s, a ≠ b ∧ a ≠ c ∧ b ≠ c

Tactic:
simp only [two_lt_ncard_iff hs, exists_and_left, exists_prop]

Result:
no goals
-- Mathlib/Order/Heyting/Basic.lean
theorem sdiff_inf_distrib (a b c : α) : a \ (b ⊓ c) = a \ b ⊔ a \ c :=
  eq_of_forall_ge_iff fun d => by
    rw [sup_le_iff, sdiff_le_comm, le_inf_iff]
    simp_rw [sdiff_le_comm]

Proof state:
α : Type u_2
inst✝ : GeneralizedCoheytingAlgebra α
a b c d : α
⊢ a \ (b ⊓ c) ≤ d ↔ a \ b ⊔ a \ c ≤ d

Tactic:
rw [sup_le_iff, sdiff_le_comm, le_inf_iff]

Result:
α : Type u_2
inst✝ : GeneralizedCoheytingAlgebra α
a b c d : α
⊢ a \ d ≤ b ∧ a \ d ≤ c ↔ a \ b ≤ d ∧ a \ c ≤ d

Proof state:
α : Type u_2
inst✝ : GeneralizedCoheytingAlgebra α
a b c d : α
⊢ a \ d ≤ b ∧ a \ d ≤ c ↔ a \ b ≤ d ∧ a \ c ≤ d

Tactic:
simp_rw [sdiff_le_comm]

Result:
no goals
-- Mathlib/LinearAlgebra/LinearDisjoint.lean
theorem of_linearDisjoint_fg_left
    (H : ∀ M' : Submodule R S, M' ≤ M → M'.FG → M'.LinearDisjoint N) :
    M.LinearDisjoint N := (linearDisjoint_iff _ _).2 fun x y hxy ↦ by
  obtain ⟨M', hM, hFG, h⟩ :=
    TensorProduct.exists_finite_submodule_left_of_finite' {x, y} (Set.toFinite _)
  rw [Module.Finite.iff_fg] at hFG
  obtain ⟨x', hx'⟩ := h (show x ∈ {x, y} by simp)
  obtain ⟨y', hy'⟩ := h (show y ∈ {x, y} by simp)
  rw [← hx', ← hy']; congr
  exact (H M' hM hFG).injective (by simp [← mulMap_comp_rTensor _ hM, hx', hy', hxy])

Proof state:
case intro.intro.intro.intro
R : Type u
S : Type v
inst✝² : CommSemiring R
inst✝¹ : Semiring S
inst✝ : Algebra R S
M N : Submodule R S
H : ∀ M' ≤ M, M'.FG → M'.LinearDisjoint N
x y : ↥M ⊗[R] ↥N
hxy : (M.mulMap N) x = (M.mulMap N) y
M' : Submodule R S
hM : M' ≤ M
hFG : M'.FG
h : {x, y} ⊆ ↑(LinearMap.range (LinearMap.rTensor (↥N) (inclusion hM)))
x' : ↥M' ⊗[R] ↥N
hx' : (LinearMap.rTensor (↥N) (inclusion hM)) x' = x
⊢ x = y

Tactic:
obtain ⟨y', hy'⟩ := h (show y ∈ {x, y} by simp)

Result:
case intro.intro.intro.intro.intro
R : Type u
S : Type v
inst✝² : CommSemiring R
inst✝¹ : Semiring S
inst✝ : Algebra R S
M N : Submodule R S
H : ∀ M' ≤ M, M'.FG → M'.LinearDisjoint N
x y : ↥M ⊗[R] ↥N
hxy : (M.mulMap N) x = (M.mulMap N) y
M' : Submodule R S
hM : M' ≤ M
hFG : M'.FG
h : {x, y} ⊆ ↑(LinearMap.range (LinearMap.rTensor (↥N) (inclusion hM)))
x' : ↥M' ⊗[R] ↥N
hx' : (LinearMap.rTensor (↥N) (inclusion hM)) x' = x
y' : ↥M' ⊗[R] ↥N
hy' : (LinearMap.rTensor (↥N) (inclusion hM)) y' = y
⊢ x = y
-- Mathlib/Algebra/MvPolynomial/PDeriv.lean
theorem pderiv_map {S} [CommSemiring S] {φ : R →+* S} {f : MvPolynomial σ R} {i : σ} :
    pderiv i (map φ f) = map φ (pderiv i f)

Proof state:
R : Type u
σ : Type v
inst✝¹ : CommSemiring R
S : Type u_1
inst✝ : CommSemiring S
φ : R →+* S
f : MvPolynomial σ R
i : σ
p : MvPolynomial σ R
j : σ
eq : (pderiv i) ((map φ) p) = (map φ) ((pderiv i) p)
⊢ (pderiv i) ((map φ) (p * X j)) = (map φ) ((pderiv i) (p * X j))

Tactic:
obtain rfl | h := eq_or_ne j i

Result:
case inl
R : Type u
σ : Type v
inst✝¹ : CommSemiring R
S : Type u_1
inst✝ : CommSemiring S
φ : R →+* S
f p : MvPolynomial σ R
j : σ
eq : (pderiv j) ((map φ) p) = (map φ) ((pderiv j) p)
⊢ (pderiv j) ((map φ) (p * X j)) = (map φ) ((pderiv j) (p * X j))

case inr
R : Type u
σ : Type v
inst✝¹ : CommSemiring R
S : Type u_1
inst✝ : CommSemiring S
φ : R →+* S
f : MvPolynomial σ R
i : σ
p : MvPolynomial σ R
j : σ
eq : (pderiv i) ((map φ) p) = (map φ) ((pderiv i) p)
h : j ≠ i
⊢ (pderiv i) ((map φ) (p * X j)) = (map φ) ((pderiv i) (p * X j))

Proof state:
case inl
R : Type u
σ : Type v
inst✝¹ : CommSemiring R
S : Type u_1
inst✝ : CommSemiring S
φ : R →+* S
f p : MvPolynomial σ R
j : σ
eq : (pderiv j) ((map φ) p) = (map φ) ((pderiv j) p)
⊢ (pderiv j) ((map φ) (p * X j)) = (map φ) ((pderiv j) (p * X j))

Tactic:
simp [eq]

Result:
no goals

Proof state:
R : Type u
σ : Type v
inst✝¹ : CommSemiring R
S : Type u_1
inst✝ : CommSemiring S
φ : R →+* S
f : MvPolynomial σ R
i : σ
r : R
⊢ (pderiv i) ((map φ) (C r)) = (map φ) ((pderiv i) (C r))

Tactic:
simp

Result:
no goals

Proof state:
R : Type u
σ : Type v
inst✝¹ : CommSemiring R
S : Type u_1
inst✝ : CommSemiring S
φ : R →+* S
f : MvPolynomial σ R
i : σ
p q : MvPolynomial σ R
hp : (pderiv i) ((map φ) p) = (map φ) ((pderiv i) p)
hq : (pderiv i) ((map φ) q) = (map φ) ((pderiv i) q)
⊢ (pderiv i) ((map φ) (p + q)) = (map φ) ((pderiv i) (p + q))

Tactic:
simp [hp, hq]

Result:
no goals

Proof state:
R : Type u
σ : Type v
inst✝¹ : CommSemiring R
S : Type u_1
inst✝ : CommSemiring S
φ : R →+* S
f : MvPolynomial σ R
i : σ
⊢ (pderiv i) ((map φ) f) = (map φ) ((pderiv i) f)

Tactic:
apply induction_on f (fun r ↦ by simp) (fun p q hp hq ↦ by simp [hp, hq]) fun p j eq ↦ ?_

Result:
R : Type u
σ : Type v
inst✝¹ : CommSemiring R
S : Type u_1
inst✝ : CommSemiring S
φ : R →+* S
f : MvPolynomial σ R
i : σ
p : MvPolynomial σ R
j : σ
eq : (pderiv i) ((map φ) p) = (map φ) ((pderiv i) p)
⊢ (pderiv i) ((map φ) (p * X j)) = (map φ) ((pderiv i) (p * X j))

Proof state:
case inr
R : Type u
σ : Type v
inst✝¹ : CommSemiring R
S : Type u_1
inst✝ : CommSemiring S
φ : R →+* S
f : MvPolynomial σ R
i : σ
p : MvPolynomial σ R
j : σ
eq : (pderiv i) ((map φ) p) = (map φ) ((pderiv i) p)
h : j ≠ i
⊢ (pderiv i) ((map φ) (p * X j)) = (map φ) ((pderiv i) (p * X j))

Tactic:
simp [eq, h]

Result:
no goals