harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/Data/Nat/Bits.lean
@[simp]
lemma bodd_add (m n : ℕ) : bodd (m + n) = bxor (bodd m) (bodd n)

Proof state:
m : ℕ
⊢ (m + 0).bodd = (m.bodd ^^ bodd 0)

Tactic:
simp

Result:
no goals

Proof state:
case zero
m : ℕ
⊢ (m + 0).bodd = (m.bodd ^^ bodd 0)

case succ
m n✝ : ℕ
a✝ : (m + n✝).bodd = (m.bodd ^^ n✝.bodd)
⊢ (m + (n✝ + 1)).bodd = (m.bodd ^^ (n✝ + 1).bodd)

Tactic:
case zero => simp

Result:
case succ
m n✝ : ℕ
a✝ : (m + n✝).bodd = (m.bodd ^^ n✝.bodd)
⊢ (m + (n✝ + 1)).bodd = (m.bodd ^^ (n✝ + 1).bodd)

Proof state:
m n : ℕ
⊢ (m + n).bodd = (m.bodd ^^ n.bodd)

Tactic:
induction n

Result:
case zero
m : ℕ
⊢ (m + 0).bodd = (m.bodd ^^ bodd 0)

case succ
m n✝ : ℕ
a✝ : (m + n✝).bodd = (m.bodd ^^ n✝.bodd)
⊢ (m + (n✝ + 1)).bodd = (m.bodd ^^ (n✝ + 1).bodd)

Proof state:
m n : ℕ
ih : (m + n).bodd = (m.bodd ^^ n.bodd)
⊢ (m + (n + 1)).bodd = (m.bodd ^^ (n + 1).bodd)

Tactic:
simp [← Nat.add_assoc, Bool.xor_not, ih]

Result:
no goals

Proof state:
case succ
m n✝ : ℕ
a✝ : (m + n✝).bodd = (m.bodd ^^ n✝.bodd)
⊢ (m + (n✝ + 1)).bodd = (m.bodd ^^ (n✝ + 1).bodd)

Tactic:
case succ n ih => simp [← Nat.add_assoc, Bool.xor_not, ih]

Result:
no goals
-- Mathlib/Algebra/Order/Group/Pointwise/Interval.lean
theorem image_add_const_Iic : (fun x => x + a) '' Iic b = Iic (b + a)

Proof state:
α : Type u_1
inst✝ : OrderedAddCommGroup α
a b : α
⊢ (fun x => x + a) '' Iic b = Iic (b + a)

Tactic:
simp

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Array/Attach.lean
theorem getElem?_pmap {p : α → Prop} (f : ∀ a, p a → β) {l : Array α} (h : ∀ a ∈ l, p a) (i : Nat) :
    (pmap f l h)[i]? = Option.pmap f l[i]? fun x H => h x (mem_of_getElem? H)

Proof state:
case mk
α : Type u_1
β : Type u_2
p : α → Prop
f : (a : α) → p a → β
i : Nat
toList✝ : List α
h : ∀ (a : α), a ∈ { toList := toList✝ } → p a
⊢ (pmap f { toList := toList✝ } h)[i]? = Option.pmap f { toList := toList✝ }[i]? ⋯

Tactic:
simp

Result:
no goals

Proof state:
α : Type u_1
β : Type u_2
p : α → Prop
f : (a : α) → p a → β
l : Array α
h : ∀ (a : α), a ∈ l → p a
i : Nat
⊢ (pmap f l h)[i]? = Option.pmap f l[i]? ⋯

Tactic:
cases l

Result:
case mk
α : Type u_1
β : Type u_2
p : α → Prop
f : (a : α) → p a → β
i : Nat
toList✝ : List α
h : ∀ (a : α), a ∈ { toList := toList✝ } → p a
⊢ (pmap f { toList := toList✝ } h)[i]? = Option.pmap f { toList := toList✝ }[i]? ⋯
-- Mathlib/Data/Nat/Choose/Basic.lean
theorem choose_eq_zero_of_lt : ∀ {n k}, n < k → choose n k = 0
  | _, 0, hk => absurd hk (Nat.not_lt_zero _)
  | 0, _ + 1, _ => choose_zero_succ _
  | n + 1, k + 1, hk => by
    have hnk : n < k := lt_of_succ_lt_succ hk
    have hnk1 : n < k + 1 := lt_of_succ_lt hk
    rw [choose_succ_succ, choose_eq_zero_of_lt hnk, choose_eq_zero_of_lt hnk1]

Proof state:
n k : ℕ
hk : n + 1 < k + 1
hnk : n < k
hnk1 : n < k + 1
⊢ (n + 1).choose (k + 1) = 0

Tactic:
rw [choose_succ_succ, choose_eq_zero_of_lt hnk, choose_eq_zero_of_lt hnk1]

Result:
no goals

Proof state:
n k : ℕ
hk : n + 1 < k + 1
hnk : n < k
⊢ (n + 1).choose (k + 1) = 0

Tactic:
have hnk1 : n < k + 1 := lt_of_succ_lt hk

Result:
n k : ℕ
hk : n + 1 < k + 1
hnk : n < k
hnk1 : n < k + 1
⊢ (n + 1).choose (k + 1) = 0

Proof state:
n k : ℕ
hk : n + 1 < k + 1
⊢ (n + 1).choose (k + 1) = 0

Tactic:
have hnk : n < k := lt_of_succ_lt_succ hk

Result:
n k : ℕ
hk : n + 1 < k + 1
hnk : n < k
⊢ (n + 1).choose (k + 1) = 0
-- Mathlib/MeasureTheory/Covering/BesicovitchVectorSpace.lean
theorem isEmpty_satelliteConfig_multiplicity :
    IsEmpty (SatelliteConfig E (multiplicity E) (goodτ E)) :=
  ⟨by
    intro a
    let b := a.centerAndRescale
    rcases b.exists_normalized a.centerAndRescale_center a.centerAndRescale_radius
        (one_lt_goodτ E).le (goodδ E) le_rfl (goodδ_lt_one E).le with
      ⟨c', c'_le_two, hc'⟩
    exact
      lt_irrefl _ ((Nat.lt_succ_self _).trans_le (le_multiplicity_of_δ_of_fin c' c'_le_two hc'))⟩

Proof state:
case intro.intro
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : FiniteDimensional ℝ E
a : SatelliteConfig E (multiplicity E) (goodτ E)
b : SatelliteConfig E (multiplicity E) (goodτ E) := a.centerAndRescale
c' : Fin (multiplicity E).succ → E
c'_le_two : ∀ (n : Fin (multiplicity E).succ), ‖c' n‖ ≤ 2
hc' : Pairwise fun i j => 1 - goodδ E ≤ ‖c' i - c' j‖
⊢ False

Tactic:
exact
  lt_irrefl _ ((Nat.lt_succ_self _).trans_le (le_multiplicity_of_δ_of_fin c' c'_le_two hc'))

Result:
no goals

Proof state:
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : FiniteDimensional ℝ E
a : SatelliteConfig E (multiplicity E) (goodτ E)
⊢ False

Tactic:
let b := a.centerAndRescale

Result:
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : FiniteDimensional ℝ E
a : SatelliteConfig E (multiplicity E) (goodτ E)
b : SatelliteConfig E (multiplicity E) (goodτ E) := a.centerAndRescale
⊢ False

Proof state:
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : FiniteDimensional ℝ E
a : SatelliteConfig E (multiplicity E) (goodτ E)
b : SatelliteConfig E (multiplicity E) (goodτ E) := a.centerAndRescale
⊢ False

Tactic:
rcases b.exists_normalized a.centerAndRescale_center a.centerAndRescale_radius
    (one_lt_goodτ E).le (goodδ E) le_rfl (goodδ_lt_one E).le with
  ⟨c', c'_le_two, hc'⟩

Result:
case intro.intro
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : FiniteDimensional ℝ E
a : SatelliteConfig E (multiplicity E) (goodτ E)
b : SatelliteConfig E (multiplicity E) (goodτ E) := a.centerAndRescale
c' : Fin (multiplicity E).succ → E
c'_le_two : ∀ (n : Fin (multiplicity E).succ), ‖c' n‖ ≤ 2
hc' : Pairwise fun i j => 1 - goodδ E ≤ ‖c' i - c' j‖
⊢ False

Proof state:
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : FiniteDimensional ℝ E
⊢ SatelliteConfig E (multiplicity E) (goodτ E) → False

Tactic:
intro a

Result:
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : FiniteDimensional ℝ E
a : SatelliteConfig E (multiplicity E) (goodτ E)
⊢ False
-- Mathlib/SetTheory/Nimber/Field.lean
theorem mul_le_of_forall_ne (h : ∀ a' < a, ∀ b' < b, a' * b + a * b' + a' * b' ≠ c) :
    a * b ≤ c

Proof state:
a b c : Nimber
h : ∀ a' < a, ∀ b' < b, a' * b + a * b' + a' * b' ≠ c
h' : c < a * b
this : ∃ a' < a, ∃ b' < b, a' * b + a * b' + a' * b' = c
⊢ False

Tactic:
tauto

Result:
no goals

Proof state:
a b c : Nimber
h : ∀ a' < a, ∀ b' < b, a' * b + a * b' + a' * b' ≠ c
h' : c < a * b
⊢ False

Tactic:
have := exists_of_lt_mul h'

Result:
a b c : Nimber
h : ∀ a' < a, ∀ b' < b, a' * b + a * b' + a' * b' ≠ c
h' : c < a * b
this : ∃ a' < a, ∃ b' < b, a' * b + a * b' + a' * b' = c
⊢ False

Proof state:
a b c : Nimber
h : ∀ a' < a, ∀ b' < b, a' * b + a * b' + a' * b' ≠ c
⊢ a * b ≤ c

Tactic:
by_contra! h'

Result:
a b c : Nimber
h : ∀ a' < a, ∀ b' < b, a' * b + a * b' + a' * b' ≠ c
h' : c < a * b
⊢ False
-- Mathlib/Topology/Baire/Lemmas.lean
theorem dense_sInter_of_isOpen {S : Set (Set X)} (ho : ∀ s ∈ S, IsOpen s) (hS : S.Countable)
    (hd : ∀ s ∈ S, Dense s) : Dense (⋂₀ S)

Proof state:
X : Type u_1
inst✝¹ : TopologicalSpace X
inst✝ : BaireSpace X
S : Set (Set X)
ho : ∀ s ∈ S, IsOpen s
hS : S.Countable
hd : ∀ s ∈ S, Dense s
⊢ Dense (⋂₀ S)

Tactic:
rcases S.eq_empty_or_nonempty with h | h

Result:
case inl
X : Type u_1
inst✝¹ : TopologicalSpace X
inst✝ : BaireSpace X
S : Set (Set X)
ho : ∀ s ∈ S, IsOpen s
hS : S.Countable
hd : ∀ s ∈ S, Dense s
h : S = ∅
⊢ Dense (⋂₀ S)

case inr
X : Type u_1
inst✝¹ : TopologicalSpace X
inst✝ : BaireSpace X
S : Set (Set X)
ho : ∀ s ∈ S, IsOpen s
hS : S.Countable
hd : ∀ s ∈ S, Dense s
h : S.Nonempty
⊢ Dense (⋂₀ S)

Proof state:
case inl
X : Type u_1
inst✝¹ : TopologicalSpace X
inst✝ : BaireSpace X
S : Set (Set X)
ho : ∀ s ∈ S, IsOpen s
hS : S.Countable
hd : ∀ s ∈ S, Dense s
h : S = ∅
⊢ Dense (⋂₀ S)

Tactic:
simp [h]

Result:
no goals

Proof state:
case inr.intro
X : Type u_1
inst✝¹ : TopologicalSpace X
inst✝ : BaireSpace X
f : ℕ → Set X
ho : ∀ s ∈ range f, IsOpen s
hS : (range f).Countable
hd : ∀ s ∈ range f, Dense s
h : (range f).Nonempty
⊢ Dense (⋂₀ range f)

Tactic:
exact dense_iInter_of_isOpen_nat (forall_mem_range.1 ho) (forall_mem_range.1 hd)

Result:
no goals

Proof state:
case inr
X : Type u_1
inst✝¹ : TopologicalSpace X
inst✝ : BaireSpace X
S : Set (Set X)
ho : ∀ s ∈ S, IsOpen s
hS : S.Countable
hd : ∀ s ∈ S, Dense s
h : S.Nonempty
⊢ Dense (⋂₀ S)

Tactic:
rcases hS.exists_eq_range h with ⟨f, rfl⟩

Result:
case inr.intro
X : Type u_1
inst✝¹ : TopologicalSpace X
inst✝ : BaireSpace X
f : ℕ → Set X
ho : ∀ s ∈ range f, IsOpen s
hS : (range f).Countable
hd : ∀ s ∈ range f, Dense s
h : (range f).Nonempty
⊢ Dense (⋂₀ range f)
-- Mathlib/Order/Lattice.lean
theorem inf_right_idem (a b : α) : a ⊓ b ⊓ b = a ⊓ b

Proof state:
α : Type u
inst✝ : SemilatticeInf α
a b : α
⊢ a ⊓ b ⊓ b = a ⊓ b

Tactic:
simp

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Vector/Lemmas.lean
theorem any_eq_true' {p : α → Bool} {xs : Vector α n} :
    xs.any p = true ↔ (∃ x, x ∈ xs ∧ p x)

Proof state:
α : Type u_1
n : Nat
p : α → Bool
xs : Vector α n
⊢ xs.any p = true ↔ ∃ x, x ∈ xs ∧ p x = true

Tactic:
rcases xs with ⟨xs, rfl⟩

Result:
case mk
α : Type u_1
p : α → Bool
xs : Array α
⊢ { toArray := xs, size_toArray := ⋯ }.any p = true ↔ ∃ x, x ∈ { toArray := xs, size_toArray := ⋯ } ∧ p x = true

Proof state:
case mk
α : Type u_1
p : α → Bool
xs : Array α
⊢ { toArray := xs, size_toArray := ⋯ }.any p = true ↔ ∃ x, x ∈ { toArray := xs, size_toArray := ⋯ } ∧ p x = true

Tactic:
simp only [any_mk, Array.any_eq_true']

Result:
case mk
α : Type u_1
p : α → Bool
xs : Array α
⊢ (∃ x, x ∈ xs ∧ p x = true) ↔ ∃ x, x ∈ { toArray := xs, size_toArray := ⋯ } ∧ p x = true

Proof state:
case mk
α : Type u_1
p : α → Bool
xs : Array α
⊢ (∃ x, x ∈ xs ∧ p x = true) ↔ ∃ x, x ∈ { toArray := xs, size_toArray := ⋯ } ∧ p x = true

Tactic:
simp

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Fin/Lemmas.lean
theorem addNat_zero (n : Nat) (i : Fin n) : addNat i 0 = i

Proof state:
n : Nat
i : Fin n
⊢ i.addNat 0 = i

Tactic:
ext

Result:
case h
n : Nat
i : Fin n
⊢ ↑(i.addNat 0) = ↑i

Proof state:
case h
n : Nat
i : Fin n
⊢ ↑(i.addNat 0) = ↑i

Tactic:
simp

Result:
no goals
-- Mathlib/Combinatorics/SimpleGraph/Finite.lean
theorem incidenceFinset_eq_filter [DecidableEq V] [Fintype G.edgeSet] :
    G.incidenceFinset v = {e ∈ G.edgeFinset | v ∈ e}

Proof state:
case h
V : Type u_1
G : SimpleGraph V
v : V
inst✝² : Fintype ↑(G.neighborSet v)
inst✝¹ : DecidableEq V
inst✝ : Fintype ↑G.edgeSet
e : Sym2 V
⊢ e ∈ G.incidenceFinset v ↔ e ∈ filter (fun e => v ∈ e) G.edgeFinset

Tactic:
induction e

Result:
case h.h
V : Type u_1
G : SimpleGraph V
v : V
inst✝² : Fintype ↑(G.neighborSet v)
inst✝¹ : DecidableEq V
inst✝ : Fintype ↑G.edgeSet
x✝ y✝ : V
⊢ s(x✝, y✝) ∈ G.incidenceFinset v ↔ s(x✝, y✝) ∈ filter (fun e => v ∈ e) G.edgeFinset

Proof state:
case h.h
V : Type u_1
G : SimpleGraph V
v : V
inst✝² : Fintype ↑(G.neighborSet v)
inst✝¹ : DecidableEq V
inst✝ : Fintype ↑G.edgeSet
x✝ y✝ : V
⊢ s(x✝, y✝) ∈ G.incidenceFinset v ↔ s(x✝, y✝) ∈ filter (fun e => v ∈ e) G.edgeFinset

Tactic:
simp [mk'_mem_incidenceSet_iff]

Result:
no goals

Proof state:
V : Type u_1
G : SimpleGraph V
v : V
inst✝² : Fintype ↑(G.neighborSet v)
inst✝¹ : DecidableEq V
inst✝ : Fintype ↑G.edgeSet
⊢ G.incidenceFinset v = filter (fun e => v ∈ e) G.edgeFinset

Tactic:
ext e

Result:
case h
V : Type u_1
G : SimpleGraph V
v : V
inst✝² : Fintype ↑(G.neighborSet v)
inst✝¹ : DecidableEq V
inst✝ : Fintype ↑G.edgeSet
e : Sym2 V
⊢ e ∈ G.incidenceFinset v ↔ e ∈ filter (fun e => v ∈ e) G.edgeFinset
-- Mathlib/GroupTheory/SpecificGroups/Cyclic.lean
theorem Subgroup.eq_bot_or_eq_top_of_prime_card
    (H : Subgroup G) [hp : Fact (Nat.card G).Prime] : H = ⊥ ∨ H = ⊤

Proof state:
G : Type u_2
inst✝ : Group G
H : Subgroup G
hp : Fact (Nat.Prime (Nat.card G))
this✝ : Finite G
this : Nat.card ↥H ∣ Nat.card G
⊢ H = ⊥ ∨ H = ⊤

Tactic:
rwa [Nat.dvd_prime hp.1, ← eq_bot_iff_card, card_eq_iff_eq_top] at this

Result:
no goals

Proof state:
G : Type u_2
inst✝ : Group G
H : Subgroup G
hp : Fact (Nat.Prime (Nat.card G))
this : Finite G
⊢ H = ⊥ ∨ H = ⊤

Tactic:
have := card_subgroup_dvd_card H

Result:
G : Type u_2
inst✝ : Group G
H : Subgroup G
hp : Fact (Nat.Prime (Nat.card G))
this✝ : Finite G
this : Nat.card ↥H ∣ Nat.card G
⊢ H = ⊥ ∨ H = ⊤

Proof state:
G : Type u_2
inst✝ : Group G
H : Subgroup G
hp : Fact (Nat.Prime (Nat.card G))
⊢ H = ⊥ ∨ H = ⊤

Tactic:
have : Finite G := Nat.finite_of_card_ne_zero hp.1.ne_zero

Result:
G : Type u_2
inst✝ : Group G
H : Subgroup G
hp : Fact (Nat.Prime (Nat.card G))
this : Finite G
⊢ H = ⊥ ∨ H = ⊤
-- Mathlib/NumberTheory/ModularForms/JacobiTheta/TwoVariable.lean
lemma jacobiTheta₂'_add_right (z τ : ℂ) : jacobiTheta₂' z (τ + 2) = jacobiTheta₂' z τ

Proof state:
z τ : ℂ
n : ℤ
⊢ cexp (↑π * I * ↑n ^ 2 * 2) = 1

Tactic:
rw [(by push_cast; ring : (π * I * n ^ 2 * 2 : ℂ) = (n ^ 2 :) * (2 * π * I)), exp_int_mul,
  exp_two_pi_mul_I, one_zpow]

Result:
no goals

Proof state:
z τ : ℂ
⊢ jacobiTheta₂' z (τ + 2) = jacobiTheta₂' z τ

Tactic:
refine tsum_congr (fun n ↦ ?_)

Result:
z τ : ℂ
n : ℤ
⊢ jacobiTheta₂'_term n z (τ + 2) = jacobiTheta₂'_term n z τ

Proof state:
z τ : ℂ
n : ℤ
this : cexp (↑π * I * ↑n ^ 2 * 2) = 1
⊢ 2 * ↑π * I * ↑n * (cexp (2 * ↑π * I * ↑n * z) * cexp (↑π * I * ↑n ^ 2 * (τ + 2))) =
    2 * ↑π * I * ↑n * (cexp (2 * ↑π * I * ↑n * z) * cexp (↑π * I * ↑n ^ 2 * τ))

Tactic:
rw [mul_add, Complex.exp_add, this, mul_one]

Result:
no goals

Proof state:
z τ : ℂ
n : ℤ
⊢ jacobiTheta₂'_term n z (τ + 2) = jacobiTheta₂'_term n z τ

Tactic:
simp_rw [jacobiTheta₂'_term, jacobiTheta₂_term, Complex.exp_add]

Result:
z τ : ℂ
n : ℤ
⊢ 2 * ↑π * I * ↑n * (cexp (2 * ↑π * I * ↑n * z) * cexp (↑π * I * ↑n ^ 2 * (τ + 2))) =
    2 * ↑π * I * ↑n * (cexp (2 * ↑π * I * ↑n * z) * cexp (↑π * I * ↑n ^ 2 * τ))

Proof state:
z τ : ℂ
n : ℤ
⊢ ↑π * I * ↑n ^ 2 * 2 = ↑(n ^ 2) * (2 * ↑π * I)

Tactic:
push_cast

Result:
z τ : ℂ
n : ℤ
⊢ ↑π * I * ↑n ^ 2 * 2 = ↑n ^ 2 * (2 * ↑π * I)

Proof state:
z τ : ℂ
n : ℤ
⊢ ↑π * I * ↑n ^ 2 * 2 = ↑n ^ 2 * (2 * ↑π * I)

Tactic:
ring

Result:
no goals

Proof state:
z τ : ℂ
n : ℤ
⊢ 2 * ↑π * I * ↑n * (cexp (2 * ↑π * I * ↑n * z) * cexp (↑π * I * ↑n ^ 2 * (τ + 2))) =
    2 * ↑π * I * ↑n * (cexp (2 * ↑π * I * ↑n * z) * cexp (↑π * I * ↑n ^ 2 * τ))

Tactic:
suffices cexp (π * I * n ^ 2 * 2 : ℂ) = 1 by rw [mul_add, Complex.exp_add, this, mul_one]

Result:
z τ : ℂ
n : ℤ
⊢ cexp (↑π * I * ↑n ^ 2 * 2) = 1
-- Mathlib/Algebra/BigOperators/Finprod.lean
theorem finprod_cond_ne (f : α → M) (a : α) [DecidableEq α] (hf : (mulSupport f).Finite) :
    (∏ᶠ (i) (_ : i ≠ a), f i) = ∏ i ∈ hf.toFinset.erase a, f i

Proof state:
case h
α : Type u_1
M : Type u_5
inst✝¹ : CommMonoid M
f : α → M
a : α
inst✝ : DecidableEq α
hf : (mulSupport f).Finite
x : α
hx : f x ≠ 1
⊢ x ≠ a ↔ x ∈ hf.toFinset.erase a

Tactic:
rw [Finset.mem_erase, Finite.mem_toFinset, mem_mulSupport]

Result:
case h
α : Type u_1
M : Type u_5
inst✝¹ : CommMonoid M
f : α → M
a : α
inst✝ : DecidableEq α
hf : (mulSupport f).Finite
x : α
hx : f x ≠ 1
⊢ x ≠ a ↔ x ≠ a ∧ f x ≠ 1

Proof state:
case h
α : Type u_1
M : Type u_5
inst✝¹ : CommMonoid M
f : α → M
a : α
inst✝ : DecidableEq α
hf : (mulSupport f).Finite
⊢ ∀ {x : α}, f x ≠ 1 → (x ≠ a ↔ x ∈ hf.toFinset.erase a)

Tactic:
intro x hx

Result:
case h
α : Type u_1
M : Type u_5
inst✝¹ : CommMonoid M
f : α → M
a : α
inst✝ : DecidableEq α
hf : (mulSupport f).Finite
x : α
hx : f x ≠ 1
⊢ x ≠ a ↔ x ∈ hf.toFinset.erase a

Proof state:
case h
α : Type u_1
M : Type u_5
inst✝¹ : CommMonoid M
f : α → M
a : α
inst✝ : DecidableEq α
hf : (mulSupport f).Finite
x : α
hx : f x ≠ 1
⊢ x ≠ a ↔ x ≠ a ∧ f x ≠ 1

Tactic:
exact ⟨fun h => And.intro h hx, fun h => h.1⟩

Result:
no goals

Proof state:
α : Type u_1
M : Type u_5
inst✝¹ : CommMonoid M
f : α → M
a : α
inst✝ : DecidableEq α
hf : (mulSupport f).Finite
⊢ ∏ᶠ (i : α) (_ : i ≠ a), f i = ∏ i ∈ hf.toFinset.erase a, f i

Tactic:
apply finprod_cond_eq_prod_of_cond_iff

Result:
case h
α : Type u_1
M : Type u_5
inst✝¹ : CommMonoid M
f : α → M
a : α
inst✝ : DecidableEq α
hf : (mulSupport f).Finite
⊢ ∀ {x : α}, f x ≠ 1 → (x ≠ a ↔ x ∈ hf.toFinset.erase a)
-- Mathlib/GroupTheory/FreeAbelianGroup.lean
theorem map_hom {α β γ} [AddCommGroup β] [AddCommGroup γ] (a : FreeAbelianGroup α) (f : α → β)
    (g : β →+ γ) : g (lift f a) = lift (g ∘ f) a

Proof state:
case hg
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝¹ : AddCommGroup β
inst✝ : AddCommGroup γ
a✝ : FreeAbelianGroup α
f : α → β
g : β →+ γ
a : α
⊢ (g.comp (lift f)) (of a) = (⇑g ∘ f) a

Tactic:
show g ((lift f) (of a)) = g (f a)

Result:
case hg
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝¹ : AddCommGroup β
inst✝ : AddCommGroup γ
a✝ : FreeAbelianGroup α
f : α → β
g : β →+ γ
a : α
⊢ g ((lift f) (of a)) = g (f a)

Proof state:
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝¹ : AddCommGroup β
inst✝ : AddCommGroup γ
a : FreeAbelianGroup α
f : α → β
g : β →+ γ
⊢ (g.comp (lift f)) a = (lift (⇑g ∘ f)) a

Tactic:
apply lift.unique

Result:
case hg
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝¹ : AddCommGroup β
inst✝ : AddCommGroup γ
a : FreeAbelianGroup α
f : α → β
g : β →+ γ
⊢ ∀ (x : α), (g.comp (lift f)) (of x) = (⇑g ∘ f) x

Proof state:
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝¹ : AddCommGroup β
inst✝ : AddCommGroup γ
a : FreeAbelianGroup α
f : α → β
g : β →+ γ
⊢ g ((lift f) a) = (lift (⇑g ∘ f)) a

Tactic:
show (g.comp (lift f)) a = lift (g ∘ f) a

Result:
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝¹ : AddCommGroup β
inst✝ : AddCommGroup γ
a : FreeAbelianGroup α
f : α → β
g : β →+ γ
⊢ (g.comp (lift f)) a = (lift (⇑g ∘ f)) a

Proof state:
case hg
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝¹ : AddCommGroup β
inst✝ : AddCommGroup γ
a : FreeAbelianGroup α
f : α → β
g : β →+ γ
⊢ ∀ (x : α), (g.comp (lift f)) (of x) = (⇑g ∘ f) x

Tactic:
intro a

Result:
case hg
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝¹ : AddCommGroup β
inst✝ : AddCommGroup γ
a✝ : FreeAbelianGroup α
f : α → β
g : β →+ γ
a : α
⊢ (g.comp (lift f)) (of a) = (⇑g ∘ f) a
-- Mathlib/NumberTheory/PellMatiyasevic.lean
theorem xn_add (m n) : xn a1 (m + n) = xn a1 m * xn a1 n + d a1 * yn a1 m * yn a1 n

Proof state:
a : ℕ
a1 : 1 < a
m n : ℕ
h : ↑(xn a1 (m + n)) = (pellZd a1 m).re * (pellZd a1 n).re + ↑(Pell.d a1) * (pellZd a1 m).im * (pellZd a1 n).im
im_eq✝ : ↑(yn a1 (m + n)) = (pellZd a1 m).re * (pellZd a1 n).im + (pellZd a1 m).im * (pellZd a1 n).re
⊢ xn a1 (m + n) = xn a1 m * xn a1 n + Pell.d a1 * yn a1 m * yn a1 n

Tactic:
zify

Result:
a : ℕ
a1 : 1 < a
m n : ℕ
h : ↑(xn a1 (m + n)) = (pellZd a1 m).re * (pellZd a1 n).re + ↑(Pell.d a1) * (pellZd a1 m).im * (pellZd a1 n).im
im_eq✝ : ↑(yn a1 (m + n)) = (pellZd a1 m).re * (pellZd a1 n).im + (pellZd a1 m).im * (pellZd a1 n).re
⊢ ↑(xn a1 (m + n)) = ↑(xn a1 m) * ↑(xn a1 n) + ↑(Pell.d a1) * ↑(yn a1 m) * ↑(yn a1 n)

Proof state:
a : ℕ
a1 : 1 < a
m n : ℕ
h : ↑(xn a1 (m + n)) = (pellZd a1 m).re * (pellZd a1 n).re + ↑(Pell.d a1) * (pellZd a1 m).im * (pellZd a1 n).im
im_eq✝ : ↑(yn a1 (m + n)) = (pellZd a1 m).re * (pellZd a1 n).im + (pellZd a1 m).im * (pellZd a1 n).re
⊢ (pellZd a1 m).re * (pellZd a1 n).re + ↑(Pell.d a1) * (pellZd a1 m).im * (pellZd a1 n).im =
    ↑(xn a1 m) * ↑(xn a1 n) + ↑(Pell.d a1) * ↑(yn a1 m) * ↑(yn a1 n)

Tactic:
simp [pellZd]

Result:
no goals

Proof state:
a : ℕ
a1 : 1 < a
m n : ℕ
h : ↑(xn a1 (m + n)) = (pellZd a1 m).re * (pellZd a1 n).re + ↑(Pell.d a1) * (pellZd a1 m).im * (pellZd a1 n).im
im_eq✝ : ↑(yn a1 (m + n)) = (pellZd a1 m).re * (pellZd a1 n).im + (pellZd a1 m).im * (pellZd a1 n).re
⊢ ↑(xn a1 (m + n)) = ↑(xn a1 m) * ↑(xn a1 n) + ↑(Pell.d a1) * ↑(yn a1 m) * ↑(yn a1 n)

Tactic:
rw [h]

Result:
a : ℕ
a1 : 1 < a
m n : ℕ
h : ↑(xn a1 (m + n)) = (pellZd a1 m).re * (pellZd a1 n).re + ↑(Pell.d a1) * (pellZd a1 m).im * (pellZd a1 n).im
im_eq✝ : ↑(yn a1 (m + n)) = (pellZd a1 m).re * (pellZd a1 n).im + (pellZd a1 m).im * (pellZd a1 n).re
⊢ (pellZd a1 m).re * (pellZd a1 n).re + ↑(Pell.d a1) * (pellZd a1 m).im * (pellZd a1 n).im =
    ↑(xn a1 m) * ↑(xn a1 n) + ↑(Pell.d a1) * ↑(yn a1 m) * ↑(yn a1 n)

Proof state:
a : ℕ
a1 : 1 < a
m n : ℕ
⊢ xn a1 (m + n) = xn a1 m * xn a1 n + Pell.d a1 * yn a1 m * yn a1 n

Tactic:
injection pellZd_add a1 m n with h _

Result:
a : ℕ
a1 : 1 < a
m n : ℕ
h : ↑(xn a1 (m + n)) = (pellZd a1 m).re * (pellZd a1 n).re + ↑(Pell.d a1) * (pellZd a1 m).im * (pellZd a1 n).im
im_eq✝ : ↑(yn a1 (m + n)) = (pellZd a1 m).re * (pellZd a1 n).im + (pellZd a1 m).im * (pellZd a1 n).re
⊢ xn a1 (m + n) = xn a1 m * xn a1 n + Pell.d a1 * yn a1 m * yn a1 n
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/BitVec/Lemmas.lean
theorem getLsbD_ge (x : BitVec w) (i : Nat) (ge : w ≤ i) : getLsbD x i = false

Proof state:
w : Nat
x : BitVec w
i : Nat
ge : w ≤ i
⊢ x.getLsbD i = false

Tactic:
let ⟨x, x_lt⟩ := x

Result:
w : Nat
x✝ : BitVec w
i : Nat
ge : w ≤ i
x : Nat
x_lt : x < 2 ^ w
⊢ { toFin := ⟨x, x_lt⟩ }.getLsbD i = false

Proof state:
case lt
w : Nat
x✝ : BitVec w
i : Nat
ge : w ≤ i
x : Nat
x_lt : x < 2 ^ w
p : 2 ^ w ≤ 2 ^ i
⊢ x < 2 ^ i

Tactic:
omega

Result:
no goals

Proof state:
w : Nat
x✝ : BitVec w
i : Nat
ge : w ≤ i
x : Nat
x_lt : x < 2 ^ w
⊢ { toFin := ⟨x, x_lt⟩ }.getLsbD i = false

Tactic:
simp only [getLsbD_ofFin]

Result:
w : Nat
x✝ : BitVec w
i : Nat
ge : w ≤ i
x : Nat
x_lt : x < 2 ^ w
⊢ x.testBit i = false

Proof state:
w : Nat
x✝ : BitVec w
i : Nat
ge : w ≤ i
x : Nat
x_lt : x < 2 ^ w
⊢ x.testBit i = false

Tactic:
apply Nat.testBit_lt_two_pow

Result:
case lt
w : Nat
x✝ : BitVec w
i : Nat
ge : w ≤ i
x : Nat
x_lt : x < 2 ^ w
⊢ x < 2 ^ i

Proof state:
case lt
w : Nat
x✝ : BitVec w
i : Nat
ge : w ≤ i
x : Nat
x_lt : x < 2 ^ w
⊢ x < 2 ^ i

Tactic:
have p : 2^w ≤ 2^i := Nat.pow_le_pow_of_le_right (by omega) ge

Result:
case lt
w : Nat
x✝ : BitVec w
i : Nat
ge : w ≤ i
x : Nat
x_lt : x < 2 ^ w
p : 2 ^ w ≤ 2 ^ i
⊢ x < 2 ^ i

Proof state:
w : Nat
x✝ : BitVec w
i : Nat
ge : w ≤ i
x : Nat
x_lt : x < 2 ^ w
⊢ 2 > 0

Tactic:
omega

Result:
no goals
-- Mathlib/Topology/Algebra/Algebra/Equiv.lean
theorem image_symm_eq_preimage (e : A ≃A[R] B) (S : Set B) : e.symm '' S = e ⁻¹' S

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
S : Set B
⊢ ⇑e.symm '' S = ⇑e ⁻¹' S

Tactic:
rw [e.symm.image_eq_preimage, e.symm_symm]

Result:
no goals
-- Mathlib/CategoryTheory/Quotient.lean
theorem sound {a b : C} {f₁ f₂ : a ⟶ b} (h : r f₁ f₂) :
    (functor r).map f₁ = (functor r).map f₂

Proof state:
C : Type u_2
inst✝ : Category.{u_1, u_2} C
r : HomRel C
a b : C
f₁ f₂ : a ⟶ b
h : r f₁ f₂
⊢ (functor r).map f₁ = (functor r).map f₂

Tactic:
simpa using Quot.sound (CompClosure.intro (𝟙 a) f₁ f₂ (𝟙 b) h)

Result:
no goals
-- Mathlib/Analysis/Calculus/FDeriv/Basic.lean
theorem hasFDerivWithinAt_inter' (h : t ∈ 𝓝[s] x) :
    HasFDerivWithinAt f f' (s ∩ t) x ↔ HasFDerivWithinAt f f' s x

Proof state:
𝕜 : Type u_1
inst✝⁴ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
F : Type u_3
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
f : E → F
f' : E →L[𝕜] F
x : E
s t : Set E
h : t ∈ 𝓝[s] x
⊢ HasFDerivWithinAt f f' (s ∩ t) x ↔ HasFDerivWithinAt f f' s x

Tactic:
simp [HasFDerivWithinAt, nhdsWithin_restrict'' s h]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Fin/Lemmas.lean
theorem cast_refl (n : Nat) (h : n = n) : Fin.cast h = id

Proof state:
n : Nat
h : n = n
⊢ Fin.cast h = id

Tactic:
ext

Result:
case h.h
n : Nat
h : n = n
x✝ : Fin n
⊢ ↑(Fin.cast h x✝) = ↑(id x✝)

Proof state:
case h.h
n : Nat
h : n = n
x✝ : Fin n
⊢ ↑(Fin.cast h x✝) = ↑(id x✝)

Tactic:
simp

Result:
no goals